|
Z3
|
|
|
Z3
|
|
Inheritance diagram for Solver:Public Member Functions | |
| def | __init__ |
| def | __del__ (self) |
| def | __enter__ (self) |
| def | __exit__ (self, exc_info) |
| def | set (self, args, keys) |
| def | push (self) |
| def | pop |
| 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 | interrupt (self) |
| def | unsat_core (self) |
| def | consequences (self, assumptions, variables) |
| def | from_file (self, filename) |
| def | from_string (self, s) |
| def | cube |
| def | cube_vars (self) |
| def | root (self, t) |
| def | next (self, t) |
| def | explain_congruent (self, a, b) |
| def | solve_for (self, ts) |
| def | proof (self) |
| def | assertions (self) |
| def | units (self) |
| def | non_units (self) |
| def | trail_levels (self) |
| def | set_initial_value (self, var, value) |
| 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__ |
| def | sexpr (self) |
| def | dimacs |
| def | to_smt2 (self) |
| def | solutions (self, t) |
| Public Member Functions inherited from Z3PPObject | |
| 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 __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 7297 of file z3py.py.
Referenced by Solver.__iadd__(), Fixedpoint.__iadd__(), and Optimize.__iadd__().
| def append | ( | self, | |
| args | |||
| ) |
| 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 7334 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 7278 of file z3py.py.
Referenced by Solver.add(), Fixedpoint.add(), Optimize.add(), Solver.append(), Fixedpoint.append(), 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 7559 of file z3py.py.
Referenced by Solver.solutions(), and 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()
sat
Definition at line 7364 of file z3py.py.
Referenced by Solver.model(), Solver.proof(), Solver.reason_unknown(), Solver.statistics(), Solver.trail(), Solver.trail_levels(), and Solver.unsat_core().
| 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 7455 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 7492 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 7513 of file z3py.py.
| def dimacs | ( | self, | |
include_names = True |
|||
| ) |
| def explain_congruent | ( | self, | |
| a, | |||
| b | |||
| ) |
Explain congruence of a and b relative to the current search state
Definition at line 7536 of file z3py.py.
| def from_file | ( | self, | |
| filename | |||
| ) |
| def from_string | ( | self, | |
| s | |||
| ) |
| def help | ( | self | ) |
Display a string describing all available options.
Definition at line 7634 of file z3py.py.
Referenced by Solver.set().
| def import_model_converter | ( | self, | |
| other | |||
| ) |
| def insert | ( | self, | |
| args | |||
| ) |
| def interrupt | ( | self | ) |
Interrupt the execution of the solver object. Remarks: This ensures that the interrupt applies only to the given solver object and it applies only if it is running.
Definition at line 7416 of file z3py.py.
| 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 7393 of file z3py.py.
Referenced by FuncInterp.translate().
| def next | ( | self, | |
| t | |||
| ) |
Retrieve congruence closure sibling of the term t relative to the current search state The function primarily works for SimpleSolver. Terms and variables that are eliminated during pre-processing are not visible to the congruence closure.
Definition at line 7528 of file z3py.py.
| def non_units | ( | self | ) |
Return an AST vector containing all atomic formulas in solver state that are not units.
Definition at line 7578 of file z3py.py.
| 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 7246 of file z3py.py.
| def param_descrs | ( | self | ) |
Return the parameter description set.
Definition at line 7638 of file z3py.py.
| 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 7224 of file z3py.py.
Referenced by Solver.__exit__(), and Optimize.__exit__().
| def proof | ( | self | ) |
| def 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 7202 of file z3py.py.
Referenced by Solver.__enter__(), Optimize.__enter__(), and Solver.reset().
| def reason_unknown | ( | self | ) |
Return a string describing why the last `check()` returned `unknown`.
>>> x = Int('x')
>>> s = SimpleSolver()
>>> s.add(x == 2**x)
>>> s.check()
unknown
>>> s.reason_unknown()
'(incomplete (theory arithmetic))'
Definition at line 7621 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 7264 of file z3py.py.
| def root | ( | self, | |
| t | |||
| ) |
Retrieve congruence closure root of the term t relative to the current search state The function primarily works for SimpleSolver. Terms and variables that are eliminated during pre-processing are not visible to the congruence closure.
Definition at line 7520 of file z3py.py.
| 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 7189 of file z3py.py.
| def set_initial_value | ( | self, | |
| var, | |||
| value | |||
| ) |
initialize the solver's state by setting the initial value of var to value
Definition at line 7591 of file z3py.py.
| def sexpr | ( | self | ) |
Return a formatted string (in Lisp-like format) with all added constraints.
Definition at line 7665 of file z3py.py.
Referenced by Fixedpoint.__repr__(), and Optimize.__repr__().
| def solutions | ( | self, | |
| t | |||
| ) |
Returns an iterator over solutions that satisfy the constraints.
The parameter `t` is an expression whose values should be returned.
>>> s = Solver()
>>> x, y, z = Ints("x y z")
>>> s.add(x * x == 4)
>>> print(list(s.solutions(x)))
[-2, 2]
>>> s.reset()
>>> s.add(x >= 0, x < 10)
>>> print(list(s.solutions(x)))
[0, 1, 2, 3, 4, 5, 6, 7, 8, 9]
>>> s.reset()
>>> s.add(x >= 0, y < 10, y == 2*x)
>>> print(list(s.solutions([x, y])))
[[0, 0], [1, 2], [2, 4], [3, 6], [4, 8]]
Definition at line 7692 of file z3py.py.
| def solve_for | ( | self, | |
| ts | |||
| ) |
Retrieve a solution for t relative to linear equations maintained in the current state.
Definition at line 7543 of file z3py.py.
| 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 7603 of file z3py.py.
| def to_smt2 | ( | self | ) |
return SMTLIB2 formatted benchmark for solver's assertions
Definition at line 7674 of file z3py.py.
| def trail | ( | self | ) |
Return trail of the solver state after a check() call.
Definition at line 7598 of file z3py.py.
| def trail_levels | ( | self | ) |
Return trail and decision levels of the solver state after a check() call.
Definition at line 7583 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 7646 of file z3py.py.
Referenced by Solver.__copy__(), and Solver.__deepcopy__().
| def units | ( | self | ) |
Return an AST vector containing all currently inferred units.
Definition at line 7573 of file z3py.py.
| 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 7423 of file z3py.py.
| ctx |
Definition at line 7167 of file z3py.py.
Referenced by Solver.__copy__(), Solver.__deepcopy__(), Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Simplifier.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), Probe.__ne__(), Simplifier.add(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), ApplyResult.as_expr(), Solver.assert_and_track(), Optimize.assert_and_track(), Solver.assert_exprs(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Solver.assertions(), Optimize.assertions(), Solver.check(), Solver.consequences(), Solver.explain_congruent(), ParserContext.from_string(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_ground_sat_answer(), Fixedpoint.get_rule_names_along_trace(), Fixedpoint.get_rules(), Fixedpoint.get_rules_along_trace(), Solver.model(), Optimize.model(), Solver.next(), Solver.non_units(), Optimize.objectives(), Solver.param_descrs(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Simplifier.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Solver.proof(), Fixedpoint.query(), Solver.root(), Solver.set(), Fixedpoint.set(), Optimize.set(), Optimize.set_on_model(), Solver.solve_for(), Tactic.solver(), Solver.statistics(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), Solver.trail(), Solver.units(), Solver.unsat_core(), Optimize.unsat_core(), Fixedpoint.update_rule(), and Simplifier.using_params().
| cube_vs |
Definition at line 7499 of file z3py.py.
Referenced by Solver.cube_vars().
| solver |
Definition at line 7169 of file z3py.py.
Referenced by Solver.__del__(), Solver.assert_and_track(), Solver.assert_exprs(), Solver.assertions(), Solver.check(), Solver.consequences(), Solver.dimacs(), Solver.explain_congruent(), Solver.from_file(), Solver.from_string(), Solver.help(), Solver.import_model_converter(), Solver.interrupt(), 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.set_initial_value(), Solver.sexpr(), Solver.solve_for(), Solver.statistics(), Solver.trail(), Solver.trail_levels(), Solver.translate(), Solver.units(), and Solver.unsat_core().
1.8.10