Z3
Public Member Functions | Data Fields
Fixedpoint Class Reference

Fixedpoint. More...

+ Inheritance diagram for Fixedpoint:

Public Member Functions

def __init__
 
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 append (self, args)
 
def insert (self, args)
 
def add_rule
 
def rule
 
def fact
 
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
 
- 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 6114 of file z3py.py.

Constructor & Destructor Documentation

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

Definition at line 6117 of file z3py.py.

6117  def __init__(self, fixedpoint=None, ctx=None):
6118  assert fixedpoint == None or ctx != None
6119  self.ctx = _get_ctx(ctx)
6120  self.fixedpoint = None
6121  if fixedpoint == None:
6122  self.fixedpoint = Z3_mk_fixedpoint(self.ctx.ref())
6123  else:
6124  self.fixedpoint = fixedpoint
6125  Z3_fixedpoint_inc_ref(self.ctx.ref(), self.fixedpoint)
6126  self.vars = []
6127 
def __init__
Definition: z3py.py:6117
void Z3_API Z3_fixedpoint_inc_ref(__in Z3_context c, __in Z3_fixedpoint d)
Increment the reference counter of the given fixedpoint context.
Z3_fixedpoint Z3_API Z3_mk_fixedpoint(__in Z3_context c)
Create a new fixedpoint context.
def __del__ (   self)

Definition at line 6128 of file z3py.py.

6128  def __del__(self):
6129  if self.fixedpoint != None:
6130  Z3_fixedpoint_dec_ref(self.ctx.ref(), self.fixedpoint)
6131 
void Z3_API Z3_fixedpoint_dec_ref(__in Z3_context c, __in Z3_fixedpoint d)
Decrement the reference counter of the given fixedpoint context.
def __del__(self)
Definition: z3py.py:6128

Member Function Documentation

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

Definition at line 6292 of file z3py.py.

6292  def __repr__(self):
6293  """Return a formatted string with all added rules and constraints."""
6294  return self.sexpr()
6295 
def __repr__(self)
Definition: z3py.py:6292
def sexpr(self)
Definition: z3py.py:6296
def abstract (   self,
  fml,
  is_forall = True 
)

Definition at line 6328 of file z3py.py.

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

6328  def abstract(self, fml, is_forall=True):
6329  if self.vars == []:
6330  return fml
6331  if is_forall:
6332  return ForAll(self.vars, fml)
6333  else:
6334  return Exists(self.vars, fml)
6335 
def Exists
Definition: z3py.py:1819
def ForAll
Definition: z3py.py:1800
def abstract
Definition: z3py.py:6328
def add (   self,
  args 
)
Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.

Definition at line 6160 of file z3py.py.

6160  def add(self, *args):
6161  """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
6162  self.assert_exprs(*args)
6163 
def assert_exprs(self, args)
Definition: z3py.py:6146
def add(self, args)
Definition: z3py.py:6160
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 6256 of file z3py.py.

6256  def add_cover(self, level, predicate, property):
6257  """Add property to predicate for the level'th unfolding. -1 is treated as infinity (infinity)"""
6258  Z3_fixedpoint_add_cover(self.ctx.ref(), self.fixedpoint, level, predicate.ast, property.ast)
6259 
void Z3_API Z3_fixedpoint_add_cover(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred, Z3_ast property)
Add property about the predicate pred. Add a property of predicate pred at level. It gets pushed forw...
def add_cover(self, level, predicate, property)
Definition: z3py.py:6256
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 6172 of file z3py.py.

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

6172  def add_rule(self, head, body = None, name = None):
6173  """Assert rules defining recursive predicates to the fixedpoint solver.
6174  >>> a = Bool('a')
6175  >>> b = Bool('b')
6176  >>> s = Fixedpoint()
6177  >>> s.register_relation(a.decl())
6178  >>> s.register_relation(b.decl())
6179  >>> s.fact(a)
6180  >>> s.rule(b, a)
6181  >>> s.query(b)
6182  sat
6183  """
6184  if name == None:
6185  name = ""
6186  name = to_symbol(name, self.ctx)
6187  if body == None:
6188  head = self.abstract(head)
6189  Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, head.as_ast(), name)
6190  else:
6191  body = _get_args(body)
6192  f = self.abstract(Implies(And(body, self.ctx),head))
6193  Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
6194 
def Implies
Definition: z3py.py:1424
def And(args)
Definition: z3py.py:1479
def abstract
Definition: z3py.py:6328
void Z3_API Z3_fixedpoint_add_rule(__in Z3_context c, __in Z3_fixedpoint d, __in Z3_ast rule, __in Z3_symbol name)
Add a universal Horn clause as a named rule. The horn_rule should be of the form: ...
def add_rule
Definition: z3py.py:6172
def to_symbol
Definition: z3py.py:94
def append (   self,
  args 
)
Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.

