Z3
 
Loading...
Searching...
No Matches
Public Member Functions | Data Fields
Fixedpoint Class Reference

Fixedpoint. More...

+ Inheritance diagram for Fixedpoint:

Public Member Functions

 __init__ (self, fixedpoint=None, ctx=None)
 
 __deepcopy__ (self, memo={})
 
 __del__ (self)
 
 set (self, *args, **keys)
 
 help (self)
 
 param_descrs (self)
 
 assert_exprs (self, *args)
 
 add (self, *args)
 
 __iadd__ (self, fml)
 
 append (self, *args)
 
 insert (self, *args)
 
 add_rule (self, head, body=None, name=None)
 
 rule (self, head, body=None, name=None)
 
 fact (self, head, name=None)
 
 query (self, *query)
 
 query_from_lvl (self, lvl, *query)
 
 update_rule (self, head, body, name)
 
 get_answer (self)
 
 get_ground_sat_answer (self)
 
 get_rules_along_trace (self)
 
 get_rule_names_along_trace (self)
 
 get_num_levels (self, predicate)
 
 get_cover_delta (self, level, predicate)
 
 add_cover (self, level, predicate, property)
 
 register_relation (self, *relations)
 
 set_predicate_representation (self, f, *representations)
 
 parse_string (self, s)
 
 parse_file (self, f)
 
 get_rules (self)
 
 get_assertions (self)
 
 __repr__ (self)
 
 sexpr (self)
 
 to_string (self, queries)
 
 statistics (self)
 
 reason_unknown (self)
 
 declare_var (self, *vars)
 
 abstract (self, fml, is_forall=True)
 
- Public Member Functions inherited from Z3PPObject
 use_pp (self)
 

Data Fields

 ctx
 
 fixedpoint
 
 vars
 

Additional Inherited Members

- Protected Member Functions inherited from Z3PPObject
 _repr_html_ (self)
 

Detailed Description

Fixedpoint.

Fixedpoint API provides methods for solving with recursive predicates

Definition at line 7498 of file z3py.py.

Constructor & Destructor Documentation

◆ __init__()

__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
void Z3_API Z3_fixedpoint_inc_ref(Z3_context c, Z3_fixedpoint d)
Increment the reference counter of the given fixedpoint context.
Z3_fixedpoint Z3_API Z3_mk_fixedpoint(Z3_context c)
Create a new fixedpoint context.

◆ __del__()

__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.

Member Function Documentation

◆ __deepcopy__()

__deepcopy__ (   self,
  memo = {} 
)

Definition at line 7512 of file z3py.py.

7512 def __deepcopy__(self, memo={}):
7513 return FixedPoint(self.fixedpoint, self.ctx)
7514

◆ __iadd__()

__iadd__ (   self,
  fml 
)

Definition at line 7551 of file z3py.py.

7551 def __iadd__(self, fml):
7552 self.add(fml)
7553 return self
7554

◆ __repr__()

__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

◆ abstract()

abstract (   self,
  fml,
  is_forall = True 
)

Definition at line 7749 of file z3py.py.

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

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

◆ add()

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

Definition at line 7547 of file z3py.py.

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

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

◆ add_cover()

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...

◆ add_rule()

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.

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:

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

◆ append()

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

◆ assert_exprs()

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

Definition at line 7533 of file z3py.py.

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
void Z3_API Z3_fixedpoint_assert(Z3_context c, Z3_fixedpoint d, Z3_ast axiom)
Assert a constraint to the fixedpoint context.

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

◆ declare_var()

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

◆ fact()

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

◆ get_answer()

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
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()

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.

◆ get_cover_delta()

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
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()

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

Definition at line 7646 of file z3py.py.

7646 def get_ground_sat_answer(self):
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

◆ get_num_levels()

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.

◆ get_rule_names_along_trace()

get_rule_names_along_trace (   self)
retrieve rule names along the counterexample trace

Definition at line 7655 of file z3py.py.

7655 def get_rule_names_along_trace(self):
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

◆ get_rules()

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
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()

get_rules_along_trace (   self)
retrieve rules along the counterexample trace

Definition at line 7651 of file z3py.py.

7651 def get_rules_along_trace(self):
7652 """retrieve rules along the counterexample trace"""
7653 return AstVector(Z3_fixedpoint_get_rules_along_trace(self.ctx.ref(), self.fixedpoint), self.ctx)
7654

◆ help()

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.

◆ insert()

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

◆ param_descrs()

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
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()

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....

