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

Fixedpoint. More...

+ Inheritance diagram for Fixedpoint:

Public Member Functions

def __init__
 
def __deepcopy__
 
def __del__
 
def set
 
def help
 
def param_descrs
 
def assert_exprs
 
def add
 
def __iadd__
 
def append
 
def insert
 
def add_rule
 
def rule
 
def fact
 
def query
 
def query_from_lvl
 
def update_rule
 
def get_answer
 
def get_ground_sat_answer
 
def get_rules_along_trace
 
def get_rule_names_along_trace
 
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 6916 of file z3py.py.

Constructor & Destructor Documentation

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

Definition at line 6919 of file z3py.py.

6920  def __init__(self, fixedpoint=None, ctx=None):
6921  assert fixedpoint is None or ctx is not None
6922  self.ctx = _get_ctx(ctx)
6923  self.fixedpoint = None
6924  if fixedpoint is None:
6925  self.fixedpoint = Z3_mk_fixedpoint(self.ctx.ref())
6926  else:
6927  self.fixedpoint = fixedpoint
6928  Z3_fixedpoint_inc_ref(self.ctx.ref(), self.fixedpoint)
6929  self.vars = []
Z3_fixedpoint Z3_API Z3_mk_fixedpoint(Z3_context c)
Create a new fixedpoint context.
def __init__
Definition: z3py.py:6919
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 6933 of file z3py.py.

6934  def __del__(self):
6935  if self.fixedpoint is not None and self.ctx.ref() is not None:
6936  Z3_fixedpoint_dec_ref(self.ctx.ref(), self.fixedpoint)
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

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 6930 of file z3py.py.

6931  def __deepcopy__(self, memo={}):
6932  return FixedPoint(self.fixedpoint, self.ctx)
def __deepcopy__
Definition: z3py.py:6930
def __iadd__ (   self,
  fml 
)

Definition at line 6969 of file z3py.py.

6970  def __iadd__(self, fml):
6971  self.add(fml)
6972  return self
def __iadd__
Definition: z3py.py:6969
def __repr__ (   self)
Return a formatted string with all added rules and constraints.

Definition at line 7126 of file z3py.py.

7127  def __repr__(self):
7128  """Return a formatted string with all added rules and constraints."""
7129  return self.sexpr()
def __repr__
Definition: z3py.py:7126
def abstract (   self,
  fml,
  is_forall = True 
)

Definition at line 7162 of file z3py.py.

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

7163  def abstract(self, fml, is_forall=True):
7164  if self.vars == []:
7165  return fml
7166  if is_forall:
7167  return ForAll(self.vars, fml)
7168  else:
7169  return Exists(self.vars, fml)
7170 
def Exists
Definition: z3py.py:2044
def ForAll
Definition: z3py.py:2027
def abstract
Definition: z3py.py:7162
def add (   self,
  args 
)
Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.

Definition at line 6965 of file z3py.py.

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

6966  def add(self, *args):
6967  """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
6968  self.assert_exprs(*args)
def assert_exprs
Definition: z3py.py:6951
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 7090 of file z3py.py.

7091  def add_cover(self, level, predicate, property):
7092  """Add property to predicate for the level'th unfolding. -1 is treated as infinity (infinity)"""
7093  Z3_fixedpoint_add_cover(self.ctx.ref(), self.fixedpoint, level, predicate.ast, property.ast)
def add_cover
Definition: z3py.py:7090
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_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 6981 of file z3py.py.

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

6982  def add_rule(self, head, body = None, name = None):
6983  """Assert rules defining recursive predicates to the fixedpoint solver.
6984  >>> a = Bool('a')
6985  >>> b = Bool('b')
6986  >>> s = Fixedpoint()
6987  >>> s.register_relation(a.decl())
6988  >>> s.register_relation(b.decl())
6989  >>> s.fact(a)
6990  >>> s.rule(b, a)
6991  >>> s.query(b)
6992  sat
6993  """
6994  if name is None:
6995  name = ""
6996  name = to_symbol(name, self.ctx)
6997  if body is None:
6998  head = self.abstract(head)
6999  Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, head.as_ast(), name)
7000  else:
7001  body = _get_args(body)
7002  f = self.abstract(Implies(And(body, self.ctx),head))
7003  Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
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:1611
def And
Definition: z3py.py:1672
def abstract
Definition: z3py.py:7162
def add_rule
Definition: z3py.py:6981
def to_symbol
Definition: z3py.py:111
def append (   self,
  args 
)
Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.

