Z3
Public Member Functions | Data Fields
Fixedpoint Class Reference

Fixedpoint. More...

+ Inheritance diagram for Fixedpoint:

Public Member Functions

def __init__
 
def __deepcopy__
 
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
 
def rule
 
def fact
 
def query (self, query)
 
def query_from_lvl (self, lvl, query)
 
def update_rule (self, head, body, name)
 
def get_answer (self)
 
def get_ground_sat_answer (self)
 
def get_rules_along_trace (self)
 
def get_rule_names_along_trace (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 7498 of file z3py.py.

Constructor & Destructor Documentation

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

Definition at line 7501 of file z3py.py.

7501  def __init__(self, fixedpoint=None, ctx=None):
7502  assert fixedpoint is None or ctx is not None
7503  self.ctx = _get_ctx(ctx)
7504  self.fixedpoint = None
7505  if fixedpoint is None:
7506  self.fixedpoint = Z3_mk_fixedpoint(self.ctx.ref())
7507  else:
7508  self.fixedpoint = fixedpoint
7509  Z3_fixedpoint_inc_ref(self.ctx.ref(), self.fixedpoint)
7510  self.vars = []
7511 
Z3_fixedpoint Z3_API Z3_mk_fixedpoint(Z3_context c)
Create a new fixedpoint context.
def __init__
Definition: z3py.py:7501
void Z3_API Z3_fixedpoint_inc_ref(Z3_context c, Z3_fixedpoint d)
Increment the reference counter of the given fixedpoint context.
def __del__ (   self)

Definition at line 7515 of file z3py.py.

7515  def __del__(self):
7516  if self.fixedpoint is not None and self.ctx.ref() is not None and Z3_fixedpoint_dec_ref is not None:
7517  Z3_fixedpoint_dec_ref(self.ctx.ref(), self.fixedpoint)
7518 
void Z3_API Z3_fixedpoint_dec_ref(Z3_context c, Z3_fixedpoint d)
Decrement the reference counter of the given fixedpoint context.
def __del__(self)
Definition: z3py.py:7515

Member Function Documentation

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 7512 of file z3py.py.

7512  def __deepcopy__(self, memo={}):
7513  return FixedPoint(self.fixedpoint, self.ctx)
7514 
def __deepcopy__
Definition: z3py.py:7512
def __iadd__ (   self,
  fml 
)

Definition at line 7551 of file z3py.py.

7551  def __iadd__(self, fml):
7552  self.add(fml)
7553  return self
7554 
def add(self, args)
Definition: z3py.py:7547
def __iadd__(self, fml)
Definition: z3py.py:7551
def __repr__ (   self)
Return a formatted string with all added rules and constraints.

Definition at line 7712 of file z3py.py.

7712  def __repr__(self):
7713  """Return a formatted string with all added rules and constraints."""
7714  return self.sexpr()
7715 
def __repr__(self)
Definition: z3py.py:7712
def sexpr(self)
Definition: z3py.py:7716
def abstract (   self,
  fml,
  is_forall = True 
)

Definition at line 7749 of file z3py.py.

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

7749  def abstract(self, fml, is_forall=True):
7750  if self.vars == []:
7751  return fml
7752  if is_forall:
7753  return ForAll(self.vars, fml)
7754  else:
7755  return Exists(self.vars, fml)
7756 
7757 
def Exists
Definition: z3py.py:2290
def ForAll
Definition: z3py.py:2272
def abstract
Definition: z3py.py:7749
def add (   self,
  args 
)
Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.

Definition at line 7547 of file z3py.py.

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

7547  def add(self, *args):
7548  """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
7549  self.assert_exprs(*args)
7550 
def assert_exprs(self, args)
Definition: z3py.py:7533
def add(self, args)
Definition: z3py.py:7547
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 7674 of file z3py.py.

7674  def add_cover(self, level, predicate, property):
7675  """Add property to predicate for the level'th unfolding.
7676  -1 is treated as infinity (infinity)
7677  """
7678  Z3_fixedpoint_add_cover(self.ctx.ref(), self.fixedpoint, level, predicate.ast, property.ast)
7679 
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:7674
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 7563 of file z3py.py.

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

7563  def add_rule(self, head, body=None, name=None):
7564  """Assert rules defining recursive predicates to the fixedpoint solver.
7565  >>> a = Bool('a')
7566  >>> b = Bool('b')
7567  >>> s = Fixedpoint()
7568  >>> s.register_relation(a.decl())
7569  >>> s.register_relation(b.decl())
7570  >>> s.fact(a)
7571  >>> s.rule(b, a)
7572  >>> s.query(b)
7573  sat
7574  """
7575  if name is None:
7576  name = ""
7577  name = to_symbol(name, self.ctx)
7578  if body is None:
7579  head = self.abstract(head)
7580  Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, head.as_ast(), name)
7581  else:
7582  body = _get_args(body)
7583  f = self.abstract(Implies(And(body, self.ctx), head))
7584  Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
7585 
void Z3_API Z3_fixedpoint_add_rule(Z3_context c, Z3_fixedpoint d, Z3_ast rule, Z3_symbol name)
Add a universal Horn clause as a named rule. The horn_rule should be of the form: ...
def Implies
Definition: z3py.py:1825
def And(args)
Definition: z3py.py:1889
def abstract
Definition: z3py.py:7749
def add_rule
Definition: z3py.py:7563
def to_symbol
Definition: z3py.py:124
def append (   self,
  args 
)
Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.

Definition at line 7555 of file z3py.py.

7555  def append(self, *args):
7556  """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
7557  self.assert_exprs(*args)
7558 
def assert_exprs(self, args)
Definition: z3py.py:7533
def append(self, args)
Definition: z3py.py:7555
def assert_exprs (   self,
  args 
)
Assert constraints as background axioms for the fixedpoint solver.

Definition at line 7533 of file z3py.py.

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

7533  def assert_exprs(self, *args):
7534  """Assert constraints as background axioms for the fixedpoint solver."""
7535  args = _get_args(args)
7536  s = BoolSort(self.ctx)
7537  for arg in args:
7538  if isinstance(arg, Goal) or isinstance(arg, AstVector):
7539  for f in arg:
7540  f = self.abstract(f)
7541  Z3_fixedpoint_assert(self.ctx.ref(), self.fixedpoint, f.as_ast())
7542  else:
7543  arg = s.cast(arg)
7544  arg = self.abstract(arg)
7545  Z3_fixedpoint_assert(self.ctx.ref(), self.fixedpoint, arg.as_ast())
7546 
def BoolSort
Definition: z3py.py:1731
def assert_exprs(self, args)
Definition: z3py.py:7533
void Z3_API Z3_fixedpoint_assert(Z3_context c, Z3_fixedpoint d, Z3_ast axiom)
Assert a constraint to the fixedpoint context.
def abstract
Definition: z3py.py:7749
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 7740 of file z3py.py.

7740  def declare_var(self, *vars):
7741  """Add variable or several variables.
7742  The added variable or variables will be bound in the rules
7743  and queries
7744  """
7745  vars = _get_args(vars)
7746  for v in vars:
7747  self.vars += [v]
7748 
def declare_var(self, vars)
Definition: z3py.py:7740
def fact (   self,
  head,
  name = None 
)
Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule.

Definition at line 7590 of file z3py.py.

7590  def fact(self, head, name=None):
7591  """Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
7592  self.add_rule(head, None, name)
7593 
def add_rule
Definition: z3py.py:7563
def get_answer (   self)
Retrieve answer from last query call.

Definition at line 7641 of file z3py.py.

7641  def get_answer(self):
7642  """Retrieve answer from last query call."""
7643  r = Z3_fixedpoint_get_answer(self.ctx.ref(), self.fixedpoint)
7644  return _to_expr_ref(r, self.ctx)
7645 
def get_answer(self)
Definition: z3py.py:7641
Z3_ast Z3_API Z3_fixedpoint_get_answer(Z3_context c, 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 7708 of file z3py.py.

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

7667  def get_cover_delta(self, level, predicate):
7668  """Retrieve properties known about predicate for the level'th unfolding.
7669  -1 is treated as the limit (infinity)
7670  """
7671  r = Z3_fixedpoint_get_cover_delta(self.ctx.ref(), self.fixedpoint, level, predicate.ast)
7672  return _to_expr_ref(r, self.ctx)
7673 
def get_cover_delta(self, level, predicate)
Definition: z3py.py:7667
Z3_ast Z3_API Z3_fixedpoint_get_cover_delta(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred)
def get_ground_sat_answer (   self)
Retrieve a ground cex from last query call.

Definition at line 7646 of file z3py.py.

7647  """Retrieve a ground cex from last query call."""
7648  r = Z3_fixedpoint_get_ground_sat_answer(self.ctx.ref(), self.fixedpoint)
7649  return _to_expr_ref(r, self.ctx)
7650 
def get_ground_sat_answer(self)
Definition: z3py.py:7646
def get_num_levels (   self,
  predicate 
)
Retrieve number of levels used for predicate in PDR engine

Definition at line 7663 of file z3py.py.

7663  def get_num_levels(self, predicate):
7664  """Retrieve number of levels used for predicate in PDR engine"""
7665  return Z3_fixedpoint_get_num_levels(self.ctx.ref(), self.fixedpoint, predicate.ast)
7666 
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:7663
def get_rule_names_along_trace (   self)
retrieve rule names along the counterexample trace

Definition at line 7655 of file z3py.py.

7656  """retrieve rule names along the counterexample trace"""
7657  # this is a hack as I don't know how to return a list of symbols from C++;
7658  # obtain names as a single string separated by semicolons
7659  names = _symbol2py(self.ctx, Z3_fixedpoint_get_rule_names_along_trace(self.ctx.ref(), self.fixedpoint))
7660  # split into individual names
7661  return names.split(";")
7662 
def get_rule_names_along_trace(self)
Definition: z3py.py:7655
def get_rules (   self)
retrieve rules that have been added to fixedpoint context

Definition at line 7704 of file z3py.py.

7704  def get_rules(self):
7705  """retrieve rules that have been added to fixedpoint context"""
7706  return AstVector(Z3_fixedpoint_get_rules(self.ctx.ref(), self.fixedpoint), self.ctx)
7707 
def get_rules(self)
Definition: z3py.py:7704
Z3_ast_vector Z3_API Z3_fixedpoint_get_rules(Z3_context c, Z3_fixedpoint f)
Retrieve set of rules from fixedpoint context.
def get_rules_along_trace (   self)
retrieve rules along the counterexample trace

Definition at line 7651 of file z3py.py.

7652  """retrieve rules along the counterexample trace"""
7653  return AstVector(Z3_fixedpoint_get_rules_along_trace(self.ctx.ref(), self.fixedpoint), self.ctx)
7654 
def get_rules_along_trace(self)
Definition: z3py.py:7651
def help (   self)
Display a string describing all available options.

Definition at line 7525 of file z3py.py.

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

Definition at line 7559 of file z3py.py.

7559  def insert(self, *args):
7560  """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
7561  self.assert_exprs(*args)
7562 
def assert_exprs(self, args)
Definition: z3py.py:7533
def insert(self, args)
Definition: z3py.py:7559
def param_descrs (   self)
Return the parameter description set.

Definition at line 7529 of file z3py.py.

7529  def param_descrs(self):
7530  """Return the parameter description set."""
7531  return ParamDescrsRef(Z3_fixedpoint_get_param_descrs(self.ctx.ref(), self.fixedpoint), self.ctx)
7532 
def param_descrs(self)
Definition: z3py.py:7529
Z3_param_descrs Z3_API Z3_fixedpoint_get_param_descrs(Z3_context c, 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 7700 of file z3py.py.

7700  def parse_file(self, f):
7701  """Parse rules and queries from a file"""
7702  return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx)
7703 
Z3_ast_vector Z3_API Z3_fixedpoint_from_file(Z3_context c, Z3_fixedpoint f, 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:7700
def parse_string (   self,
  s 
)
Parse rules and queries from a string

Definition at line 7696 of file z3py.py.

7696  def parse_string(self, s):
7697  """Parse rules and queries from a string"""
7698  return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx)
7699 
Z3_ast_vector Z3_API Z3_fixedpoint_from_string(Z3_context c, Z3_fixedpoint f, 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:7696
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 7594 of file z3py.py.

7594  def query(self, *query):
7595  """Query the fixedpoint engine whether formula is derivable.
7596  You can also pass an tuple or list of recursive predicates.
7597  """
7598  query = _get_args(query)
7599  sz = len(query)
7600  if sz >= 1 and isinstance(query[0], FuncDeclRef):
7601  _decls = (FuncDecl * sz)()
7602  i = 0
7603  for q in query:
7604  _decls[i] = q.ast
7605  i = i + 1
7606  r = Z3_fixedpoint_query_relations(self.ctx.ref(), self.fixedpoint, sz, _decls)
7607  else:
7608  if sz == 1:
7609  query = query[0]
7610  else:
7611  query = And(query, self.ctx)
7612  query = self.abstract(query, False)
7613  r = Z3_fixedpoint_query(self.ctx.ref(), self.fixedpoint, query.as_ast())
7614  return CheckSatResult(r)
7615 
def And(args)
Definition: z3py.py:1889
def abstract
Definition: z3py.py:7749
def query(self, query)
Definition: z3py.py:7594
Z3_lbool Z3_API Z3_fixedpoint_query(Z3_context c, Z3_fixedpoint d, Z3_ast query)
Pose a query against the asserted rules.
Z3_lbool Z3_API Z3_fixedpoint_query_relations(Z3_context c, Z3_fixedpoint d, unsigned num_relations, Z3_func_decl const relations[])
Pose multiple queries against the asserted rules.
def query_from_lvl (   self,
  lvl,
  query 
)
Query the fixedpoint engine whether formula is derivable starting at the given query level.

Definition at line 7616 of file z3py.py.

7616  def query_from_lvl(self, lvl, *query):
7617  """Query the fixedpoint engine whether formula is derivable starting at the given query level.
7618  """
7619  query = _get_args(query)
7620  sz = len(query)
7621  if sz >= 1 and isinstance(query[0], FuncDecl):
7622  _z3_assert(False, "unsupported")
7623  else:
7624  if sz == 1:
7625  query = query[0]
7626  else:
7627  query = And(query)
7628  query = self.abstract(query, False)
7629  r = Z3_fixedpoint_query_from_lvl(self.ctx.ref(), self.fixedpoint, query.as_ast(), lvl)
7630  return CheckSatResult(r)
7631 
def And(args)
Definition: z3py.py:1889
def abstract
Definition: z3py.py:7749
def query_from_lvl(self, lvl, query)
Definition: z3py.py:7616
def reason_unknown (   self)
Return a string describing why the last `query()` returned `unknown`.

Definition at line 7735 of file z3py.py.

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

Definition at line 7680 of file z3py.py.

7680  def register_relation(self, *relations):
7681  """Register relation as recursive"""
7682  relations = _get_args(relations)
7683  for f in relations:
7684  Z3_fixedpoint_register_relation(self.ctx.ref(), self.fixedpoint, f.ast)
7685 
def register_relation(self, relations)
Definition: z3py.py:7680
void Z3_API Z3_fixedpoint_register_relation(Z3_context c, Z3_fixedpoint d, 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 7586 of file z3py.py.

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

Definition at line 7519 of file z3py.py.

7519  def set(self, *args, **keys):
7520  """Set a configuration option. The method `help()` return a string containing all available options.
7521  """
7522  p = args2params(args, keys, self.ctx)
7523  Z3_fixedpoint_set_params(self.ctx.ref(), self.fixedpoint, p.params)
7524 
def args2params
Definition: z3py.py:5512
def set(self, args, keys)
Definition: z3py.py:7519
void Z3_API Z3_fixedpoint_set_params(Z3_context c, Z3_fixedpoint f, Z3_params p)
Set parameters on fixedpoint context.
def set_predicate_representation (   self,
  f,
  representations 
)
Control how relation is represented

Definition at line 7686 of file z3py.py.

7686  def set_predicate_representation(self, f, *representations):
7687  """Control how relation is represented"""
7688  representations = _get_args(representations)
7689  representations = [to_symbol(s) for s in representations]
7690  sz = len(representations)
7691  args = (Symbol * sz)()
7692  for i in range(sz):
7693  args[i] = representations[i]
7694  Z3_fixedpoint_set_predicate_representation(self.ctx.ref(), self.fixedpoint, f.ast, sz, args)
7695 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:4085
def set_predicate_representation(self, f, representations)
Definition: z3py.py:7686
def to_symbol
Definition: z3py.py:124
void Z3_API Z3_fixedpoint_set_predicate_representation(Z3_context c, Z3_fixedpoint d, Z3_func_decl f, unsigned num_relations, Z3_symbol const relation_kinds[])
Configure the predicate representation.
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 7716 of file z3py.py.

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

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

Definition at line 7730 of file z3py.py.

7730  def statistics(self):
7731  """Return statistics for the last `query()`.
7732  """
7733  return Statistics(Z3_fixedpoint_get_statistics(self.ctx.ref(), self.fixedpoint), self.ctx)
7734 
Z3_stats Z3_API Z3_fixedpoint_get_statistics(Z3_context c, Z3_fixedpoint d)
Retrieve statistics information from the last call to Z3_fixedpoint_query.
Statistics.
Definition: z3py.py:6758
def statistics(self)
Definition: z3py.py:7730
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 7722 of file z3py.py.

7722  def to_string(self, queries):
7723  """Return a formatted string (in Lisp-like format) with all added constraints.
7724  We say the string is in s-expression format.
7725  Include also queries.
7726  """
7727  args, len = _to_ast_array(queries)
7728  return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, len, args)
7729 
def to_string(self, queries)
Definition: z3py.py:7722
Z3_string Z3_API Z3_fixedpoint_to_string(Z3_context c, Z3_fixedpoint f, unsigned num_queries, Z3_ast queries[])
Print the current rules and background axioms as a string.
def update_rule (   self,
  head,
  body,
  name 
)
update rule

Definition at line 7632 of file z3py.py.

7632  def update_rule(self, head, body, name):
7633  """update rule"""
7634  if name is None:
7635  name = ""
7636  name = to_symbol(name, self.ctx)
7637  body = _get_args(body)
7638  f = self.abstract(Implies(And(body, self.ctx), head))
7639  Z3_fixedpoint_update_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
7640 
def update_rule(self, head, body, name)
Definition: z3py.py:7632
def Implies
Definition: z3py.py:1825
def And(args)
Definition: z3py.py:1889
def abstract
Definition: z3py.py:7749
void Z3_API Z3_fixedpoint_update_rule(Z3_context c, Z3_fixedpoint d, Z3_ast a, Z3_symbol name)
Update a named rule. A rule with the same name must have been previously created. ...
def to_symbol
Definition: z3py.py:124

Field Documentation

ctx
fixedpoint
vars

Definition at line 7510 of file z3py.py.

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