|
Z3
|
|
All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
|
Z3
|
|
Inheritance diagram for Solver:Public Member Functions | |
| def | __init__ |
| def | __del__ |
| def | set |
| def | push |
| def | pop |
| def | reset |
| def | assert_exprs |
| def | add |
| def | append |
| def | insert |
| def | assert_and_track |
| def | check |
| def | model |
| def | unsat_core |
| def | proof |
| def | assertions |
| def | statistics |
| def | reason_unknown |
| def | help |
| def | param_descrs |
| def | __repr__ |
| def | sexpr |
| def | to_smt2 |
| Public Member Functions inherited from Z3PPObject | |
| def | use_pp |
Data Fields | |
| ctx | |
| solver | |
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 |
|||
| ) |
| def __del__ | ( | self | ) |
| def __repr__ | ( | self | ) |
| def add | ( | self, | |
| args | |||
| ) |
| 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 5914 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 5862 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 6027 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()
[x = 1]
>>> s.add(x < 1)
>>> s.check()
unsat
>>> s.reset()
>>> s.add(2**x == 4)
>>> s.check()
unknown
Definition at line 5944 of file z3py.py.
Referenced by Solver.model(), Solver.proof(), Solver.reason_unknown(), Solver.statistics(), and Solver.unsat_core().
| def help | ( | self | ) |
Display a string describing all available options.
Definition at line 6072 of file z3py.py.
Referenced by Solver.set().
| def insert | ( | self, | |
| args | |||
| ) |
| 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 5972 of file z3py.py.
| def param_descrs | ( | self | ) |
Return the parameter description set.
Definition at line 6076 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 5826 of file z3py.py.
| 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 5804 of file z3py.py.
Referenced by Solver.reset().
| 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 6059 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 5848 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 5792 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 6084 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 6041 of file z3py.py.
| def to_smt2 | ( | self | ) |
return SMTLIB2 formatted benchmark for solver's assertions
Definition at line 6095 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 5991 of file z3py.py.
| ctx |
Definition at line 5780 of file z3py.py.
Referenced by Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), Probe.__ne__(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), ApplyResult.as_expr(), Solver.assert_and_track(), Solver.assert_exprs(), Fixedpoint.assert_exprs(), Solver.assertions(), ApplyResult.convert_model(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_rules(), Solver.model(), Optimize.model(), Solver.param_descrs(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Solver.proof(), Fixedpoint.query(), Solver.set(), Fixedpoint.set(), Optimize.set(), Tactic.solver(), Solver.statistics(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), Solver.unsat_core(), and Fixedpoint.update_rule().
| solver |
Definition at line 5781 of file z3py.py.
Referenced by Solver.__del__(), Solver.assert_and_track(), Solver.assert_exprs(), Solver.assertions(), Solver.check(), Solver.help(), Solver.model(), Solver.param_descrs(), Solver.pop(), Solver.proof(), Solver.push(), Solver.reason_unknown(), Solver.reset(), Solver.set(), Solver.sexpr(), Solver.statistics(), and Solver.unsat_core().
1.8.5