Definition at line 6164 of file z3py.py.

6164  def append(self, *args):
6165  """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
6166  self.assert_exprs(*args)
6167 
def assert_exprs(self, args)
Definition: z3py.py:6146
def append(self, args)
Definition: z3py.py:6164
def assert_exprs (   self,
  args 
)
Assert constraints as background axioms for the fixedpoint solver.

Definition at line 6146 of file z3py.py.

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

6146  def assert_exprs(self, *args):
6147  """Assert constraints as background axioms for the fixedpoint solver."""
6148  args = _get_args(args)
6149  s = BoolSort(self.ctx)
6150  for arg in args:
6151  if isinstance(arg, Goal) or isinstance(arg, AstVector):
6152  for f in arg:
6153  f = self.abstract(f)
6154  Z3_fixedpoint_assert(self.ctx.ref(), self.fixedpoint, f.as_ast())
6155  else:
6156  arg = s.cast(arg)
6157  arg = self.abstract(arg)
6158  Z3_fixedpoint_assert(self.ctx.ref(), self.fixedpoint, arg.as_ast())
6159 
void Z3_API Z3_fixedpoint_assert(__in Z3_context c, __in Z3_fixedpoint d, __in Z3_ast axiom)
Assert a constraint to the fixedpoint context.
def BoolSort
Definition: z3py.py:1336
def assert_exprs(self, args)
Definition: z3py.py:6146
def abstract
Definition: z3py.py:6328
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 6319 of file z3py.py.

6319  def declare_var(self, *vars):
6320  """Add variable or several variables.
6321  The added variable or variables will be bound in the rules
6322  and queries
6323  """
6324  vars = _get_args(vars)
6325  for v in vars:
6326  self.vars += [v]
6327 
def declare_var(self, vars)
Definition: z3py.py:6319
def fact (   self,
  head,
  name = None 
)
Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule.

Definition at line 6199 of file z3py.py.

6199  def fact(self, head, name = None):
6200  """Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
6201  self.add_rule(head, None, name)
6202 
def add_rule
Definition: z3py.py:6172
def get_answer (   self)
Retrieve answer from last query call.

Definition at line 6242 of file z3py.py.

6242  def get_answer(self):
6243  """Retrieve answer from last query call."""
6244  r = Z3_fixedpoint_get_answer(self.ctx.ref(), self.fixedpoint)
6245  return _to_expr_ref(r, self.ctx)
6246 
def get_answer(self)
Definition: z3py.py:6242
Z3_ast Z3_API Z3_fixedpoint_get_answer(__in Z3_context c, __in Z3_fixedpoint d)
Retrieve a formula that encodes satisfying answers to the query.
def get_assertions (   self)
retrieve assertions that have been added to fixedpoint context

Definition at line 6288 of file z3py.py.

6288  def get_assertions(self):
6289  """retrieve assertions that have been added to fixedpoint context"""
6290  return AstVector(Z3_fixedpoint_get_assertions(self.ctx.ref(), self.fixedpoint), self.ctx)
6291 
Z3_ast_vector Z3_API Z3_fixedpoint_get_assertions(__in Z3_context c, __in Z3_fixedpoint f)
Retrieve set of background assertions from fixedpoint context.
def get_assertions(self)
Definition: z3py.py:6288
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 6251 of file z3py.py.

