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 | 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) |
![]() | |
def | use_pp (self) |
Data Fields | |
ctx | |
fixedpoint | |
vars | |
Fixedpoint API provides methods for solving with recursive predicates
def __init__ | ( | self, | |
fixedpoint = None , |
|||
ctx = None |
|||
) |
Definition at line 7315 of file z3py.py.
def __del__ | ( | self | ) |
Definition at line 7329 of file z3py.py.
def __deepcopy__ | ( | self, | |
memo = {} |
|||
) |
def __iadd__ | ( | self, | |
fml | |||
) |
def __repr__ | ( | self | ) |
def abstract | ( | self, | |
fml, | |||
is_forall = True |
|||
) |
Definition at line 7563 of file z3py.py.
Referenced by Fixedpoint.add_rule(), Fixedpoint.assert_exprs(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), and Fixedpoint.update_rule().
def add | ( | self, | |
* | args | ||
) |
Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.
Definition at line 7361 of file z3py.py.
Referenced by Solver.__iadd__(), Fixedpoint.__iadd__(), and Optimize.__iadd__().
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 7488 of file z3py.py.
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 7377 of file z3py.py.
Referenced by Fixedpoint.fact(), and Fixedpoint.rule().
def append | ( | self, | |
* | args | ||
) |
def assert_exprs | ( | self, | |
* | args | ||
) |
Assert constraints as background axioms for the fixedpoint solver.
Definition at line 7347 of file z3py.py.
Referenced by Goal.add(), Solver.add(), Fixedpoint.add(), Optimize.add(), Goal.append(), Solver.append(), Fixedpoint.append(), Goal.insert(), Solver.insert(), and Fixedpoint.insert().
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 7554 of file z3py.py.
def fact | ( | self, | |
head, | |||
name = None |
|||
) |
Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule.
Definition at line 7404 of file z3py.py.
def get_answer | ( | self | ) |
Retrieve answer from last query call.
Definition at line 7455 of file z3py.py.
def get_assertions | ( | self | ) |
retrieve assertions that have been added to fixedpoint context
Definition at line 7522 of file z3py.py.
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 7481 of file z3py.py.
def get_ground_sat_answer | ( | self | ) |
def get_num_levels | ( | self, | |
predicate | |||
) |
Retrieve number of levels used for predicate in PDR engine
Definition at line 7477 of file z3py.py.
def get_rule_names_along_trace | ( | self | ) |
retrieve rule names along the counterexample trace
Definition at line 7469 of file z3py.py.
def get_rules | ( | self | ) |
retrieve rules that have been added to fixedpoint context
Definition at line 7518 of file z3py.py.
def get_rules_along_trace | ( | self | ) |
def help | ( | self | ) |
Display a string describing all available options.
Definition at line 7339 of file z3py.py.
def insert | ( | self, | |
* | args | ||
) |
def param_descrs | ( | self | ) |
Return the parameter description set.
Definition at line 7343 of file z3py.py.
def parse_file | ( | self, | |
f | |||
) |
Parse rules and queries from a file
Definition at line 7514 of file z3py.py.
def parse_string | ( | self, | |
s | |||
) |
Parse rules and queries from a string
Definition at line 7510 of file z3py.py.
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 7408 of file z3py.py.
def query_from_lvl | ( | self, | |
lvl, | |||
* | query | ||
) |
Query the fixedpoint engine whether formula is derivable starting at the given query level.
Definition at line 7430 of file z3py.py.
def reason_unknown | ( | self | ) |
Return a string describing why the last `query()` returned `unknown`.
Definition at line 7549 of file z3py.py.
def register_relation | ( | self, | |
* | relations | ||
) |
Register relation as recursive
Definition at line 7494 of file z3py.py.
def rule | ( | self, | |
head, | |||
body = None , |
|||
name = None |
|||
) |
Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule.
Definition at line 7400 of file z3py.py.
def set | ( | self, | |
* | args, | ||
** | keys | ||
) |
Set a configuration option. The method `help()` return a string containing all available options.
Definition at line 7333 of file z3py.py.
def set_predicate_representation | ( | self, | |
f, | |||
* | representations | ||
) |
Control how relation is represented
Definition at line 7500 of file z3py.py.
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 7530 of file z3py.py.
Referenced by Fixedpoint.__repr__(), and Optimize.__repr__().
def statistics | ( | self | ) |
Return statistics for the last `query()`.
Definition at line 7544 of file z3py.py.
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 7536 of file z3py.py.
def update_rule | ( | self, | |
head, | |||
body, | |||
name | |||
) |
update rule
Definition at line 7446 of file z3py.py.
ctx |
Definition at line 7317 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__(), 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__(), Tactic.__del__(), Probe.__del__(), ArithRef.__div__(), BitVecRef.__div__(), FPRef.__div__(), ExprRef.__eq__(), Probe.__eq__(), ArithRef.__ge__(), BitVecRef.__ge__(), Probe.__ge__(), FPRef.__ge__(), SeqRef.__ge__(), QuantifierRef.__getitem__(), ArrayRef.__getitem__(), 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__(), 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__(), 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(), Fixedpoint.add_cover(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), AlgebraicNumRef.approx(), 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(), SeqSortRef.basis(), ReSortRef.basis(), QuantifierRef.body(), BoolSortRef.cast(), Solver.check(), Optimize.check(), UserPropagateBase.conflict(), Solver.consequences(), DatatypeSortRef.constructor(), Goal.convert_model(), AstRef.ctx_ref(), UserPropagateBase.ctx_ref(), ExprRef.decl(), ModelRef.decls(), ArrayRef.default(), RatNumRef.denominator(), Goal.depth(), Goal.dimacs(), Solver.dimacs(), ArraySortRef.domain(), FuncDeclRef.domain(), 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(), 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(), Tactic.help(), Solver.import_model_converter(), Goal.inconsistent(), FPNumRef.isInf(), FPNumRef.isNaN(), FPNumRef.isNegative(), FPNumRef.isNormal(), FPNumRef.isPositive(), FPNumRef.isSubnormal(), FPNumRef.isZero(), AstMap.keys(), Statistics.keys(), SortRef.kind(), Optimize.maximize(), Optimize.minimize(), Solver.model(), Optimize.model(), SortRef.name(), FuncDeclRef.name(), QuantifierRef.no_pattern(), Solver.non_units(), FuncEntry.num_args(), FuncInterp.num_entries(), Solver.num_scopes(), ModelRef.num_sorts(), RatNumRef.numerator(), Optimize.objectives(), Solver.param_descrs(), Fixedpoint.param_descrs(), Optimize.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(), 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.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.sign_as_bv(), FPNumRef.significand(), FPNumRef.significand_as_bv(), FPNumRef.significand_as_long(), ParamDescrsRef.size(), Goal.size(), Tactic.solver(), ExprRef.sort(), BoolRef.sort(), QuantifierRef.sort(), ArithRef.sort(), BitVecRef.sort(), ArrayRef.sort(), DatatypeRef.sort(), FiniteDomainRef.sort(), FPRef.sort(), SeqRef.sort(), Solver.statistics(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), Fixedpoint.to_string(), Solver.trail(), Solver.trail_levels(), AstVector.translate(), FuncInterp.translate(), AstRef.translate(), Goal.translate(), ModelRef.translate(), Solver.translate(), Solver.units(), Solver.unsat_core(), Optimize.unsat_core(), Fixedpoint.update_rule(), ParamsRef.validate(), FuncEntry.value(), QuantifierRef.var_name(), and QuantifierRef.var_sort().
fixedpoint |
Definition at line 7318 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 7324 of file z3py.py.
Referenced by Fixedpoint.abstract(), and Fixedpoint.declare_var().