Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
Public Member Functions | Data Fields
Fixedpoint Class Reference

Fixedpoint. More...

+ Inheritance diagram for Fixedpoint:

Public Member Functions

def __init__
 
def __del__
 
def set
 
def help
 
def param_descrs
 
def assert_exprs
 
def add
 
def append
 
def insert
 
def add_rule
 
def rule
 
def fact
 
def query
 
def push
 
def pop
 
def update_rule
 
def get_answer
 
def get_num_levels
 
def get_cover_delta
 
def add_cover
 
def register_relation
 
def set_predicate_representation
 
def parse_string
 
def parse_file
 
def get_rules
 
def get_assertions
 
def __repr__
 
def sexpr
 
def to_string
 
def statistics
 
def reason_unknown
 
def declare_var
 
def abstract
 
- Public Member Functions inherited from Z3PPObject
def use_pp
 

Data Fields

 ctx
 
 fixedpoint
 
 vars
 

Detailed Description

Fixedpoint.

Fixedpoint API provides methods for solving with recursive predicates

Definition at line 5975 of file z3py.py.

Constructor & Destructor Documentation

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

Definition at line 5978 of file z3py.py.

5979  def __init__(self, fixedpoint=None, ctx=None):
5980  assert fixedpoint == None or ctx != None
5981  self.ctx = _get_ctx(ctx)
5982  self.fixedpoint = None
5983  if fixedpoint == None:
5984  self.fixedpoint = Z3_mk_fixedpoint(self.ctx.ref())
5985  else:
5986  self.fixedpoint = fixedpoint
5987  Z3_fixedpoint_inc_ref(self.ctx.ref(), self.fixedpoint)
5988  self.vars = []
def __del__ (   self)

Definition at line 5989 of file z3py.py.

5990  def __del__(self):
5991  if self.fixedpoint != None:
5992  Z3_fixedpoint_dec_ref(self.ctx.ref(), self.fixedpoint)

Member Function Documentation

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

Definition at line 6153 of file z3py.py.

6154  def __repr__(self):
6155  """Return a formatted string with all added rules and constraints."""
6156  return self.sexpr()
def abstract (   self,
  fml,
  is_forall = True 
)

Definition at line 6189 of file z3py.py.

6190  def abstract(self, fml, is_forall=True):
6191  if self.vars == []:
6192  return fml
6193  if is_forall:
6194  return ForAll(self.vars, fml)
6195  else:
6196  return Exists(self.vars, fml)
def add (   self,
  args 
)
Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.

Definition at line 6021 of file z3py.py.

6022  def add(self, *args):
6023  """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
6024  self.assert_exprs(*args)
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 6117 of file z3py.py.

6118  def add_cover(self, level, predicate, property):
6119  """Add property to predicate for the level'th unfolding. -1 is treated as infinity (infinity)"""
6120  Z3_fixedpoint_add_cover(self.ctx.ref(), self.fixedpoint, level, predicate.ast, property.ast)
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 6033 of file z3py.py.

6034  def add_rule(self, head, body = None, name = None):
6035  """Assert rules defining recursive predicates to the fixedpoint solver.
6036  >>> a = Bool('a')
6037  >>> b = Bool('b')
6038  >>> s = Fixedpoint()
6039  >>> s.register_relation(a.decl())
6040  >>> s.register_relation(b.decl())
6041  >>> s.fact(a)
6042  >>> s.rule(b, a)
6043  >>> s.query(b)
6044  sat
6045  """
6046  if name == None:
6047  name = ""
6048  name = to_symbol(name, self.ctx)
6049  if body == None:
6050  head = self.abstract(head)
6051  Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, head.as_ast(), name)
6052  else:
6053  body = _get_args(body)
6054  f = self.abstract(Implies(And(body),head))
6055  Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
def append (   self,
  args 
)
Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.

Definition at line 6025 of file z3py.py.

6026  def append(self, *args):
6027  """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
6028  self.assert_exprs(*args)
def assert_exprs (   self,
  args 
)
Assert constraints as background axioms for the fixedpoint solver.

Definition at line 6007 of file z3py.py.

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

6008  def assert_exprs(self, *args):
6009  """Assert constraints as background axioms for the fixedpoint solver."""
6010  args = _get_args(args)
6011  s = BoolSort(self.ctx)
6012  for arg in args:
6013  if isinstance(arg, Goal) or isinstance(arg, AstVector):
6014  for f in arg:
6015  f = self.abstract(f)
6016  Z3_fixedpoint_assert(self.ctx.ref(), self.fixedpoint, f.as_ast())
6017  else:
6018  arg = s.cast(arg)
6019  arg = self.abstract(arg)
6020  Z3_fixedpoint_assert(self.ctx.ref(), self.fixedpoint, arg.as_ast())
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 6180 of file z3py.py.

6181  def declare_var(self, *vars):
6182  """Add variable or several variables.
6183  The added variable or variables will be bound in the rules
6184  and queries
6185  """
6186  vars = _get_args(vars)
6187  for v in vars:
6188  self.vars += [v]
def fact (   self,
  head,
  name = None 
)
Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule.

Definition at line 6060 of file z3py.py.

6061  def fact(self, head, name = None):
6062  """Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
6063  self.add_rule(head, None, name)
def get_answer (   self)
Retrieve answer from last query call.