◆ parse_string()

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....

◆ query()

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
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()

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

◆ reason_unknown()

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.

◆ register_relation()

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
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()

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

◆ set()

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
void Z3_API Z3_fixedpoint_set_params(Z3_context c, Z3_fixedpoint f, Z3_params p)
Set parameters on fixedpoint context.

◆ set_predicate_representation()

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
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()

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.

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
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.

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

◆ statistics()

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.

◆ to_string()

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

◆ update_rule()

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

Referenced by ArithRef.__add__(), BitVecRef.__add__(), FPRef.__add__(), BitVecRef.__and__(), FuncDeclRef.__call__(), Probe.__call__(), AstMap.__contains__(), AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), Solver.__copy__(), AstRef.__deepcopy__(), Datatype.__deepcopy__(), ParamsRef.__deepcopy__(), ParamDescrsRef.__deepcopy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), AstMap.__deepcopy__(), FuncEntry.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), Statistics.__deepcopy__(), Solver.__deepcopy__(), Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Simplifier.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), Context.__del__(), AstRef.__del__(), ScopedConstructor.__del__(), ScopedConstructorList.__del__(), ParamsRef.__del__(), ParamDescrsRef.__del__(), Goal.__del__(), AstVector.__del__(), AstMap.__del__(), FuncEntry.__del__(), FuncInterp.__del__(), ModelRef.__del__(), Statistics.__del__(), Solver.__del__(), Fixedpoint.__del__(), Optimize.__del__(), ApplyResult.__del__(), Simplifier.__del__(), Tactic.__del__(), Probe.__del__(), ParserContext.__del__(), ArithRef.__div__(), BitVecRef.__div__(), FPRef.__div__(), ExprRef.__eq__(), Probe.__eq__(), ArithRef.__ge__(), BitVecRef.__ge__(), Probe.__ge__(), FPRef.__ge__(), SeqRef.__ge__(), AstVector.__getitem__(), SeqRef.__getitem__(), ModelRef.__getitem__(), Statistics.__getitem__(), ApplyResult.__getitem__(), AstMap.__getitem__(), ArithRef.__gt__(), BitVecRef.__gt__(), Probe.__gt__(), FPRef.__gt__(), SeqRef.__gt__(), BitVecRef.__invert__(), ArithRef.__le__(), BitVecRef.__le__(), Probe.__le__(), FPRef.__le__(), SeqRef.__le__(), CharRef.__le__(), AstVector.__len__(), AstMap.__len__(), ModelRef.__len__(), Statistics.__len__(), ApplyResult.__len__(), BitVecRef.__lshift__(), ArithRef.__lt__(), BitVecRef.__lt__(), Probe.__lt__(), FPRef.__lt__(), SeqRef.__lt__(), ArithRef.__mod__(), BitVecRef.__mod__(), BoolRef.__mul__(), ArithRef.__mul__(), BitVecRef.__mul__(), FPRef.__mul__(), ExprRef.__ne__(), Probe.__ne__(), ArithRef.__neg__(), BitVecRef.__neg__(), BitVecRef.__or__(), ArithRef.__pow__(), ArithRef.__radd__(), BitVecRef.__radd__(), FPRef.__radd__(), BitVecRef.__rand__(), ArithRef.__rdiv__(), BitVecRef.__rdiv__(), FPRef.__rdiv__(), ParamsRef.__repr__(), ParamDescrsRef.__repr__(), AstMap.__repr__(), Statistics.__repr__(), BitVecRef.__rlshift__(), ArithRef.__rmod__(), BitVecRef.__rmod__(), ArithRef.__rmul__(), BitVecRef.__rmul__(), FPRef.__rmul__(), BitVecRef.__ror__(), ArithRef.__rpow__(), BitVecRef.__rrshift__(), BitVecRef.__rshift__(), ArithRef.__rsub__(), BitVecRef.__rsub__(), FPRef.__rsub__(), BitVecRef.__rxor__(), AstVector.__setitem__(), AstMap.__setitem__(), ArithRef.__sub__(), BitVecRef.__sub__(), FPRef.__sub__(), BitVecRef.__xor__(), DatatypeSortRef.accessor(), Simplifier.add(), Fixedpoint.add_cover(), ParserContext.add_decl(), Fixedpoint.add_rule(), Optimize.add_soft(), ParserContext.add_sort(), Tactic.apply(), ExprRef.arg(), FuncEntry.arg_value(), FuncInterp.arity(), Goal.as_expr(), ApplyResult.as_expr(), FPNumRef.as_string(), Solver.assert_and_track(), Optimize.assert_and_track(), Goal.assert_exprs(), Solver.assert_exprs(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Solver.assertions(), Optimize.assertions(), SeqRef.at(), QuantifierRef.body(), Solver.check(), Optimize.check(), UserPropagateBase.conflict(), Solver.consequences(), Goal.convert_model(), AstRef.ctx_ref(), UserPropagateBase.ctx_ref(), ExprRef.decl(), ModelRef.decls(), ArrayRef.default(), RatNumRef.denominator(), Goal.depth(), Goal.dimacs(), Solver.dimacs(), FuncDeclRef.domain(), ArraySortRef.domain_n(), FuncInterp.else_value(), FuncInterp.entry(), AstMap.erase(), ModelRef.eval(), FPNumRef.exponent(), FPNumRef.exponent_as_bv(), FPNumRef.exponent_as_long(), Solver.from_file(), Optimize.from_file(), Solver.from_string(), Optimize.from_string(), ParserContext.from_string(), Goal.get(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), ParamDescrsRef.get_documentation(), Fixedpoint.get_ground_sat_answer(), ModelRef.get_interp(), Statistics.get_key_value(), ParamDescrsRef.get_kind(), ParamDescrsRef.get_name(), Fixedpoint.get_num_levels(), Fixedpoint.get_rule_names_along_trace(), Fixedpoint.get_rules(), Fixedpoint.get_rules_along_trace(), ModelRef.get_sort(), ModelRef.get_universe(), Solver.help(), Fixedpoint.help(), Optimize.help(), Simplifier.help(), Tactic.help(), Solver.import_model_converter(), Goal.inconsistent(), Solver.interrupt(), CharRef.is_digit(), FPNumRef.isInf(), FPNumRef.isNaN(), FPNumRef.isNegative(), FPNumRef.isNormal(), FPNumRef.isPositive(), FPNumRef.isSubnormal(), FPNumRef.isZero(), AstMap.keys(), Statistics.keys(), Optimize.maximize(), Optimize.minimize(), Solver.model(), Optimize.model(), SortRef.name(), Solver.next(), QuantifierRef.no_pattern(), Solver.non_units(), FuncEntry.num_args(), FuncInterp.num_entries(), Solver.num_scopes(), ModelRef.num_sorts(), Optimize.objectives(), Solver.param_descrs(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Simplifier.param_descrs(), Tactic.param_descrs(), FuncDeclRef.params(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), QuantifierRef.pattern(), AlgebraicNumRef.poly(), Optimize.pop(), Solver.pop(), Goal.prec(), Solver.proof(), Solver.push(), Optimize.push(), AstVector.push(), QuantifierRef.qid(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), FuncDeclRef.range(), ArraySortRef.range(), Solver.reason_unknown(), Fixedpoint.reason_unknown(), Optimize.reason_unknown(), DatatypeSortRef.recognizer(), Context.ref(), Fixedpoint.register_relation(), AstMap.reset(), Solver.reset(), AstVector.resize(), Solver.root(), Solver.set(), Fixedpoint.set(), Optimize.set(), ParamsRef.set(), Optimize.set_on_model(), Fixedpoint.set_predicate_representation(), Goal.sexpr(), AstVector.sexpr(), ModelRef.sexpr(), Solver.sexpr(), Fixedpoint.sexpr(), Optimize.sexpr(), ApplyResult.sexpr(), FPNumRef.sign(), FPNumRef.significand(), FPNumRef.significand_as_bv(), FPNumRef.significand_as_long(), ParamDescrsRef.size(), Goal.size(), QuantifierRef.skolem_id(), Tactic.solver(), Solver.statistics(), Fixedpoint.statistics(), Optimize.statistics(), CharRef.to_bv(), CharRef.to_int(), Solver.to_smt2(), Fixedpoint.to_string(), Solver.trail(), Solver.trail_levels(), AstVector.translate(), AstRef.translate(), Goal.translate(), ModelRef.translate(), Solver.translate(), Solver.units(), Solver.unsat_core(), Optimize.unsat_core(), Fixedpoint.update_rule(), Simplifier.using_params(), ParamsRef.validate(), FuncEntry.value(), QuantifierRef.var_name(), and QuantifierRef.var_sort().

◆ fixedpoint

fixedpoint

◆ vars

vars

Definition at line 7510 of file z3py.py.

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