Definition at line 6973 of file z3py.py.

6974  def append(self, *args):
6975  """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
6976  self.assert_exprs(*args)
def assert_exprs
Definition: z3py.py:6951
def assert_exprs (   self,
  args 
)
Assert constraints as background axioms for the fixedpoint solver.

Definition at line 6951 of file z3py.py.

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

6952  def assert_exprs(self, *args):
6953  """Assert constraints as background axioms for the fixedpoint solver."""
6954  args = _get_args(args)
6955  s = BoolSort(self.ctx)
6956  for arg in args:
6957  if isinstance(arg, Goal) or isinstance(arg, AstVector):
6958  for f in arg:
6959  f = self.abstract(f)
6960  Z3_fixedpoint_assert(self.ctx.ref(), self.fixedpoint, f.as_ast())
6961  else:
6962  arg = s.cast(arg)
6963  arg = self.abstract(arg)
6964  Z3_fixedpoint_assert(self.ctx.ref(), self.fixedpoint, arg.as_ast())
def BoolSort
Definition: z3py.py:1523
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:7162
def assert_exprs
Definition: z3py.py:6951
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 7153 of file z3py.py.

7154  def declare_var(self, *vars):
7155  """Add variable or several variables.
7156  The added variable or variables will be bound in the rules
7157  and queries
7158  """
7159  vars = _get_args(vars)
7160  for v in vars:
7161  self.vars += [v]
def declare_var
Definition: z3py.py:7153
def fact (   self,
  head,
  name = None 
)
Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule.

Definition at line 7008 of file z3py.py.

7009  def fact(self, head, name = None):
7010  """Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
7011  self.add_rule(head, None, name)
def add_rule
Definition: z3py.py:6981
def get_answer (   self)
Retrieve answer from last query call.

Definition at line 7059 of file z3py.py.

7060  def get_answer(self):
7061  """Retrieve answer from last query call."""
7062  r = Z3_fixedpoint_get_answer(self.ctx.ref(), self.fixedpoint)
7063  return _to_expr_ref(r, self.ctx)
def get_answer
Definition: z3py.py:7059
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 7122 of file z3py.py.

7123  def get_assertions(self):
7124  """retrieve assertions that have been added to fixedpoint context"""
7125  return AstVector(Z3_fixedpoint_get_assertions(self.ctx.ref(), self.fixedpoint), self.ctx)
def get_assertions
Definition: z3py.py:7122
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_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 7085 of file z3py.py.

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

Definition at line 7064 of file z3py.py.

7065  def get_ground_sat_answer(self):
7066  """Retrieve a ground cex from last query call."""
7067  r = Z3_fixedpoint_get_ground_sat_answer(self.ctx.ref(), self.fixedpoint)
7068  return _to_expr_ref(r, self.ctx)
def get_ground_sat_answer
Definition: z3py.py:7064
def get_num_levels (   self,
  predicate 
)
Retrieve number of levels used for predicate in PDR engine

Definition at line 7081 of file z3py.py.

7082  def get_num_levels(self, predicate):
7083  """Retrieve number of levels used for predicate in PDR engine"""
7084  return Z3_fixedpoint_get_num_levels(self.ctx.ref(), self.fixedpoint, predicate.ast)
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
Definition: z3py.py:7081
def get_rule_names_along_trace (   self)
retrieve rule names along the counterexample trace

Definition at line 7073 of file z3py.py.