Definition at line 6103 of file z3py.py.

6104  def get_answer(self):
6105  """Retrieve answer from last query call."""
6106  r = Z3_fixedpoint_get_answer(self.ctx.ref(), self.fixedpoint)
6107  return _to_expr_ref(r, self.ctx)
def get_assertions (   self)
retrieve assertions that have been added to fixedpoint context

Definition at line 6149 of file z3py.py.

6150  def get_assertions(self):
6151  """retrieve assertions that have been added to fixedpoint context"""
6152  return AstVector(Z3_fixedpoint_get_assertions(self.ctx.ref(), self.fixedpoint), self.ctx)
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 6112 of file z3py.py.

6113  def get_cover_delta(self, level, predicate):
6114  """Retrieve properties known about predicate for the level'th unfolding. -1 is treated as the limit (infinity)"""
6115  r = Z3_fixedpoint_get_cover_delta(self.ctx.ref(), self.fixedpoint, level, predicate.ast)
6116  return _to_expr_ref(r, self.ctx)
def get_num_levels (   self,
  predicate 
)
Retrieve number of levels used for predicate in PDR engine

Definition at line 6108 of file z3py.py.

6109  def get_num_levels(self, predicate):
6110  """Retrieve number of levels used for predicate in PDR engine"""
6111  return Z3_fixedpoint_get_num_levels(self.ctx.ref(), self.fixedpoint, predicate.ast)
def get_rules (   self)
retrieve rules that have been added to fixedpoint context

Definition at line 6145 of file z3py.py.

6146  def get_rules(self):
6147  """retrieve rules that have been added to fixedpoint context"""
6148  return AstVector(Z3_fixedpoint_get_rules(self.ctx.ref(), self.fixedpoint), self.ctx)
def help (   self)
Display a string describing all available options.

Definition at line 5999 of file z3py.py.

Referenced by Fixedpoint.set().

6000  def help(self):
6001  """Display a string describing all available options."""
6002  print Z3_fixedpoint_get_help(self.ctx.ref(), self.fixedpoint)
def insert (   self,
  args 
)
Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.

Definition at line 6029 of file z3py.py.

6030  def insert(self, *args):
6031  """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
6032  self.assert_exprs(*args)
def param_descrs (   self)
Return the parameter description set.

Definition at line 6003 of file z3py.py.

6004  def param_descrs(self):
6005  """Return the parameter description set."""
6006  return ParamDescrsRef(Z3_fixedpoint_get_param_descrs(self.ctx.ref(), self.fixedpoint), self.ctx)
def parse_file (   self,
  f 
)
Parse rules and queries from a file

Definition at line 6141 of file z3py.py.

6142  def parse_file(self, f):
6143  """Parse rules and queries from a file"""
6144  return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx)
def parse_string (   self,
  s 
)
Parse rules and queries from a string

Definition at line 6137 of file z3py.py.

6138  def parse_string(self, s):
6139  """Parse rules and queries from a string"""
6140  return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx)
def pop (   self)
restore to previously created backtracking point

Definition at line 6090 of file z3py.py.

6091  def pop(self):
6092  """restore to previously created backtracking point"""
6093  Z3_fixedpoint_pop(self.ctx.ref(), self.fixedpoint)
def push (   self)
create a backtracking point for added rules, facts and assertions

Definition at line 6086 of file z3py.py.

6087  def push(self):
6088  """create a backtracking point for added rules, facts and assertions"""
6089  Z3_fixedpoint_push(self.ctx.ref(), self.fixedpoint)
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 6064 of file z3py.py.

6065  def query(self, *query):
6066  """Query the fixedpoint engine whether formula is derivable.
6067  You can also pass an tuple or list of recursive predicates.
6068  """
6069  query = _get_args(query)
6070  sz = len(query)
6071  if sz >= 1 and isinstance(query[0], FuncDecl):
6072  _decls = (FuncDecl * sz)()
6073  i = 0
6074  for q in query:
6075  _decls[i] = q.ast
6076  i = i + 1
6077  r = Z3_fixedpoint_query_relations(self.ctx.ref(), self.fixedpoint, sz, _decls)
6078  else:
6079  if sz == 1:
6080  query = query[0]
6081  else:
6082  query = And(query)
6083  query = self.abstract(query, False)
6084  r = Z3_fixedpoint_query(self.ctx.ref(), self.fixedpoint, query.as_ast())
6085  return CheckSatResult(r)
def reason_unknown (   self)
Return a string describing why the last `query()` returned `unknown`.

Definition at line 6175 of file z3py.py.

6176  def reason_unknown(self):
6177  """Return a string describing why the last `query()` returned `unknown`.
6178  """
6179  return Z3_fixedpoint_get_reason_unknown(self.ctx.ref(), self.fixedpoint)
def register_relation (   self,
  relations 
)
Register relation as recursive

Definition at line 6121 of file z3py.py.

6122  def register_relation(self, *relations):
6123  """Register relation as recursive"""
6124  relations = _get_args(relations)
6125  for f in relations:
6126  Z3_fixedpoint_register_relation(self.ctx.ref(), self.fixedpoint, f.ast)
def rule (   self,
  head,
  body = None,
  name = None 
)
Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule.

Definition at line 6056 of file z3py.py.

6057  def rule(self, head, body = None, name = None):
6058  """Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
6059  self.add_rule(head, body, name)
def set (   self,
  args,
  keys 
)
Set a configuration option. The method `help()` return a string containing all available options.        

