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 6952 of file z3py.py.
def __del__ | ( | self | ) |
Definition at line 6966 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 7195 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 6998 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 7123 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 7014 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 6984 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 7186 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 7041 of file z3py.py.
def get_answer | ( | self | ) |
Retrieve answer from last query call.
Definition at line 7092 of file z3py.py.
def get_assertions | ( | self | ) |
retrieve assertions that have been added to fixedpoint context
Definition at line 7155 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 7118 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 7114 of file z3py.py.
def get_rule_names_along_trace | ( | self | ) |
retrieve rule names along the counterexample trace
Definition at line 7106 of file z3py.py.
def get_rules | ( | self | ) |
retrieve rules that have been added to fixedpoint context
Definition at line 7151 of file z3py.py.
def get_rules_along_trace | ( | self | ) |
def help | ( | self | ) |
Display a string describing all available options.
Definition at line 6976 of file z3py.py.
def insert | ( | self, | |
* | args | ||
) |
def param_descrs | ( | self | ) |
Return the parameter description set.
Definition at line 6980 of file z3py.py.
def parse_file | ( | self, | |
f | |||
) |
Parse rules and queries from a file
Definition at line 7147 of file z3py.py.
def parse_string | ( | self, | |
s | |||
) |
Parse rules and queries from a string
Definition at line 7143 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 7045 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 7067 of file z3py.py.
def reason_unknown | ( | self | ) |
Return a string describing why the last `query()` returned `unknown`.
Definition at line 7181 of file z3py.py.
def register_relation | ( | self, | |
* | relations | ||
) |
Register relation as recursive
Definition at line 7127 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 7037 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 6970 of file z3py.py.
def set_predicate_representation | ( | self, | |
f, | |||
* | representations | ||
) |
Control how relation is represented
Definition at line 7133 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 7163 of file z3py.py.
Referenced by Fixedpoint.__repr__(), and Optimize.__repr__().
def statistics | ( | self | ) |
Return statistics for the last `query()`.
Definition at line 7176 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 7168 of file z3py.py.
def update_rule | ( | self, | |
head, | |||
body, | |||
name | |||
) |
update rule
Definition at line 7083 of file z3py.py.
ctx |
Definition at line 6954 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(), Solver.consequences(), DatatypeSortRef.constructor(), Goal.convert_model(), AstRef.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(), 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(), 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 6955 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 6961 of file z3py.py.
Referenced by Fixedpoint.abstract(), and Fixedpoint.declare_var().