6251  def get_cover_delta(self, level, predicate):
6252  """Retrieve properties known about predicate for the level'th unfolding. -1 is treated as the limit (infinity)"""
6253  r = Z3_fixedpoint_get_cover_delta(self.ctx.ref(), self.fixedpoint, level, predicate.ast)
6254  return _to_expr_ref(r, self.ctx)
6255 
def get_cover_delta(self, level, predicate)
Definition: z3py.py:6251
Z3_ast Z3_API Z3_fixedpoint_get_cover_delta(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred)
def get_num_levels (   self,
  predicate 
)
Retrieve number of levels used for predicate in PDR engine

Definition at line 6247 of file z3py.py.

6247  def get_num_levels(self, predicate):
6248  """Retrieve number of levels used for predicate in PDR engine"""
6249  return Z3_fixedpoint_get_num_levels(self.ctx.ref(), self.fixedpoint, predicate.ast)
6250 
unsigned Z3_API Z3_fixedpoint_get_num_levels(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred)
Query the PDR engine for the maximal levels properties are known about predicate. ...
def get_num_levels(self, predicate)
Definition: z3py.py:6247
def get_rules (   self)
retrieve rules that have been added to fixedpoint context

Definition at line 6284 of file z3py.py.

6284  def get_rules(self):
6285  """retrieve rules that have been added to fixedpoint context"""
6286  return AstVector(Z3_fixedpoint_get_rules(self.ctx.ref(), self.fixedpoint), self.ctx)
6287 
def get_rules(self)
Definition: z3py.py:6284
Z3_ast_vector Z3_API Z3_fixedpoint_get_rules(__in Z3_context c, __in Z3_fixedpoint f)
Retrieve set of rules from fixedpoint context.
def help (   self)
Display a string describing all available options.

Definition at line 6138 of file z3py.py.

6138  def help(self):
6139  """Display a string describing all available options."""
6140  print(Z3_fixedpoint_get_help(self.ctx.ref(), self.fixedpoint))
6141 
Z3_string Z3_API Z3_fixedpoint_get_help(__in Z3_context c, __in Z3_fixedpoint f)
Return a string describing all fixedpoint available parameters.
def help(self)
Definition: z3py.py:6138
def insert (   self,
  args 
)
Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.

Definition at line 6168 of file z3py.py.

