Z3
Public Member Functions | Data Fields
Fixedpoint Class Reference

Fixedpoint. More...

+ Inheritance diagram for Fixedpoint:

Public Member Functions

def __init__ (self, fixedpoint=None, ctx=None)
 
def __del__ (self)
 
def set (self, args, keys)
 
def help (self)
 
def param_descrs (self)
 
def assert_exprs (self, args)
 
def add (self, args)
 
def __iadd__ (self, fml)
 
def append (self, args)
 
def insert (self, args)
 
def add_rule (self, head, body=None, name=None)
 
def rule (self, head, body=None, name=None)
 
def fact (self, head, name=None)
 
def query (self, query)
 
def push (self)
 
def pop (self)
 
def update_rule (self, head, body, name)
 
def get_answer (self)
 
def get_num_levels (self, predicate)
 
def get_cover_delta (self, level, predicate)
 
def add_cover (self, level, predicate, property)
 
def register_relation (self, relations)
 
def set_predicate_representation (self, f, representations)
 
def parse_string (self, s)
 
def parse_file (self, f)
 
def get_rules (self)
 
def get_assertions (self)
 
def __repr__ (self)
 
def sexpr (self)
 
def to_string (self, queries)
 
def statistics (self)
 
def reason_unknown (self)
 
def declare_var (self, vars)
 
def abstract (self, fml, is_forall=True)
 
- Public Member Functions inherited from Z3PPObject
def use_pp (self)
 

Data Fields

 ctx
 
 fixedpoint
 
 vars
 

Detailed Description

Fixedpoint.

Fixedpoint API provides methods for solving with recursive predicates

Definition at line 6319 of file z3py.py.

Constructor & Destructor Documentation

§ __init__()

def __init__ (   self,
  fixedpoint = None,
  ctx = None 
)

Definition at line 6322 of file z3py.py.

6322  def __init__(self, fixedpoint=None, ctx=None):
6323  assert fixedpoint is None or ctx is not None
6324  self.ctx = _get_ctx(ctx)
6325  self.fixedpoint = None
6326  if fixedpoint is None:
6327  self.fixedpoint = Z3_mk_fixedpoint(self.ctx.ref())
6328  else:
6329  self.fixedpoint = fixedpoint
6330  Z3_fixedpoint_inc_ref(self.ctx.ref(), self.fixedpoint)
6331  self.vars = []
6332 

§ __del__()

def __del__ (   self)

Definition at line 6333 of file z3py.py.

6333  def __del__(self):
6334  if self.fixedpoint is not None and self.ctx.ref() is not None:
6335  Z3_fixedpoint_dec_ref(self.ctx.ref(), self.fixedpoint)
6336 

Member Function Documentation

§ __iadd__()

def __iadd__ (   self,
  fml 
)

Definition at line 6369 of file z3py.py.

6369  def __iadd__(self, fml):
6370  self.add(fml)
6371  return self
6372 

§ __repr__()

def __repr__ (   self)
Return a formatted string with all added rules and constraints.

Definition at line 6501 of file z3py.py.

6501  def __repr__(self):
6502  """Return a formatted string with all added rules and constraints."""
6503  return self.sexpr()
6504 

§ abstract()

def abstract (   self,
  fml,
  is_forall = True 
)

Definition at line 6537 of file z3py.py.

Referenced by Fixedpoint.add_rule(), Fixedpoint.assert_exprs(), Fixedpoint.query(), and Fixedpoint.update_rule().

6537  def abstract(self, fml, is_forall=True):
6538  if self.vars == []:
6539  return fml
6540  if is_forall:
6541  return ForAll(self.vars, fml)
6542  else:
6543  return Exists(self.vars, fml)
6544 
6545 
def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
Definition: z3py.py:1895
def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
Definition: z3py.py:1876

§ add()

def add (   self,
  args 
)
Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.

Definition at line 6365 of file z3py.py.

Referenced by Fixedpoint.__iadd__(), and Optimize.__iadd__().

6365  def add(self, *args):
6366  """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
6367  self.assert_exprs(*args)
6368 

§ add_cover()

def add_cover (   self,
  level,
  predicate,
  property 
)
Add property to predicate for the level'th unfolding. -1 is treated as infinity (infinity)

Definition at line 6465 of file z3py.py.

6465  def add_cover(self, level, predicate, property):
6466  """Add property to predicate for the level'th unfolding. -1 is treated as infinity (infinity)"""
6467  Z3_fixedpoint_add_cover(self.ctx.ref(), self.fixedpoint, level, predicate.ast, property.ast)
6468 