7074  def get_rule_names_along_trace(self):
7075  """retrieve rule names along the counterexample trace"""
7076  # this is a hack as I don't know how to return a list of symbols from C++;
7077  # obtain names as a single string separated by semicolons
7078  names = _symbol2py (self.ctx, Z3_fixedpoint_get_rule_names_along_trace(self.ctx.ref(), self.fixedpoint))
7079  # split into individual names
7080  return names.split (';')
def get_rule_names_along_trace
Definition: z3py.py:7073
def get_rules (   self)
retrieve rules that have been added to fixedpoint context

Definition at line 7118 of file z3py.py.

7119  def get_rules(self):
7120  """retrieve rules that have been added to fixedpoint context"""
7121  return AstVector(Z3_fixedpoint_get_rules(self.ctx.ref(), self.fixedpoint), self.ctx)
def get_rules
Definition: z3py.py:7118
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 7069 of file z3py.py.

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

Definition at line 6943 of file z3py.py.

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

Definition at line 6977 of file z3py.py.

6978  def insert(self, *args):
6979  """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
6980  self.assert_exprs(*args)
def assert_exprs
Definition: z3py.py:6951
def param_descrs (   self)
Return the parameter description set.

Definition at line 6947 of file z3py.py.

6948  def param_descrs(self):
6949  """Return the parameter description set."""
6950  return ParamDescrsRef(Z3_fixedpoint_get_param_descrs(self.ctx.ref(), self.fixedpoint), self.ctx)
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 param_descrs
Definition: z3py.py:6947
def parse_file (   self,
  f 
)
Parse rules and queries from a file

Definition at line 7114 of file z3py.py.

7115  def parse_file(self, f):
7116  """Parse rules and queries from a file"""
7117  return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx)
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
Definition: z3py.py:7114
def parse_string (   self,
  s 
)
Parse rules and queries from a string

Definition at line 7110 of file z3py.py.

7111  def parse_string(self, s):
7112  """Parse rules and queries from a string"""
7113  return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx)
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
Definition: z3py.py:7110
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 7012 of file z3py.py.

7013  def query(self, *query):
7014  """Query the fixedpoint engine whether formula is derivable.
7015  You can also pass an tuple or list of recursive predicates.
7016  """
7017  query = _get_args(query)
7018  sz = len(query)
7019  if sz >= 1 and isinstance(query[0], FuncDeclRef):
7020  _decls = (FuncDecl * sz)()
7021  i = 0
7022  for q in query:
7023  _decls[i] = q.ast
7024  i = i + 1
7025  r = Z3_fixedpoint_query_relations(self.ctx.ref(), self.fixedpoint, sz, _decls)
7026  else:
7027  if sz == 1:
7028  query = query[0]
7029  else:
7030  query = And(query, self.ctx)
7031  query = self.abstract(query, False)
7032  r = Z3_fixedpoint_query(self.ctx.ref(), self.fixedpoint, query.as_ast())
7033  return CheckSatResult(r)
def And
Definition: z3py.py:1672
def abstract
Definition: z3py.py:7162
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 7034 of file z3py.py.

7035  def query_from_lvl (self, lvl, *query):
7036  """Query the fixedpoint engine whether formula is derivable starting at the given query level.
7037  """
7038  query = _get_args(query)
7039  sz = len(query)
7040  if sz >= 1 and isinstance(query[0], FuncDecl):
7041  _z3_assert (False, "unsupported")
7042  else:
7043  if sz == 1:
7044  query = query[0]
7045  else:
7046  query = And(query)
7047  query = self.abstract(query, False)
7048  r = Z3_fixedpoint_query_from_lvl (self.ctx.ref(), self.fixedpoint, query.as_ast(), lvl)
7049  return CheckSatResult(r)
def And
Definition: z3py.py:1672
def abstract
Definition: z3py.py:7162
def query_from_lvl
Definition: z3py.py:7034
def reason_unknown (   self)
Return a string describing why the last `query()` returned `unknown`.

Definition at line 7148 of file z3py.py.

7149  def reason_unknown(self):
7150  """Return a string describing why the last `query()` returned `unknown`.
7151  """
7152  return Z3_fixedpoint_get_reason_unknown(self.ctx.ref(), self.fixedpoint)
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
Definition: z3py.py:7148
def register_relation (   self,
  relations 
)
Register relation as recursive

Definition at line 7094 of file z3py.py.

7095  def register_relation(self, *relations):
7096  """Register relation as recursive"""
7097  relations = _get_args(relations)
7098  for f in relations:
7099  Z3_fixedpoint_register_relation(self.ctx.ref(), self.fixedpoint, f.ast)
def register_relation
Definition: z3py.py:7094
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 7004 of file z3py.py.

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

Definition at line 6937 of file z3py.py.

6938  def set(self, *args, **keys):
6939  """Set a configuration option. The method `help()` return a string containing all available options.
6940  """
6941  p = args2params(args, keys, self.ctx)
6942  Z3_fixedpoint_set_params(self.ctx.ref(), self.fixedpoint, p.params)
def args2params
Definition: z3py.py:5050
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 7100 of file z3py.py.

7101  def set_predicate_representation(self, f, *representations):
7102  """Control how relation is represented"""
7103  representations = _get_args(representations)
7104  representations = [to_symbol(s) for s in representations]
7105  sz = len(representations)
7106  args = (Symbol * sz)()
7107  for i in range(sz):
7108  args[i] = representations[i]
7109  Z3_fixedpoint_set_predicate_representation(self.ctx.ref(), self.fixedpoint, f.ast, sz, args)
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3358
def set_predicate_representation
Definition: z3py.py:7100
def to_symbol
Definition: z3py.py:111
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 7130 of file z3py.py.

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

7131  def sexpr(self):
7132  """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
7133  """
7134  return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, 0, (Ast * 0)())
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 7143 of file z3py.py.

7144  def statistics(self):
7145  """Return statistics for the last `query()`.
7146  """
7147  return Statistics(Z3_fixedpoint_get_statistics(self.ctx.ref(), self.fixedpoint), self.ctx)
def statistics
Definition: z3py.py:7143
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:6235
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 7135 of file z3py.py.

7136  def to_string(self, queries):
7137  """Return a formatted string (in Lisp-like format) with all added constraints.
7138  We say the string is in s-expression format.
7139  Include also queries.
7140  """
7141  args, len = _to_ast_array(queries)
7142  return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, len, args)
def to_string
Definition: z3py.py:7135
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 7050 of file z3py.py.

7051  def update_rule(self, head, body, name):
7052  """update rule"""
7053  if name is None:
7054  name = ""
7055  name = to_symbol(name, self.ctx)
7056  body = _get_args(body)
7057  f = self.abstract(Implies(And(body, self.ctx),head))
7058  Z3_fixedpoint_update_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
def Implies
Definition: z3py.py:1611
def And
Definition: z3py.py:1672
def abstract
Definition: z3py.py:7162
def update_rule
Definition: z3py.py:7050
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:111

Field Documentation

ctx

Definition at line 6921 of file z3py.py.

Referenced by Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), Probe.__ne__(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), ApplyResult.as_expr(), Optimize.assert_and_track(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Optimize.assertions(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_ground_sat_answer(), Fixedpoint.get_rule_names_along_trace(), Fixedpoint.get_rules(), Fixedpoint.get_rules_along_trace(), Optimize.model(), Optimize.objectives(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Fixedpoint.query(), Fixedpoint.set(), Optimize.set(), Tactic.solver(), Fixedpoint.statistics(), Optimize.statistics(), Optimize.unsat_core(), and Fixedpoint.update_rule().

fixedpoint

Definition at line 6922 of file z3py.py.

Referenced by Fixedpoint.__deepcopy__(), Fixedpoint.__del__(), Fixedpoint.add_cover(), Fixedpoint.add_rule(), Fixedpoint.assert_exprs(), 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(), Fixedpoint.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), Fixedpoint.reason_unknown(), Fixedpoint.register_relation(), Fixedpoint.set(), Fixedpoint.set_predicate_representation(), Fixedpoint.sexpr(), Fixedpoint.statistics(), Fixedpoint.to_string(), and Fixedpoint.update_rule().

vars

Definition at line 6928 of file z3py.py.

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