6168  def insert(self, *args):
6169  """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
6170  self.assert_exprs(*args)
6171 
def assert_exprs(self, args)
Definition: z3py.py:6146
def insert(self, args)
Definition: z3py.py:6168
def param_descrs (   self)
Return the parameter description set.

Definition at line 6142 of file z3py.py.

6142  def param_descrs(self):
6143  """Return the parameter description set."""
6144  return ParamDescrsRef(Z3_fixedpoint_get_param_descrs(self.ctx.ref(), self.fixedpoint), self.ctx)
6145 
def param_descrs(self)
Definition: z3py.py:6142
Z3_param_descrs Z3_API Z3_fixedpoint_get_param_descrs(__in Z3_context c, __in Z3_fixedpoint f)
Return the parameter description set for the given fixedpoint object.
def parse_file (   self,
  f 
)
Parse rules and queries from a file

Definition at line 6280 of file z3py.py.

6280  def parse_file(self, f):
6281  """Parse rules and queries from a file"""
6282  return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx)
6283 
Z3_ast_vector Z3_API Z3_fixedpoint_from_file(__in Z3_context c, __in Z3_fixedpoint f, __in Z3_string s)
Parse an SMT-LIB2 file with fixedpoint rules. Add the rules to the current fixedpoint context...
def parse_file(self, f)
Definition: z3py.py:6280
def parse_string (   self,
  s 
)
Parse rules and queries from a string

Definition at line 6276 of file z3py.py.

6276  def parse_string(self, s):
6277  """Parse rules and queries from a string"""
6278  return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx)
6279 
Z3_ast_vector Z3_API Z3_fixedpoint_from_string(__in Z3_context c, __in Z3_fixedpoint f, __in Z3_string s)
Parse an SMT-LIB2 string with fixedpoint rules. Add the rules to the current fixedpoint context...
def parse_string(self, s)
Definition: z3py.py:6276
def pop (   self)
restore to previously created backtracking point

Definition at line 6229 of file z3py.py.

6229  def pop(self):
6230  """restore to previously created backtracking point"""
6231  Z3_fixedpoint_pop(self.ctx.ref(), self.fixedpoint)
6232 
void Z3_API Z3_fixedpoint_pop(Z3_context c, Z3_fixedpoint d)
Backtrack one backtracking point.
def pop(self)
Definition: z3py.py:6229
def push (   self)
create a backtracking point for added rules, facts and assertions

Definition at line 6225 of file z3py.py.

6225  def push(self):
6226  """create a backtracking point for added rules, facts and assertions"""
6227  Z3_fixedpoint_push(self.ctx.ref(), self.fixedpoint)
6228 
def push(self)
Definition: z3py.py:6225
void Z3_API Z3_fixedpoint_push(Z3_context c, Z3_fixedpoint d)
Create a backtracking point.
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 6203 of file z3py.py.

6203  def query(self, *query):
6204  """Query the fixedpoint engine whether formula is derivable.
6205  You can also pass an tuple or list of recursive predicates.
6206  """
6207  query = _get_args(query)
6208  sz = len(query)
6209  if sz >= 1 and isinstance(query[0], FuncDeclRef):
6210  _decls = (FuncDecl * sz)()
6211  i = 0
6212  for q in query:
6213  _decls[i] = q.ast
6214  i = i + 1
6215  r = Z3_fixedpoint_query_relations(self.ctx.ref(), self.fixedpoint, sz, _decls)
6216  else:
6217  if sz == 1:
6218  query = query[0]
6219  else:
6220  query = And(query, self.ctx)
6221  query = self.abstract(query, False)
6222  r = Z3_fixedpoint_query(self.ctx.ref(), self.fixedpoint, query.as_ast())
6223  return CheckSatResult(r)
6224 
def And(args)
Definition: z3py.py:1479
Z3_lbool Z3_API Z3_fixedpoint_query(__in Z3_context c, __in Z3_fixedpoint d, __in Z3_ast query)
Pose a query against the asserted rules.
Z3_lbool Z3_API Z3_fixedpoint_query_relations(__in Z3_context c, __in Z3_fixedpoint d, __in unsigned num_relations, __in_ecount(num_relations) Z3_func_decl const relations[])
Pose multiple queries against the asserted rules.
def abstract
Definition: z3py.py:6328
def query(self, query)
Definition: z3py.py:6203
def reason_unknown (   self)
Return a string describing why the last `query()` returned `unknown`.

Definition at line 6314 of file z3py.py.

6314  def reason_unknown(self):
6315  """Return a string describing why the last `query()` returned `unknown`.
6316  """
6317  return Z3_fixedpoint_get_reason_unknown(self.ctx.ref(), self.fixedpoint)
6318 
Z3_string Z3_API Z3_fixedpoint_get_reason_unknown(__in Z3_context c, __in Z3_fixedpoint d)
Retrieve a string that describes the last status returned by Z3_fixedpoint_query. ...
def reason_unknown(self)
Definition: z3py.py:6314
def register_relation (   self,
  relations 
)
Register relation as recursive

Definition at line 6260 of file z3py.py.

6260  def register_relation(self, *relations):
6261  """Register relation as recursive"""
6262  relations = _get_args(relations)
6263  for f in relations:
6264  Z3_fixedpoint_register_relation(self.ctx.ref(), self.fixedpoint, f.ast)
6265 
def register_relation(self, relations)
Definition: z3py.py:6260
void Z3_API Z3_fixedpoint_register_relation(__in Z3_context c, __in Z3_fixedpoint d, __in Z3_func_decl f)
Register relation as Fixedpoint defined. Fixedpoint defined relations have least-fixedpoint semantics...
def rule (   self,
  head,
  body = None,
  name = None 
)
Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule.

Definition at line 6195 of file z3py.py.

6195  def rule(self, head, body = None, name = None):
6196  """Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
6197  self.add_rule(head, body, name)
6198 
def add_rule
Definition: z3py.py:6172
def set (   self,
  args,
  keys 
)
Set a configuration option. The method `help()` return a string containing all available options.        

Definition at line 6132 of file z3py.py.

