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) | |
![]() | |
use_pp (self) | |
Data Fields | |
ctx = _get_ctx(ctx) | |
fixedpoint = None | |
list | vars = [] |
Additional Inherited Members | |
![]() | |
_repr_html_ (self) | |
Fixedpoint API provides methods for solving with recursive predicates
__init__ | ( | self, | |
fixedpoint = None, | |||
ctx = None ) |
Definition at line 7508 of file z3py.py.
__del__ | ( | self | ) |
Definition at line 7522 of file z3py.py.
__deepcopy__ | ( | self, | |
memo = {} ) |
__iadd__ | ( | self, | |
fml ) |
__repr__ | ( | self | ) |
abstract | ( | self, | |
fml, | |||
is_forall = True ) |
add | ( | self, | |
* | args ) |
Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.
Definition at line 7554 of file z3py.py.
Referenced by Solver.__iadd__().
add_cover | ( | self, | |
level, | |||
predicate, | |||
property ) |
Add property to predicate for the level'th unfolding. -1 is treated as infinity (infinity)
Definition at line 7681 of file z3py.py.
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 7570 of file z3py.py.
append | ( | self, | |
* | args ) |
assert_exprs | ( | self, | |
* | args ) |
Assert constraints as background axioms for the fixedpoint solver.
Definition at line 7540 of file z3py.py.
Referenced by Goal.add(), Solver.add(), Goal.append(), Solver.append(), Goal.insert(), and Solver.insert().
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 7747 of file z3py.py.
fact | ( | self, | |
head, | |||
name = None ) |
Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule.
Definition at line 7597 of file z3py.py.
get_answer | ( | self | ) |
Retrieve answer from last query call.
Definition at line 7648 of file z3py.py.
get_assertions | ( | self | ) |
retrieve assertions that have been added to fixedpoint context
Definition at line 7715 of file z3py.py.
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 7674 of file z3py.py.
get_ground_sat_answer | ( | self | ) |
get_num_levels | ( | self, | |
predicate ) |
Retrieve number of levels used for predicate in PDR engine
Definition at line 7670 of file z3py.py.
get_rule_names_along_trace | ( | self | ) |
retrieve rule names along the counterexample trace
Definition at line 7662 of file z3py.py.
get_rules | ( | self | ) |
retrieve rules that have been added to fixedpoint context
Definition at line 7711 of file z3py.py.
get_rules_along_trace | ( | self | ) |
help | ( | self | ) |
Display a string describing all available options.
Definition at line 7532 of file z3py.py.
insert | ( | self, | |
* | args ) |
param_descrs | ( | self | ) |
Return the parameter description set.
Definition at line 7536 of file z3py.py.
parse_file | ( | self, | |
f ) |
Parse rules and queries from a file
Definition at line 7707 of file z3py.py.
parse_string | ( | self, | |
s ) |
Parse rules and queries from a string
Definition at line 7703 of file z3py.py.
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 7601 of file z3py.py.
query_from_lvl | ( | self, | |
lvl, | |||
* | query ) |
Query the fixedpoint engine whether formula is derivable starting at the given query level.
Definition at line 7623 of file z3py.py.
reason_unknown | ( | self | ) |
Return a string describing why the last `query()` returned `unknown`.
Definition at line 7742 of file z3py.py.
register_relation | ( | self, | |
* | relations ) |
Register relation as recursive
Definition at line 7687 of file z3py.py.
rule | ( | self, | |
head, | |||
body = None, | |||
name = None ) |
Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule.
Definition at line 7593 of file z3py.py.
set | ( | self, | |
* | args, | ||
** | keys ) |
Set a configuration option. The method `help()` return a string containing all available options.
Definition at line 7526 of file z3py.py.
set_predicate_representation | ( | self, | |
f, | |||
* | representations ) |
Control how relation is represented
Definition at line 7693 of file z3py.py.
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 7723 of file z3py.py.
statistics | ( | self | ) |
Return statistics for the last `query()`.
Definition at line 7737 of file z3py.py.
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 7729 of file z3py.py.
update_rule | ( | self, | |
head, | |||
body, | |||
name ) |
update rule
Definition at line 7639 of file z3py.py.
ctx = _get_ctx(ctx) |
Definition at line 7510 of file z3py.py.
Referenced by ArithRef.__add__(), BitVecRef.__add__(), BitVecRef.__and__(), FuncDeclRef.__call__(), AstMap.__contains__(), AstRef.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), Goal.__copy__(), ModelRef.__copy__(), AstMap.__deepcopy__(), AstRef.__deepcopy__(), AstVector.__deepcopy__(), Datatype.__deepcopy__(), FuncEntry.__deepcopy__(), FuncInterp.__deepcopy__(), Goal.__deepcopy__(), ModelRef.__deepcopy__(), ParamDescrsRef.__deepcopy__(), ParamsRef.__deepcopy__(), Statistics.__deepcopy__(), AstMap.__del__(), AstRef.__del__(), AstVector.__del__(), Context.__del__(), FuncEntry.__del__(), FuncInterp.__del__(), Goal.__del__(), ModelRef.__del__(), ParamDescrsRef.__del__(), ParamsRef.__del__(), ScopedConstructor.__del__(), ScopedConstructorList.__del__(), Solver.__del__(), Statistics.__del__(), ArithRef.__div__(), BitVecRef.__div__(), ExprRef.__eq__(), ArithRef.__ge__(), BitVecRef.__ge__(), AstMap.__getitem__(), AstVector.__getitem__(), ModelRef.__getitem__(), Statistics.__getitem__(), ArithRef.__gt__(), BitVecRef.__gt__(), BitVecRef.__invert__(), ArithRef.__le__(), BitVecRef.__le__(), AstMap.__len__(), AstVector.__len__(), ModelRef.__len__(), Statistics.__len__(), BitVecRef.__lshift__(), ArithRef.__lt__(), BitVecRef.__lt__(), ArithRef.__mod__(), BitVecRef.__mod__(), ArithRef.__mul__(), BitVecRef.__mul__(), BoolRef.__mul__(), ExprRef.__ne__(), ArithRef.__neg__(), BitVecRef.__neg__(), BitVecRef.__or__(), ArithRef.__pow__(), ArithRef.__radd__(), BitVecRef.__radd__(), BitVecRef.__rand__(), ArithRef.__rdiv__(), BitVecRef.__rdiv__(), AstMap.__repr__(), ParamDescrsRef.__repr__(), ParamsRef.__repr__(), Statistics.__repr__(), BitVecRef.__rlshift__(), ArithRef.__rmod__(), BitVecRef.__rmod__(), ArithRef.__rmul__(), BitVecRef.__rmul__(), BitVecRef.__ror__(), ArithRef.__rpow__(), BitVecRef.__rrshift__(), BitVecRef.__rshift__(), ArithRef.__rsub__(), BitVecRef.__rsub__(), BitVecRef.__rxor__(), AstMap.__setitem__(), AstVector.__setitem__(), ArithRef.__sub__(), BitVecRef.__sub__(), BitVecRef.__xor__(), DatatypeSortRef.accessor(), ExprRef.arg(), FuncEntry.arg_value(), FuncInterp.arity(), Goal.as_expr(), Solver.assert_and_track(), Goal.assert_exprs(), Solver.assert_exprs(), QuantifierRef.body(), Solver.check(), Goal.convert_model(), AstRef.ctx_ref(), ExprRef.decl(), ModelRef.decls(), ArrayRef.default(), RatNumRef.denominator(), Goal.depth(), Goal.dimacs(), FuncDeclRef.domain(), ArraySortRef.domain_n(), FuncInterp.else_value(), FuncInterp.entry(), AstMap.erase(), ModelRef.eval(), Goal.get(), ParamDescrsRef.get_documentation(), ModelRef.get_interp(), Statistics.get_key_value(), ParamDescrsRef.get_kind(), ParamDescrsRef.get_name(), ModelRef.get_sort(), ModelRef.get_universe(), Goal.inconsistent(), AstMap.keys(), Statistics.keys(), Solver.model(), SortRef.name(), QuantifierRef.no_pattern(), FuncEntry.num_args(), FuncInterp.num_entries(), Solver.num_scopes(), ModelRef.num_sorts(), FuncDeclRef.params(), QuantifierRef.pattern(), AlgebraicNumRef.poly(), Solver.pop(), Goal.prec(), AstVector.push(), Solver.push(), QuantifierRef.qid(), ArraySortRef.range(), FuncDeclRef.range(), DatatypeSortRef.recognizer(), Context.ref(), AstMap.reset(), Solver.reset(), AstVector.resize(), ParamsRef.set(), Solver.set(), AstVector.sexpr(), Goal.sexpr(), ModelRef.sexpr(), Goal.size(), ParamDescrsRef.size(), QuantifierRef.skolem_id(), AstRef.translate(), AstVector.translate(), Goal.translate(), ModelRef.translate(), ParamsRef.validate(), FuncEntry.value(), QuantifierRef.var_name(), and QuantifierRef.var_sort().