§ add_rule()

def add_rule (   self,
  head,
  body = None,
  name = None 
)
Assert rules defining recursive predicates to the fixedpoint solver.
>>> a = Bool('a')
>>> b = Bool('b')
>>> s = Fixedpoint()
>>> s.register_relation(a.decl())
>>> s.register_relation(b.decl())
>>> s.fact(a)
>>> s.rule(b, a)
>>> s.query(b)
sat

Definition at line 6381 of file z3py.py.

Referenced by Fixedpoint.fact(), and Fixedpoint.rule().

6381  def add_rule(self, head, body = None, name = None):
6382  """Assert rules defining recursive predicates to the fixedpoint solver.
6383  >>> a = Bool('a')
6384  >>> b = Bool('b')
6385  >>> s = Fixedpoint()
6386  >>> s.register_relation(a.decl())
6387  >>> s.register_relation(b.decl())
6388  >>> s.fact(a)
6389  >>> s.rule(b, a)
6390  >>> s.query(b)
6391  sat
6392  """
6393  if name is None:
6394  name = ""
6395  name = to_symbol(name, self.ctx)
6396  if body is None:
6397  head = self.abstract(head)
6398  Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, head.as_ast(), name)
6399  else:
6400  body = _get_args(body)
6401  f = self.abstract(Implies(And(body, self.ctx),head))
6402  Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
6403 
def to_symbol(s, ctx=None)
Definition: z3py.py:100
def And(args)
Definition: z3py.py:1550
def Implies(a, b, ctx=None)
Definition: z3py.py:1495

§ append()

def append (   self,
  args 
)
Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.

Definition at line 6373 of file z3py.py.

6373  def append(self, *args):
6374  """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
6375  self.assert_exprs(*args)
6376 

§ assert_exprs()

def assert_exprs (   self,
  args 
)
Assert constraints as background axioms for the fixedpoint solver.

Definition at line 6351 of file z3py.py.

Referenced by Fixedpoint.add(), Optimize.add(), Fixedpoint.append(), and Fixedpoint.insert().

6351  def assert_exprs(self, *args):
6352  """Assert constraints as background axioms for the fixedpoint solver."""
6353  args = _get_args(args)
6354  s = BoolSort(self.ctx)
6355  for arg in args:
6356  if isinstance(arg, Goal) or isinstance(arg, AstVector):
6357  for f in arg:
6358  f = self.abstract(f)
6359  Z3_fixedpoint_assert(self.ctx.ref(), self.fixedpoint, f.as_ast())
6360  else:
6361  arg = s.cast(arg)
6362  arg = self.abstract(arg)
6363  Z3_fixedpoint_assert(self.ctx.ref(), self.fixedpoint, arg.as_ast())
6364 
def BoolSort(ctx=None)
Definition: z3py.py:1407

§ declare_var()

def declare_var (   self,
  vars 
)
Add variable or several variables.
The added variable or variables will be bound in the rules
and queries

Definition at line 6528 of file z3py.py.

6528  def declare_var(self, *vars):
6529  """Add variable or several variables.
6530  The added variable or variables will be bound in the rules
6531  and queries
6532  """
6533  vars = _get_args(vars)
6534  for v in vars:
6535  self.vars += [v]
6536 

§ fact()

def fact (   self,
  head,
  name = None 
)
Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule.

Definition at line 6408 of file z3py.py.

6408  def fact(self, head, name = None):
6409  """Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
6410  self.add_rule(head, None, name)
6411 

§ get_answer()

def get_answer (   self)
Retrieve answer from last query call.

Definition at line 6451 of file z3py.py.

6451  def get_answer(self):
6452  """Retrieve answer from last query call."""
6453  r = Z3_fixedpoint_get_answer(self.ctx.ref(), self.fixedpoint)
6454  return _to_expr_ref(r, self.ctx)
6455 

§ get_assertions()

def get_assertions (   self)
retrieve assertions that have been added to fixedpoint context

Definition at line 6497 of file z3py.py.

6497  def get_assertions(self):
6498  """retrieve assertions that have been added to fixedpoint context"""
6499  return AstVector(Z3_fixedpoint_get_assertions(self.ctx.ref(), self.fixedpoint), self.ctx)
6500 

