Public Member Functions | |
__init__ (self, solver=None, ctx=None, logFile=None) | |
__del__ (self) | |
set (self, *args, **keys) | |
push (self) | |
pop (self, num=1) | |
num_scopes (self) | |
reset (self) | |
assert_exprs (self, *args) | |
add (self, *args) | |
__iadd__ (self, fml) | |
append (self, *args) | |
insert (self, *args) | |
assert_and_track (self, a, p) | |
check (self, *assumptions) | |
model (self) | |
import_model_converter (self, other) | |
unsat_core (self) | |
consequences (self, assumptions, variables) | |
from_file (self, filename) | |
from_string (self, s) | |
cube (self, vars=None) | |
cube_vars (self) | |
root (self, t) | |
next (self, t) | |
proof (self) | |
assertions (self) | |
units (self) | |
non_units (self) | |
trail_levels (self) | |
trail (self) | |
statistics (self) | |
reason_unknown (self) | |
help (self) | |
param_descrs (self) | |
__repr__ (self) | |
translate (self, target) | |
__copy__ (self) | |
__deepcopy__ (self, memo={}) | |
sexpr (self) | |
dimacs (self, include_names=True) | |
to_smt2 (self) | |
![]() | |
use_pp (self) | |
Data Fields | |
ctx | |
backtrack_level | |
solver | |
cube_vs | |
Additional Inherited Members | |
![]() | |
_repr_html_ (self) | |
Solver API provides methods for implementing the main SMT 2.0 commands: push, pop, check, get-model, etc.
__init__ | ( | self, | |
solver = None , |
|||
ctx = None , |
|||
logFile = None |
|||
) |
Definition at line 6895 of file z3py.py.
__del__ | ( | self | ) |
Definition at line 6908 of file z3py.py.
__copy__ | ( | self | ) |
__deepcopy__ | ( | self, | |
memo = {} |
|||
) |
__iadd__ | ( | self, | |
fml | |||
) |
__repr__ | ( | self | ) |
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 7020 of file z3py.py.
Referenced by Solver.__iadd__().
append | ( | self, | |
* | args | ||
) |
Assert constraints into the solver. >>> x = Int('x') >>> s = Solver() >>> s.append(x > 0, x < 2) >>> s [x > 0, x < 2]
Definition at line 7035 of file z3py.py.
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 7057 of file z3py.py.
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 7001 of file z3py.py.
Referenced by Goal.add(), Solver.add(), Goal.append(), Solver.append(), Goal.insert(), and Solver.insert().
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 7256 of file z3py.py.
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 7087 of file z3py.py.
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 7171 of file z3py.py.
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 7208 of file z3py.py.
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 7229 of file z3py.py.
dimacs | ( | self, | |
include_names = True |
|||
) |
Return a textual representation of the solver in DIMACS format.
Definition at line 7367 of file z3py.py.
from_file | ( | self, | |
filename | |||
) |
Parse assertions from a file
Definition at line 7200 of file z3py.py.
from_string | ( | self, | |
s | |||
) |
Parse assertions from a string
Definition at line 7204 of file z3py.py.
help | ( | self | ) |
Display a string describing all available options.
Definition at line 7324 of file z3py.py.
import_model_converter | ( | self, | |
other | |||
) |
insert | ( | self, | |
* | args | ||
) |
Assert constraints into the solver. >>> x = Int('x') >>> s = Solver() >>> s.insert(x > 0, x < 2) >>> s [x > 0, x < 2]
Definition at line 7046 of file z3py.py.
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 7116 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(), ModelRef.translate(), and ModelRef.update_value().
next | ( | self, | |
t | |||
) |
Definition at line 7244 of file z3py.py.
non_units | ( | self | ) |
Return an AST vector containing all atomic formulas in solver state that are not units.
Definition at line 7275 of file z3py.py.
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 6969 of file z3py.py.
param_descrs | ( | self | ) |
Return the parameter description set.
Definition at line 7328 of file z3py.py.
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 6947 of file z3py.py.
proof | ( | self | ) |
Return a proof for the last `check()`. Proof construction must be enabled.
Definition at line 7252 of file z3py.py.
push | ( | self | ) |
Create a backtracking point. >>> 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 6925 of file z3py.py.
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 7311 of file z3py.py.
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 6987 of file z3py.py.
root | ( | self, | |
t | |||
) |
Definition at line 7236 of file z3py.py.
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 6912 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. >>> x = Int('x') >>> s = Solver() >>> s.add(x > 0) >>> s.add(x < 2) >>> r = s.sexpr()
Definition at line 7355 of file z3py.py.
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 7293 of file z3py.py.
to_smt2 | ( | self | ) |
return SMTLIB2 formatted benchmark for solver's assertions
Definition at line 7371 of file z3py.py.
trail | ( | self | ) |
Return trail of the solver state after a check() call.
Definition at line 7288 of file z3py.py.
trail_levels | ( | self | ) |
Return trail and decision levels of the solver state after a check() call.
Definition at line 7280 of file z3py.py.
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 7336 of file z3py.py.
Referenced by AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), FuncInterp.__deepcopy__(), and ModelRef.__deepcopy__().
units | ( | self | ) |
Return an AST vector containing all currently inferred units.
Definition at line 7270 of file z3py.py.
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 7139 of file z3py.py.
ctx |
Definition at line 6897 of file z3py.py.
Referenced by ArithRef.__add__(), BitVecRef.__add__(), BitVecRef.__and__(), FuncDeclRef.__call__(), AstMap.__contains__(), AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), AstRef.__deepcopy__(), Datatype.__deepcopy__(), ParamsRef.__deepcopy__(), ParamDescrsRef.__deepcopy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), AstMap.__deepcopy__(), FuncEntry.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), Statistics.__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__(), ArithRef.__div__(), BitVecRef.__div__(), ExprRef.__eq__(), ArithRef.__ge__(), BitVecRef.__ge__(), AstVector.__getitem__(), ModelRef.__getitem__(), Statistics.__getitem__(), AstMap.__getitem__(), ArithRef.__gt__(), BitVecRef.__gt__(), BitVecRef.__invert__(), ArithRef.__le__(), BitVecRef.__le__(), AstVector.__len__(), AstMap.__len__(), ModelRef.__len__(), Statistics.__len__(), BitVecRef.__lshift__(), ArithRef.__lt__(), BitVecRef.__lt__(), ArithRef.__mod__(), BitVecRef.__mod__(), BoolRef.__mul__(), ArithRef.__mul__(), BitVecRef.__mul__(), ExprRef.__ne__(), ArithRef.__neg__(), BitVecRef.__neg__(), BitVecRef.__or__(), ArithRef.__pow__(), ArithRef.__radd__(), BitVecRef.__radd__(), BitVecRef.__rand__(), ArithRef.__rdiv__(), BitVecRef.__rdiv__(), ParamsRef.__repr__(), ParamDescrsRef.__repr__(), AstMap.__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__(), AstVector.__setitem__(), AstMap.__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(), Solver.push(), AstVector.push(), FuncDeclRef.range(), ArraySortRef.range(), DatatypeSortRef.recognizer(), Context.ref(), AstMap.reset(), Solver.reset(), AstVector.resize(), Solver.set(), ParamsRef.set(), Goal.sexpr(), AstVector.sexpr(), ModelRef.sexpr(), ParamDescrsRef.size(), Goal.size(), AstVector.translate(), AstRef.translate(), Goal.translate(), ModelRef.translate(), ParamsRef.validate(), FuncEntry.value(), QuantifierRef.var_name(), and QuantifierRef.var_sort().
solver |
Definition at line 6899 of file z3py.py.
Referenced by Solver.__del__(), Solver.assert_and_track(), Solver.assert_exprs(), Solver.check(), Solver.model(), Solver.num_scopes(), Solver.pop(), Solver.push(), Solver.reset(), and Solver.set().