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 7416 of file z3py.py.
def __del__ | ( | self | ) |
Definition at line 7430 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 7664 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 7462 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 7589 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 7478 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 7448 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 7655 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 7505 of file z3py.py.
def get_answer | ( | self | ) |
Retrieve answer from last query call.
Definition at line 7556 of file z3py.py.
def get_assertions | ( | self | ) |
retrieve assertions that have been added to fixedpoint context
Definition at line 7623 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 7582 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 7578 of file z3py.py.
def get_rule_names_along_trace | ( | self | ) |
retrieve rule names along the counterexample trace
Definition at line 7570 of file z3py.py.
def get_rules | ( | self | ) |
retrieve rules that have been added to fixedpoint context
Definition at line 7619 of file z3py.py.
def get_rules_along_trace | ( | self | ) |
def help | ( | self | ) |
Display a string describing all available options.
Definition at line 7440 of file z3py.py.
def insert | ( | self, | |
* | args | ||
) |
def param_descrs | ( | self | ) |
Return the parameter description set.
Definition at line 7444 of file z3py.py.
def parse_file | ( | self, | |
f | |||
) |
Parse rules and queries from a file
Definition at line 7615 of file z3py.py.
def parse_string | ( | self, | |
s | |||
) |
Parse rules and queries from a string
Definition at line 7611 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 7509 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 7531 of file z3py.py.
def reason_unknown | ( | self | ) |
Return a string describing why the last `query()` returned `unknown`.
Definition at line 7650 of file z3py.py.
def register_relation | ( | self, | |
* | relations | ||
) |
Register relation as recursive
Definition at line 7595 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 7501 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 7434 of file z3py.py.
def set_predicate_representation | ( | self, | |
f, | |||
* | representations | ||
) |
Control how relation is represented
Definition at line 7601 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 7631 of file z3py.py.
Referenced by Fixedpoint.__repr__(), and Optimize.__repr__().
def statistics | ( | self | ) |
Return statistics for the last `query()`.
Definition at line 7645 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 7637 of file z3py.py.
def update_rule | ( | self, | |
head, | |||
body, | |||
name | |||
) |
update rule
Definition at line 7547 of file z3py.py.
ctx |
Definition at line 7418 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__(), 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__(), 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(), ParserContext.add_decl(), Fixedpoint.add_rule(), Optimize.add_soft(), ParserContext.add_sort(), 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(), 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(), Tactic.help(), Solver.import_model_converter(), Goal.inconsistent(), CharRef.is_digit(), 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(), CharRef.to_bv(), CharRef.to_int(), 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 7419 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 7425 of file z3py.py.
Referenced by Fixedpoint.abstract(), and Fixedpoint.declare_var().