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 __deepcopy__ (self, memo={})
 
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 query_from_lvl (self, lvl, query)
 
def push (self)
 
def pop (self)
 
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 (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 6856 of file z3py.py.

Constructor & Destructor Documentation

◆ __init__()

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

Definition at line 6859 of file z3py.py.

6859  def __init__(self, fixedpoint=None, ctx=None):
6860  assert fixedpoint is None or ctx is not None
6861  self.ctx = _get_ctx(ctx)
6862  self.fixedpoint = None
6863  if fixedpoint is None:
6864  self.fixedpoint = Z3_mk_fixedpoint(self.ctx.ref())
6865  else:
6866  self.fixedpoint = fixedpoint
6867  Z3_fixedpoint_inc_ref(self.ctx.ref(), self.fixedpoint)
6868  self.vars = []
6869 
Z3_fixedpoint Z3_API Z3_mk_fixedpoint(Z3_context c)
Create a new fixedpoint context.
void Z3_API Z3_fixedpoint_inc_ref(Z3_context c, Z3_fixedpoint d)
Increment the reference counter of the given fixedpoint context.

◆ __del__()

def __del__ (   self)

Definition at line 6873 of file z3py.py.

6873  def __del__(self):
6874  if self.fixedpoint is not None and self.ctx.ref() is not None:
6875  Z3_fixedpoint_dec_ref(self.ctx.ref(), self.fixedpoint)
6876 
void Z3_API Z3_fixedpoint_dec_ref(Z3_context c, Z3_fixedpoint d)
Decrement the reference counter of the given fixedpoint context.

Member Function Documentation

◆ __deepcopy__()

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 6870 of file z3py.py.

6870  def __deepcopy__(self, memo={}):
6871  return FixedPoint(self.fixedpoint, self.ctx)
6872 

◆ __iadd__()

def __iadd__ (   self,
  fml 
)

Definition at line 6909 of file z3py.py.

6909  def __iadd__(self, fml):
6910  self.add(fml)
6911  return self
6912 

◆ __repr__()

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

Definition at line 7080 of file z3py.py.

7080  def __repr__(self):
7081  """Return a formatted string with all added rules and constraints."""
7082  return self.sexpr()
7083 

◆ abstract()

def abstract (   self,
  fml,
  is_forall = True 
)

Definition at line 7116 of file z3py.py.

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

7116  def abstract(self, fml, is_forall=True):
7117  if self.vars == []:
7118  return fml
7119  if is_forall:
7120  return ForAll(self.vars, fml)
7121  else:
7122  return Exists(self.vars, fml)
7123 
7124 
def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
Definition: z3py.py:2027
def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
Definition: z3py.py:2010

◆ add()

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

Definition at line 6905 of file z3py.py.

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

6905  def add(self, *args):
6906  """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
6907  self.assert_exprs(*args)
6908 

◆ 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 7038 of file z3py.py.

7038  def add_cover(self, level, predicate, property):
7039  """Add property to predicate for the level'th unfolding. -1 is treated as infinity (infinity)"""
7040  Z3_fixedpoint_add_cover(self.ctx.ref(), self.fixedpoint, level, predicate.ast, property.ast)
7041 
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...

◆ 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 6921 of file z3py.py.

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

6921  def add_rule(self, head, body = None, name = None):
6922  """Assert rules defining recursive predicates to the fixedpoint solver.
6923  >>> a = Bool('a')
6924  >>> b = Bool('b')
6925  >>> s = Fixedpoint()
6926  >>> s.register_relation(a.decl())
6927  >>> s.register_relation(b.decl())
6928  >>> s.fact(a)
6929  >>> s.rule(b, a)
6930  >>> s.query(b)
6931  sat
6932  """
6933  if name is None:
6934  name = ""
6935  name = to_symbol(name, self.ctx)
6936  if body is None:
6937  head = self.abstract(head)
6938  Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, head.as_ast(), name)
6939  else:
6940  body = _get_args(body)
6941  f = self.abstract(Implies(And(body, self.ctx),head))
6942  Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
6943 
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 to_symbol(s, ctx=None)
Definition: z3py.py:105
def And(args)
Definition: z3py.py:1655
def Implies(a, b, ctx=None)
Definition: z3py.py:1600

◆ append()

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

Definition at line 6913 of file z3py.py.

