Public Member Functions | |
def | __init__ (self, solver=None, ctx=None, logFile=None) |
def | __del__ (self) |
def | set (self, *args, **keys) |
def | push (self) |
def | pop (self, num=1) |
def | num_scopes (self) |
def | reset (self) |
def | assert_exprs (self, *args) |
def | add (self, *args) |
def | __iadd__ (self, fml) |
def | append (self, *args) |
def | insert (self, *args) |
def | assert_and_track (self, a, p) |
def | check (self, *assumptions) |
def | model (self) |
def | import_model_converter (self, other) |
def | unsat_core (self) |
def | consequences (self, assumptions, variables) |
def | from_file (self, filename) |
def | from_string (self, s) |
def | cube (self, vars=None) |
def | cube_vars (self) |
def | root (self, t) |
def | next (self, t) |
def | proof (self) |
def | assertions (self) |
def | units (self) |
def | non_units (self) |
def | trail_levels (self) |
def | trail (self) |
def | statistics (self) |
def | reason_unknown (self) |
def | help (self) |
def | param_descrs (self) |
def | __repr__ (self) |
def | translate (self, target) |
def | __copy__ (self) |
def | __deepcopy__ (self, memo={}) |
def | sexpr (self) |
def | dimacs (self, include_names=True) |
def | to_smt2 (self) |
![]() | |
def | use_pp (self) |
Data Fields | |
ctx | |
backtrack_level | |
solver | |
cube_vs | |
Solver API provides methods for implementing the main SMT 2.0 commands: push, pop, check, get-model, etc.
def __init__ | ( | self, | |
solver = None , |
|||
ctx = None , |
|||
logFile = None |
|||
) |
def __del__ | ( | self | ) |
def __copy__ | ( | self | ) |
def __deepcopy__ | ( | self, | |
memo = {} |
|||
) |
def __iadd__ | ( | self, | |
fml | |||
) |
def __repr__ | ( | self | ) |
def add | ( | self, | |
* | args | ||
) |
Assert constraints into the solver. >>> x = Int('x') >>> s = Solver() >>> s.add(x > 0, x < 2) >>> s [x > 0, x < 2]
Definition at line 7028 of file z3py.py.
Referenced by Solver.__iadd__(), Fixedpoint.__iadd__(), and Optimize.__iadd__().
def append | ( | self, | |
* | args | ||
) |
Assert constraints into the solver. >>> x = Int('x') >>> s = Solver() >>> s.append(x > 0, x < 2) >>> s [x > 0, x < 2]
def assert_and_track | ( | self, | |
a, | |||
p | |||
) |
Assert constraint `a` and track it in the unsat core using the Boolean constant `p`. If `p` is a string, it will be automatically converted into a Boolean constant. >>> x = Int('x') >>> p3 = Bool('p3') >>> s = Solver() >>> s.set(unsat_core=True) >>> s.assert_and_track(x > 0, 'p1') >>> s.assert_and_track(x != 1, 'p2') >>> s.assert_and_track(x < 0, p3) >>> print(s.check()) unsat >>> c = s.unsat_core() >>> len(c) 2 >>> Bool('p1') in c True >>> Bool('p2') in c False >>> p3 in c True
Definition at line 7065 of file z3py.py.
def assert_exprs | ( | self, | |
* | args | ||
) |
Assert constraints into the solver. >>> x = Int('x') >>> s = Solver() >>> s.assert_exprs(x > 0, x < 2) >>> s [x > 0, x < 2]
Definition at line 7009 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 assertions | ( | self | ) |
Return an AST vector containing all added constraints. >>> s = Solver() >>> s.assertions() [] >>> a = Int('a') >>> s.add(a > 0) >>> s.add(a < 10) >>> s.assertions() [a > 0, a < 10]
Definition at line 7264 of file z3py.py.
Referenced by Solver.to_smt2().
def check | ( | self, | |
* | assumptions | ||
) |
Check whether the assertions in the given solver plus the optional assumptions are consistent or not. >>> x = Int('x') >>> s = Solver() >>> s.check() sat >>> s.add(x > 0, x < 2) >>> s.check() sat >>> s.model().eval(x) 1 >>> s.add(x < 1) >>> s.check() unsat >>> s.reset() >>> s.add(2**x == 4) >>> s.check() unknown
Definition at line 7095 of file z3py.py.
def consequences | ( | self, | |
assumptions, | |||
variables | |||
) |
Determine fixed values for the variables based on the solver state and assumptions. >>> s = Solver() >>> a, b, c, d = Bools('a b c d') >>> s.add(Implies(a,b), Implies(b, c)) >>> s.consequences([a],[b,c,d]) (sat, [Implies(a, b), Implies(a, c)]) >>> s.consequences([Not(c),d],[a,b,c,d]) (sat, [Implies(d, d), Implies(Not(c), Not(c)), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))])
Definition at line 7179 of file z3py.py.
def cube | ( | self, | |
vars = None |
|||
) |
Get set of cubes The method takes an optional set of variables that restrict which variables may be used as a starting point for cubing. If vars is not None, then the first case split is based on a variable in this set.
Definition at line 7216 of file z3py.py.
def cube_vars | ( | self | ) |
Access the set of variables that were touched by the most recently generated cube. This set of variables can be used as a starting point for additional cubes. The idea is that variables that appear in clauses that are reduced by the most recent cube are likely more useful to cube on.
Definition at line 7237 of file z3py.py.
def dimacs | ( | self, | |
include_names = True |
|||
) |
def from_file | ( | self, | |
filename | |||
) |
def from_string | ( | self, | |
s | |||
) |
def help | ( | self | ) |
def import_model_converter | ( | self, | |
other | |||
) |
def insert | ( | self, | |
* | args | ||
) |
Assert constraints into the solver. >>> x = Int('x') >>> s = Solver() >>> s.insert(x > 0, x < 2) >>> s [x > 0, x < 2]
def model | ( | self | ) |
Return a model for the last `check()`. This function raises an exception if a model is not available (e.g., last `check()` returned unsat). >>> s = Solver() >>> a = Int('a') >>> s.add(a + 2 == 0) >>> s.check() sat >>> s.model() [a = -2]
Definition at line 7124 of file z3py.py.
Referenced by ModelRef.__del__(), ModelRef.__getitem__(), ModelRef.__len__(), ModelRef.decls(), ModelRef.eval(), ModelRef.get_interp(), ModelRef.get_sort(), ModelRef.get_universe(), ModelRef.num_sorts(), ModelRef.sexpr(), FuncInterp.translate(), ModelRef.translate(), and ModelRef.update_value().
def next | ( | self, | |
t | |||
) |
def non_units | ( | self | ) |
def num_scopes | ( | self | ) |
Return the current number of backtracking points. >>> s = Solver() >>> s.num_scopes() 0 >>> s.push() >>> s.num_scopes() 1 >>> s.push() >>> s.num_scopes() 2 >>> s.pop() >>> s.num_scopes() 1
Definition at line 6977 of file z3py.py.
def param_descrs | ( | self | ) |
def pop | ( | self, | |
num = 1 |
|||
) |
Backtrack \\c num backtracking points. >>> x = Int('x') >>> s = Solver() >>> s.add(x > 0) >>> s [x > 0] >>> s.push() >>> s.add(x < 1) >>> s [x > 0, x < 1] >>> s.check() unsat >>> s.pop() >>> s.check() sat >>> s [x > 0]
Definition at line 6955 of file z3py.py.
def proof | ( | self | ) |
def push | ( | self | ) |
def reason_unknown | ( | self | ) |
Return a string describing why the last `check()` returned `unknown`. >>> x = Int('x') >>> s = SimpleSolver() >>> s.add(2**x == 4) >>> s.check() unknown >>> s.reason_unknown() '(incomplete (theory arithmetic))'
Definition at line 7319 of file z3py.py.
def reset | ( | self | ) |
Remove all asserted constraints and backtracking points created using `push()`. >>> x = Int('x') >>> s = Solver() >>> s.add(x > 0) >>> s [x > 0] >>> s.reset() >>> s []
Definition at line 6995 of file z3py.py.
def root | ( | self, | |
t | |||
) |
def set | ( | self, | |
* | args, | ||
** | keys | ||
) |
Set a configuration option. The method `help()` return a string containing all available options. >>> s = Solver() >>> # The option MBQI can be set using three different approaches. >>> s.set(mbqi=True) >>> s.set('MBQI', True) >>> s.set(':mbqi', True)
Definition at line 6920 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. >>> x = Int('x') >>> s = Solver() >>> s.add(x > 0) >>> s.add(x < 2) >>> r = s.sexpr()
Definition at line 7363 of file z3py.py.
Referenced by Fixedpoint.__repr__(), and Optimize.__repr__().
def statistics | ( | self | ) |
Return statistics for the last `check()`. >>> s = SimpleSolver() >>> x = Int('x') >>> s.add(x > 0) >>> s.check() sat >>> st = s.statistics() >>> st.get_key_value('final checks') 1 >>> len(st) > 0 True >>> st[0] != 0 True
Definition at line 7301 of file z3py.py.
def to_smt2 | ( | self | ) |
return SMTLIB2 formatted benchmark for solver's assertions
Definition at line 7379 of file z3py.py.
def trail | ( | self | ) |
Return trail of the solver state after a check() call.
Definition at line 7296 of file z3py.py.
Referenced by Solver.trail_levels().
def trail_levels | ( | self | ) |
Return trail and decision levels of the solver state after a check() call.
Definition at line 7288 of file z3py.py.
def translate | ( | self, | |
target | |||
) |
Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`. >>> c1 = Context() >>> c2 = Context() >>> s1 = Solver(ctx=c1) >>> s2 = s1.translate(c2)
Definition at line 7344 of file z3py.py.
Referenced by AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), Solver.__copy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), and Solver.__deepcopy__().
def units | ( | self | ) |
def unsat_core | ( | self | ) |
Return a subset (as an AST vector) of the assumptions provided to the last check(). These are the assumptions Z3 used in the unsatisfiability proof. Assumptions are available in Z3. They are used to extract unsatisfiable cores. They may be also used to "retract" assumptions. Note that, assumptions are not really "soft constraints", but they can be used to implement them. >>> p1, p2, p3 = Bools('p1 p2 p3') >>> x, y = Ints('x y') >>> s = Solver() >>> s.add(Implies(p1, x > 0)) >>> s.add(Implies(p2, y > x)) >>> s.add(Implies(p2, y < 1)) >>> s.add(Implies(p3, y > -3)) >>> s.check(p1, p2, p3) unsat >>> core = s.unsat_core() >>> len(core) 2 >>> p1 in core True >>> p2 in core True >>> p3 in core False >>> # "Retracting" p2 >>> s.check(p1, p3) sat
Definition at line 7147 of file z3py.py.
ctx |
Definition at line 6905 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__(), 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(), 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(), Solver.next(), 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.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.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().
cube_vs |
Definition at line 7223 of file z3py.py.
Referenced by Solver.cube_vars().
solver |
Definition at line 6907 of file z3py.py.
Referenced by Solver.__del__(), UserPropagateBase.add(), UserPropagateBase.add_created(), UserPropagateBase.add_decide(), UserPropagateBase.add_diseq(), UserPropagateBase.add_eq(), UserPropagateBase.add_final(), UserPropagateBase.add_fixed(), Solver.assert_and_track(), Solver.assert_exprs(), Solver.assertions(), Solver.check(), Solver.consequences(), UserPropagateBase.ctx(), Solver.dimacs(), Solver.from_file(), Solver.from_string(), Solver.help(), Solver.import_model_converter(), Solver.model(), Solver.next(), Solver.non_units(), Solver.num_scopes(), Solver.param_descrs(), Solver.pop(), Solver.proof(), Solver.push(), Solver.reason_unknown(), Solver.reset(), Solver.root(), Solver.set(), Solver.sexpr(), Solver.statistics(), Solver.trail(), Solver.trail_levels(), Solver.translate(), Solver.units(), and Solver.unsat_core().