Definition at line 5993 of file z3py.py.

5994  def set(self, *args, **keys):
5995  """Set a configuration option. The method `help()` return a string containing all available options.
5996  """
5997  p = args2params(args, keys, self.ctx)
5998  Z3_fixedpoint_set_params(self.ctx.ref(), self.fixedpoint, p.params)
def set_predicate_representation (   self,
  f,
  representations 
)
Control how relation is represented

Definition at line 6127 of file z3py.py.

6128  def set_predicate_representation(self, f, *representations):
6129  """Control how relation is represented"""
6130  representations = _get_args(representations)
6131  representations = map(to_symbol, representations)
6132  sz = len(representations)
6133  args = (Symbol * sz)()
6134  for i in range(sz):
6135  args[i] = representations[i]
6136  Z3_fixedpoint_set_predicate_representation(self.ctx.ref(), self.fixedpoint, f.ast, sz, args)
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 6157 of file z3py.py.

6158  def sexpr(self):
6159  """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
6160  """
6161  return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, 0, (Ast * 0)())
def statistics (   self)
Return statistics for the last `query()`.

Definition at line 6170 of file z3py.py.

6171  def statistics(self):
6172  """Return statistics for the last `query()`.
6173  """
6174  return Statistics(Z3_fixedpoint_get_statistics(self.ctx.ref(), self.fixedpoint), self.ctx)
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 6162 of file z3py.py.

6163  def to_string(self, queries):
6164  """Return a formatted string (in Lisp-like format) with all added constraints.
6165  We say the string is in s-expression format.
6166  Include also queries.
6167  """
6168  args, len = _to_ast_array(queries)
6169  return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, len, args)
def update_rule (   self,
  head,
  body,
  name 
)
update rule

Definition at line 6094 of file z3py.py.

6095  def update_rule(self, head, body, name):
6096  """update rule"""
6097  if name == None:
6098  name = ""
6099  name = to_symbol(name, self.ctx)
6100  body = _get_args(body)
6101  f = self.abstract(Implies(And(body),head))
6102  Z3_fixedpoint_update_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)

Field Documentation

ctx

Definition at line 5980 of file z3py.py.

Referenced by Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), Probe.__ne__(), Fixedpoint.add_rule(), Tactic.apply(), ApplyResult.as_expr(), Fixedpoint.assert_exprs(), ApplyResult.convert_model(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_rules(), Fixedpoint.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Fixedpoint.set(), Tactic.solver(), and Fixedpoint.statistics().

fixedpoint

Definition at line 5981 of file z3py.py.

Referenced by Fixedpoint.__del__(), Fixedpoint.add_cover(), Fixedpoint.add_rule(), Fixedpoint.assert_exprs(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_num_levels(), Fixedpoint.get_rules(), Fixedpoint.help(), Fixedpoint.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Fixedpoint.pop(), Fixedpoint.push(), Fixedpoint.query(), Fixedpoint.reason_unknown(), Fixedpoint.register_relation(), Fixedpoint.set(), Fixedpoint.set_predicate_representation(), Fixedpoint.sexpr(), Fixedpoint.statistics(), and Fixedpoint.to_string().

vars

Definition at line 5987 of file z3py.py.

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