§ get_cover_delta()

def get_cover_delta (   self,
  level,
  predicate 
)
Retrieve properties known about predicate for the level'th unfolding. -1 is treated as the limit (infinity)

Definition at line 6460 of file z3py.py.

6460  def get_cover_delta(self, level, predicate):
6461  """Retrieve properties known about predicate for the level'th unfolding. -1 is treated as the limit (infinity)"""
6462  r = Z3_fixedpoint_get_cover_delta(self.ctx.ref(), self.fixedpoint, level, predicate.ast)
6463  return _to_expr_ref(r, self.ctx)
6464 

§ get_num_levels()

def get_num_levels (   self,
  predicate 
)
Retrieve number of levels used for predicate in PDR engine

Definition at line 6456 of file z3py.py.

6456  def get_num_levels(self, predicate):
6457  """Retrieve number of levels used for predicate in PDR engine"""
6458  return Z3_fixedpoint_get_num_levels(self.ctx.ref(), self.fixedpoint, predicate.ast)
6459 

§ get_rules()

def get_rules (   self)
retrieve rules that have been added to fixedpoint context

Definition at line 6493 of file z3py.py.

6493  def get_rules(self):
6494  """retrieve rules that have been added to fixedpoint context"""
6495  return AstVector(Z3_fixedpoint_get_rules(self.ctx.ref(), self.fixedpoint), self.ctx)
6496 

§ help()

def help (   self)
Display a string describing all available options.

Definition at line 6343 of file z3py.py.

6343  def help(self):
6344  """Display a string describing all available options."""
6345  print(Z3_fixedpoint_get_help(self.ctx.ref(), self.fixedpoint))
6346 

§ insert()

def insert (   self,
  args 
)
Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.

Definition at line 6377 of file z3py.py.

6377  def insert(self, *args):
6378  """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
6379  self.assert_exprs(*args)
6380 

§ param_descrs()

def param_descrs (   self)
Return the parameter description set.

Definition at line 6347 of file z3py.py.

6347  def param_descrs(self):
6348  """Return the parameter description set."""
6349  return ParamDescrsRef(Z3_fixedpoint_get_param_descrs(self.ctx.ref(), self.fixedpoint), self.ctx)
6350 

§ parse_file()

def parse_file (   self,
  f 
)
Parse rules and queries from a file

Definition at line 6489 of file z3py.py.

6489  def parse_file(self, f):
6490  """Parse rules and queries from a file"""
6491  return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx)
6492 

§ parse_string()

def parse_string (   self,
  s 
)
Parse rules and queries from a string

Definition at line 6485 of file z3py.py.

6485  def parse_string(self, s):
6486  """Parse rules and queries from a string"""
6487  return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx)
6488 

§ pop()

def pop (   self)
restore to previously created backtracking point

Definition at line 6438 of file z3py.py.

6438  def pop(self):
6439  """restore to previously created backtracking point"""
6440  Z3_fixedpoint_pop(self.ctx.ref(), self.fixedpoint)
6441 

§ push()

def push (   self)
create a backtracking point for added rules, facts and assertions

Definition at line 6434 of file z3py.py.

6434  def push(self):
6435  """create a backtracking point for added rules, facts and assertions"""
6436  Z3_fixedpoint_push(self.ctx.ref(), self.fixedpoint)
6437 

§ query()

def query (   self,
  query 
)
Query the fixedpoint engine whether formula is derivable.
   You can also pass an tuple or list of recursive predicates.

Definition at line 6412 of file z3py.py.

6412  def query(self, *query):
6413  """Query the fixedpoint engine whether formula is derivable.
6414  You can also pass an tuple or list of recursive predicates.
6415  """
6416  query = _get_args(query)
6417  sz = len(query)
6418  if sz >= 1 and isinstance(query[0], FuncDeclRef):
6419  _decls = (FuncDecl * sz)()
6420  i = 0
6421  for q in query:
6422  _decls[i] = q.ast
6423  i = i + 1
6424  r = Z3_fixedpoint_query_relations(self.ctx.ref(), self.fixedpoint, sz, _decls)
6425  else:
6426  if sz == 1:
6427  query = query[0]
6428  else:
6429  query = And(query, self.ctx)
6430  query = self.abstract(query, False)
6431  r = Z3_fixedpoint_query(self.ctx.ref(), self.fixedpoint, query.as_ast())
6432  return CheckSatResult(r)
6433 
def And(args)
Definition: z3py.py:1550

§ reason_unknown()

def reason_unknown (   self)
Return a string describing why the last `query()` returned `unknown`.

Definition at line 6523 of file z3py.py.

6523  def reason_unknown(self):
6524  """Return a string describing why the last `query()` returned `unknown`.
6525  """
6526  return Z3_fixedpoint_get_reason_unknown(self.ctx.ref(), self.fixedpoint)
6527 

§ register_relation()

def register_relation (   self,
  relations 
)
Register relation as recursive

Definition at line 6469 of file z3py.py.

6469  def register_relation(self, *relations):
6470  """Register relation as recursive"""
6471  relations = _get_args(relations)
6472  for f in relations:
6473  Z3_fixedpoint_register_relation(self.ctx.ref(), self.fixedpoint, f.ast)
6474 

§ rule()

def rule (   self,
  head,
  body = None,
  name = None 
)
Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule.

Definition at line 6404 of file z3py.py.

6404  def rule(self, head, body = None, name = None):
6405  """Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
6406  self.add_rule(head, body, name)
6407 