6913  def append(self, *args):
6914  """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
6915  self.assert_exprs(*args)
6916 

◆ assert_exprs()

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

Definition at line 6891 of file z3py.py.

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

6891  def assert_exprs(self, *args):
6892  """Assert constraints as background axioms for the fixedpoint solver."""
6893  args = _get_args(args)
6894  s = BoolSort(self.ctx)
6895  for arg in args:
6896  if isinstance(arg, Goal) or isinstance(arg, AstVector):
6897  for f in arg:
6898  f = self.abstract(f)
6899  Z3_fixedpoint_assert(self.ctx.ref(), self.fixedpoint, f.as_ast())
6900  else:
6901  arg = s.cast(arg)
6902  arg = self.abstract(arg)
6903  Z3_fixedpoint_assert(self.ctx.ref(), self.fixedpoint, arg.as_ast())
6904 
void Z3_API Z3_fixedpoint_assert(Z3_context c, Z3_fixedpoint d, Z3_ast axiom)
Assert a constraint to the fixedpoint context.
def BoolSort(ctx=None)
Definition: z3py.py:1512

◆ 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 7107 of file z3py.py.

7107  def declare_var(self, *vars):
7108  """Add variable or several variables.
7109  The added variable or variables will be bound in the rules
7110  and queries
7111  """
7112  vars = _get_args(vars)
7113  for v in vars:
7114  self.vars += [v]
7115 

◆ fact()

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

Definition at line 6948 of file z3py.py.

6948  def fact(self, head, name = None):
6949  """Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
6950  self.add_rule(head, None, name)
6951 

◆ get_answer()

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

Definition at line 7007 of file z3py.py.

7007  def get_answer(self):
7008  """Retrieve answer from last query call."""
7009  r = Z3_fixedpoint_get_answer(self.ctx.ref(), self.fixedpoint)
7010  return _to_expr_ref(r, self.ctx)
7011 
Z3_ast Z3_API Z3_fixedpoint_get_answer(Z3_context c, Z3_fixedpoint d)
Retrieve a formula that encodes satisfying answers to the query.

◆ get_assertions()

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

Definition at line 7076 of file z3py.py.

7076  def get_assertions(self):
7077  """retrieve assertions that have been added to fixedpoint context"""
7078  return AstVector(Z3_fixedpoint_get_assertions(self.ctx.ref(), self.fixedpoint), self.ctx)
7079 
Z3_ast_vector Z3_API Z3_fixedpoint_get_assertions(Z3_context c, Z3_fixedpoint f)
Retrieve set of background assertions from fixedpoint context.

◆ 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 7033 of file z3py.py.

7033  def get_cover_delta(self, level, predicate):
7034  """Retrieve properties known about predicate for the level'th unfolding. -1 is treated as the limit (infinity)"""
7035  r = Z3_fixedpoint_get_cover_delta(self.ctx.ref(), self.fixedpoint, level, predicate.ast)
7036  return _to_expr_ref(r, self.ctx)
7037 
Z3_ast Z3_API Z3_fixedpoint_get_cover_delta(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred)

◆ get_ground_sat_answer()

def get_ground_sat_answer (   self)
Retrieve a ground cex from last query call.

Definition at line 7012 of file z3py.py.

7012  def get_ground_sat_answer(self):
7013  """Retrieve a ground cex from last query call."""
7014  r = Z3_fixedpoint_get_ground_sat_answer(self.ctx.ref(), self.fixedpoint)
7015  return _to_expr_ref(r, self.ctx)
7016 

◆ get_num_levels()

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

Definition at line 7029 of file z3py.py.

7029  def get_num_levels(self, predicate):
7030  """Retrieve number of levels used for predicate in PDR engine"""
7031  return Z3_fixedpoint_get_num_levels(self.ctx.ref(), self.fixedpoint, predicate.ast)
7032 
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. ...

◆ get_rule_names_along_trace()

def get_rule_names_along_trace (   self)
retrieve rule names along the counterexample trace

Definition at line 7021 of file z3py.py.

7021  def get_rule_names_along_trace(self):
7022  """retrieve rule names along the counterexample trace"""
7023  # this is a hack as I don't know how to return a list of symbols from C++;
7024  # obtain names as a single string separated by semicolons
7025  names = _symbol2py (self.ctx, Z3_fixedpoint_get_rule_names_along_trace(self.ctx.ref(), self.fixedpoint))
7026  # split into individual names
7027  return names.split (';')
7028 

◆ get_rules()

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

Definition at line 7072 of file z3py.py.

7072  def get_rules(self):
7073  """retrieve rules that have been added to fixedpoint context"""
7074  return AstVector(Z3_fixedpoint_get_rules(self.ctx.ref(), self.fixedpoint), self.ctx)
7075 
Z3_ast_vector Z3_API Z3_fixedpoint_get_rules(Z3_context c, Z3_fixedpoint f)
Retrieve set of rules from fixedpoint context.

◆ get_rules_along_trace()

def get_rules_along_trace (   self)
retrieve rules along the counterexample trace

Definition at line 7017 of file z3py.py.