6132  def set(self, *args, **keys):
6133  """Set a configuration option. The method `help()` return a string containing all available options.
6134  """
6135  p = args2params(args, keys, self.ctx)
6136  Z3_fixedpoint_set_params(self.ctx.ref(), self.fixedpoint, p.params)
6137 
def args2params
Definition: z3py.py:4490
def set(self, args, keys)
Definition: z3py.py:6132
void Z3_API Z3_fixedpoint_set_params(__in Z3_context c, __in Z3_fixedpoint f, __in Z3_params p)
Set parameters on fixedpoint context.
def set_predicate_representation (   self,
  f,
  representations 
)
Control how relation is represented

Definition at line 6266 of file z3py.py.

6266  def set_predicate_representation(self, f, *representations):
6267  """Control how relation is represented"""
6268  representations = _get_args(representations)
6269  representations = [to_symbol(s) for s in representations]
6270  sz = len(representations)
6271  args = (Symbol * sz)()
6272  for i in range(sz):
6273  args[i] = representations[i]
6274  Z3_fixedpoint_set_predicate_representation(self.ctx.ref(), self.fixedpoint, f.ast, sz, args)
6275 
def set_predicate_representation(self, f, representations)
Definition: z3py.py:6266
void Z3_API Z3_fixedpoint_set_predicate_representation(__in Z3_context c, __in Z3_fixedpoint d, __in Z3_func_decl f, __in unsigned num_relations, __in_ecount(num_relations) Z3_symbol const relation_kinds[])
Configure the predicate representation.
def to_symbol
Definition: z3py.py:94
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 6296 of file z3py.py.

Referenced by Fixedpoint.__repr__().

6296  def sexpr(self):
6297  """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
6298  """
6299  return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, 0, (Ast * 0)())
6300 
Z3_string Z3_API Z3_fixedpoint_to_string(__in Z3_context c, __in Z3_fixedpoint f, __in unsigned num_queries, __in_ecount(num_queries) Z3_ast queries[])
Print the current rules and background axioms as a string.
def sexpr(self)
Definition: z3py.py:6296
def statistics (   self)
Return statistics for the last `query()`.

Definition at line 6309 of file z3py.py.

6309  def statistics(self):
6310  """Return statistics for the last `query()`.
6311  """
6312  return Statistics(Z3_fixedpoint_get_statistics(self.ctx.ref(), self.fixedpoint), self.ctx)
6313 
Statistics.
Definition: z3py.py:5567
Z3_stats Z3_API Z3_fixedpoint_get_statistics(__in Z3_context c, __in Z3_fixedpoint d)
Retrieve statistics information from the last call to Z3_fixedpoint_query.
def statistics(self)
Definition: z3py.py:6309
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 6301 of file z3py.py.

6301  def to_string(self, queries):
6302  """Return a formatted string (in Lisp-like format) with all added constraints.
6303  We say the string is in s-expression format.
6304  Include also queries.
6305  """
6306  args, len = _to_ast_array(queries)
6307  return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, len, args)
6308 
Z3_string Z3_API Z3_fixedpoint_to_string(__in Z3_context c, __in Z3_fixedpoint f, __in unsigned num_queries, __in_ecount(num_queries) Z3_ast queries[])
Print the current rules and background axioms as a string.
def to_string(self, queries)
Definition: z3py.py:6301
def update_rule (   self,
  head,
  body,
  name 
)
update rule

Definition at line 6233 of file z3py.py.

6233  def update_rule(self, head, body, name):
6234  """update rule"""
6235  if name == None:
6236  name = ""
6237  name = to_symbol(name, self.ctx)
6238  body = _get_args(body)
6239  f = self.abstract(Implies(And(body, self.ctx),head))
6240  Z3_fixedpoint_update_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
6241 
def update_rule(self, head, body, name)
Definition: z3py.py:6233
void Z3_API Z3_fixedpoint_update_rule(__in Z3_context c, __in Z3_fixedpoint d, __in Z3_ast a, __in Z3_symbol name)
Update a named rule. A rule with the same name must have been previously created. ...
def Implies
Definition: z3py.py:1424
def And(args)
Definition: z3py.py:1479
def abstract
Definition: z3py.py:6328
def to_symbol
Definition: z3py.py:94

Field Documentation

ctx
fixedpoint
vars

Definition at line 6126 of file z3py.py.

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