§ set()

def set (   self,
  args,
  keys 
)
Set a configuration option. The method `help()` return a string containing all available options.

Definition at line 6337 of file z3py.py.

6337  def set(self, *args, **keys):
6338  """Set a configuration option. The method `help()` return a string containing all available options.
6339  """
6340  p = args2params(args, keys, self.ctx)
6341  Z3_fixedpoint_set_params(self.ctx.ref(), self.fixedpoint, p.params)
6342 
def args2params(arguments, keywords, ctx=None)
Definition: z3py.py:4644

§ set_predicate_representation()

def set_predicate_representation (   self,
  f,
  representations 
)
Control how relation is represented

Definition at line 6475 of file z3py.py.

6475  def set_predicate_representation(self, f, *representations):
6476  """Control how relation is represented"""
6477  representations = _get_args(representations)
6478  representations = [to_symbol(s) for s in representations]
6479  sz = len(representations)
6480  args = (Symbol * sz)()
6481  for i in range(sz):
6482  args[i] = representations[i]
6483  Z3_fixedpoint_set_predicate_representation(self.ctx.ref(), self.fixedpoint, f.ast, sz, args)
6484 
def to_symbol(s, ctx=None)
Definition: z3py.py:100

§ sexpr()

def sexpr (   self)
Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.

Definition at line 6505 of file z3py.py.

Referenced by Fixedpoint.__repr__(), and Optimize.__repr__().

6505  def sexpr(self):
6506  """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
6507  """
6508  return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, 0, (Ast * 0)())
6509 

§ statistics()

def statistics (   self)
Return statistics for the last `query()`.

Definition at line 6518 of file z3py.py.

6518  def statistics(self):
6519  """Return statistics for the last `query()`.
6520  """
6521  return Statistics(Z3_fixedpoint_get_statistics(self.ctx.ref(), self.fixedpoint), self.ctx)
6522 

§ to_string()

def to_string (   self,
  queries 
)
Return a formatted string (in Lisp-like format) with all added constraints.
   We say the string is in s-expression format.
   Include also queries.

Definition at line 6510 of file z3py.py.

6510  def to_string(self, queries):
6511  """Return a formatted string (in Lisp-like format) with all added constraints.
6512  We say the string is in s-expression format.
6513  Include also queries.
6514  """
6515  args, len = _to_ast_array(queries)
6516  return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, len, args)
6517 

§ update_rule()

def update_rule (   self,
  head,
  body,
  name 
)
update rule

Definition at line 6442 of file z3py.py.

6442  def update_rule(self, head, body, name):
6443  """update rule"""
6444  if name is None:
6445  name = ""
6446  name = to_symbol(name, self.ctx)
6447  body = _get_args(body)
6448  f = self.abstract(Implies(And(body, self.ctx),head))
6449  Z3_fixedpoint_update_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
6450 
def to_symbol(s, ctx=None)
Definition: z3py.py:100
def And(args)
Definition: z3py.py:1550
def Implies(a, b, ctx=None)
Definition: z3py.py:1495

Field Documentation

§ ctx

ctx

§ fixedpoint

fixedpoint

§ vars

vars

Definition at line 6331 of file z3py.py.

Referenced by Fixedpoint.abstract(), and Fixedpoint.declare_var().