7017  def get_rules_along_trace(self):
7018  """retrieve rules along the counterexample trace"""
7019  return AstVector(Z3_fixedpoint_get_rules_along_trace(self.ctx.ref(), self.fixedpoint), self.ctx)
7020 

◆ help()

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

Definition at line 6883 of file z3py.py.

6883  def help(self):
6884  """Display a string describing all available options."""
6885  print(Z3_fixedpoint_get_help(self.ctx.ref(), self.fixedpoint))
6886 
Z3_string Z3_API Z3_fixedpoint_get_help(Z3_context c, Z3_fixedpoint f)
Return a string describing all fixedpoint available parameters.

◆ insert()

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

Definition at line 6917 of file z3py.py.

6917  def insert(self, *args):
6918  """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
6919  self.assert_exprs(*args)
6920 

◆ param_descrs()

def param_descrs (   self)
Return the parameter description set.

Definition at line 6887 of file z3py.py.

6887  def param_descrs(self):
6888  """Return the parameter description set."""
6889  return ParamDescrsRef(Z3_fixedpoint_get_param_descrs(self.ctx.ref(), self.fixedpoint), self.ctx)
6890 
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.

◆ parse_file()

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

Definition at line 7065 of file z3py.py.

7065  def parse_file(self, f):
7066  """Parse rules and queries from a file"""
7067  try:
7068  return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx)
7069  except Z3Exception as e:
7070  _handle_parse_error(e, self.ctx)
7071 
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...

◆ parse_string()

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

Definition at line 7058 of file z3py.py.

7058  def parse_string(self, s):
7059  """Parse rules and queries from a string"""
7060  try:
7061  return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx)
7062  except Z3Exception as e:
7063  _handle_parse_error(e, self.ctx)
7064 
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...

◆ pop()

def pop (   self)
restore to previously created backtracking point

Definition at line 6994 of file z3py.py.

6994  def pop(self):
6995  """restore to previously created backtracking point"""
6996  Z3_fixedpoint_pop(self.ctx.ref(), self.fixedpoint)
6997 
void Z3_API Z3_fixedpoint_pop(Z3_context c, Z3_fixedpoint d)
Backtrack one backtracking point.

◆ push()

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

Definition at line 6990 of file z3py.py.

6990  def push(self):
6991  """create a backtracking point for added rules, facts and assertions"""
6992  Z3_fixedpoint_push(self.ctx.ref(), self.fixedpoint)
6993 
void Z3_API Z3_fixedpoint_push(Z3_context c, Z3_fixedpoint d)
Create a backtracking point.

◆ 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 6952 of file z3py.py.

6952  def query(self, *query):
6953  """Query the fixedpoint engine whether formula is derivable.
6954  You can also pass an tuple or list of recursive predicates.
6955  """
6956  query = _get_args(query)
6957  sz = len(query)
6958  if sz >= 1 and isinstance(query[0], FuncDeclRef):
6959  _decls = (FuncDecl * sz)()
6960  i = 0
6961  for q in query:
6962  _decls[i] = q.ast
6963  i = i + 1
6964  r = Z3_fixedpoint_query_relations(self.ctx.ref(), self.fixedpoint, sz, _decls)
6965  else:
6966  if sz == 1:
6967  query = query[0]
6968  else:
6969  query = And(query, self.ctx)
6970  query = self.abstract(query, False)
6971  r = Z3_fixedpoint_query(self.ctx.ref(), self.fixedpoint, query.as_ast())
6972  return CheckSatResult(r)
6973 
def And(args)
Definition: z3py.py:1655
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.

◆ query_from_lvl()

def query_from_lvl (   self,
  lvl,
  query 
)
Query the fixedpoint engine whether formula is derivable starting at the given query level.

Definition at line 6974 of file z3py.py.

6974  def query_from_lvl (self, lvl, *query):
6975  """Query the fixedpoint engine whether formula is derivable starting at the given query level.
6976  """
6977  query = _get_args(query)
6978  sz = len(query)
6979  if sz >= 1 and isinstance(query[0], FuncDecl):
6980  _z3_assert (False, "unsupported")
6981  else:
6982  if sz == 1:
6983  query = query[0]
6984  else:
6985  query = And(query)
6986  query = self.abstract(query, False)
6987  r = Z3_fixedpoint_query_from_lvl (self.ctx.ref(), self.fixedpoint, query.as_ast(), lvl)
6988  return CheckSatResult(r)
6989 
def And(args)
Definition: z3py.py:1655

◆ reason_unknown()

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

Definition at line 7102 of file z3py.py.

7102  def reason_unknown(self):
7103  """Return a string describing why the last `query()` returned `unknown`.
7104  """
7105  return Z3_fixedpoint_get_reason_unknown(self.ctx.ref(), self.fixedpoint)
7106 
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. ...

◆ register_relation()

def register_relation (   self,
  relations 
)
Register relation as recursive

Definition at line 7042 of file z3py.py.

7042  def register_relation(self, *relations):
7043  """Register relation as recursive"""
7044  relations = _get_args(relations)
7045  for f in relations:
7046  Z3_fixedpoint_register_relation(self.ctx.ref(), self.fixedpoint, f.ast)
7047 
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...

◆ 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 6944 of file z3py.py.

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

◆ set()

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

Definition at line 6877 of file z3py.py.

6877  def set(self, *args, **keys):
6878  """Set a configuration option. The method `help()` return a string containing all available options.
6879  """
6880  p = args2params(args, keys, self.ctx)
6881  Z3_fixedpoint_set_params(self.ctx.ref(), self.fixedpoint, p.params)
6882 
def args2params(arguments, keywords, ctx=None)
Definition: z3py.py:5001
void Z3_API Z3_fixedpoint_set_params(Z3_context c, Z3_fixedpoint f, Z3_params p)
Set parameters on fixedpoint context.

◆ set_predicate_representation()

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

Definition at line 7048 of file z3py.py.

7048  def set_predicate_representation(self, f, *representations):
7049  """Control how relation is represented"""
7050  representations = _get_args(representations)
7051  representations = [to_symbol(s) for s in representations]
7052  sz = len(representations)
7053  args = (Symbol * sz)()
7054  for i in range(sz):
7055  args[i] = representations[i]
7056  Z3_fixedpoint_set_predicate_representation(self.ctx.ref(), self.fixedpoint, f.ast, sz, args)
7057 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3244
def to_symbol(s, ctx=None)
Definition: z3py.py:105
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.

◆ 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 7084 of file z3py.py.

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

7084  def sexpr(self):
7085  """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
7086  """
7087  return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, 0, (Ast * 0)())
7088 
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.

◆ statistics()

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

Definition at line 7097 of file z3py.py.

7097  def statistics(self):
7098  """Return statistics for the last `query()`.
7099  """
7100  return Statistics(Z3_fixedpoint_get_statistics(self.ctx.ref(), self.fixedpoint), self.ctx)
7101 
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.

◆ 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 7089 of file z3py.py.

7089  def to_string(self, queries):
7090  """Return a formatted string (in Lisp-like format) with all added constraints.
7091  We say the string is in s-expression format.
7092  Include also queries.
7093  """
7094  args, len = _to_ast_array(queries)
7095  return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, len, args)
7096 
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.

◆ update_rule()

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

Definition at line 6998 of file z3py.py.

6998  def update_rule(self, head, body, name):
6999  """update rule"""
7000  if name is None:
7001  name = ""
7002  name = to_symbol(name, self.ctx)
7003  body = _get_args(body)
7004  f = self.abstract(Implies(And(body, self.ctx),head))
7005  Z3_fixedpoint_update_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
7006 
def to_symbol(s, ctx=None)
Definition: z3py.py:105
def And(args)
Definition: z3py.py:1655
def Implies(a, b, ctx=None)
Definition: z3py.py:1600
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. ...

Field Documentation

◆ ctx

ctx

Definition at line 6861 of file z3py.py.

Referenced by Probe.__call__(), Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), Fixedpoint.__del__(), Optimize.__del__(), ApplyResult.__del__(), Tactic.__del__(), Probe.__del__(), Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), ApplyResult.__len__(), Probe.__lt__(), Probe.__ne__(), Fixedpoint.add_cover(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), ApplyResult.as_expr(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Optimize.assertions(), Optimize.check(), Optimize.from_file(), Optimize.from_string(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_ground_sat_answer(), Fixedpoint.get_num_levels(), Fixedpoint.get_rule_names_along_trace(), Fixedpoint.get_rules(), Fixedpoint.get_rules_along_trace(), Fixedpoint.help(), Optimize.help(), Tactic.help(), Optimize.maximize(), Optimize.minimize(), Optimize.model(), Optimize.objectives(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Fixedpoint.pop(), Optimize.pop(), Fixedpoint.push(), Optimize.push(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), Fixedpoint.reason_unknown(), Optimize.reason_unknown(), Fixedpoint.register_relation(), Fixedpoint.set(), Optimize.set(), Fixedpoint.set_predicate_representation(), Fixedpoint.sexpr(), Optimize.sexpr(), ApplyResult.sexpr(), Tactic.solver(), Fixedpoint.statistics(), Optimize.statistics(), Fixedpoint.to_string(), Optimize.unsat_core(), and Fixedpoint.update_rule().

◆ fixedpoint

fixedpoint

◆ vars

vars

Definition at line 6868 of file z3py.py.

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