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 |
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 |
|||
) |
Definition at line 5718 of file z3py.py.
05718 05719 def __init__(self, solver=None, ctx=None): 05720 assert solver == None or ctx != None 05721 self.ctx = _get_ctx(ctx) 05722 self.solver = None 05723 if solver == None: 05724 self.solver = Z3_mk_solver(self.ctx.ref()) 05725 else: 05726 self.solver = solver 05727 Z3_solver_inc_ref(self.ctx.ref(), self.solver)
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 5821 of file z3py.py.
05821 05822 def add(self, *args): 05823 """Assert constraints into the solver. 05824 05825 >>> x = Int('x') 05826 >>> s = Solver() 05827 >>> s.add(x > 0, x < 2) 05828 >>> s 05829 [x > 0, x < 2] 05830 """ 05831 self.assert_exprs(*args)
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]
Definition at line 5832 of file z3py.py.
05832 05833 def append(self, *args): 05834 """Assert constraints into the solver. 05835 05836 >>> x = Int('x') 05837 >>> s = Solver() 05838 >>> s.append(x > 0, x < 2) 05839 >>> s 05840 [x > 0, x < 2] 05841 """ 05842 self.assert_exprs(*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 5854 of file z3py.py.
05854 05855 def assert_and_track(self, a, p): 05856 """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`. 05857 05858 If `p` is a string, it will be automatically converted into a Boolean constant. 05859 05860 >>> x = Int('x') 05861 >>> p3 = Bool('p3') 05862 >>> s = Solver() 05863 >>> s.set(unsat_core=True) 05864 >>> s.assert_and_track(x > 0, 'p1') 05865 >>> s.assert_and_track(x != 1, 'p2') 05866 >>> s.assert_and_track(x < 0, p3) 05867 >>> print(s.check()) 05868 unsat 05869 >>> c = s.unsat_core() 05870 >>> len(c) 05871 2 05872 >>> Bool('p1') in c 05873 True 05874 >>> Bool('p2') in c 05875 False 05876 >>> p3 in c 05877 True 05878 """ 05879 if isinstance(p, str): 05880 p = Bool(p, self.ctx) 05881 _z3_assert(isinstance(a, BoolRef), "Boolean expression expected") 05882 _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected") 05883 Z3_solver_assert_and_track(self.ctx.ref(), self.solver, a.as_ast(), p.as_ast())
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 5802 of file z3py.py.
Referenced by Solver.add(), Fixedpoint.add(), Solver.append(), Fixedpoint.append(), and Fixedpoint.insert().
05802 05803 def assert_exprs(self, *args): 05804 """Assert constraints into the solver. 05805 05806 >>> x = Int('x') 05807 >>> s = Solver() 05808 >>> s.assert_exprs(x > 0, x < 2) 05809 >>> s 05810 [x > 0, x < 2] 05811 """ 05812 args = _get_args(args) 05813 s = BoolSort(self.ctx) 05814 for arg in args: 05815 if isinstance(arg, Goal) or isinstance(arg, AstVector): 05816 for f in arg: 05817 Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast()) 05818 else: 05819 arg = s.cast(arg) 05820 Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast())
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 5967 of file z3py.py.
Referenced by Solver.to_smt2().
05967 05968 def assertions(self): 05969 """Return an AST vector containing all added constraints. 05970 05971 >>> s = Solver() 05972 >>> s.assertions() 05973 [] 05974 >>> a = Int('a') 05975 >>> s.add(a > 0) 05976 >>> s.add(a < 10) 05977 >>> s.assertions() 05978 [a > 0, a < 10] 05979 """ 05980 return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
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 5884 of file z3py.py.
Referenced by Solver.model(), Solver.proof(), Solver.reason_unknown(), Solver.statistics(), and Solver.unsat_core().
05884 05885 def check(self, *assumptions): 05886 """Check whether the assertions in the given solver plus the optional assumptions are consistent or not. 05887 05888 >>> x = Int('x') 05889 >>> s = Solver() 05890 >>> s.check() 05891 sat 05892 >>> s.add(x > 0, x < 2) 05893 >>> s.check() 05894 sat 05895 >>> s.model() 05896 [x = 1] 05897 >>> s.add(x < 1) 05898 >>> s.check() 05899 unsat 05900 >>> s.reset() 05901 >>> s.add(2**x == 4) 05902 >>> s.check() 05903 unknown 05904 """ 05905 assumptions = _get_args(assumptions) 05906 num = len(assumptions) 05907 _assumptions = (Ast * num)() 05908 for i in range(num): 05909 _assumptions[i] = assumptions[i].as_ast() 05910 r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions) 05911 return CheckSatResult(r)
def help | ( | self | ) |
Display a string describing all available options.
Definition at line 6012 of file z3py.py.
Referenced by Solver.set().
06012 06013 def help(self): 06014 """Display a string describing all available options.""" 06015 print(Z3_solver_get_help(self.ctx.ref(), self.solver))
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]
Definition at line 5843 of file z3py.py.
05843 05844 def insert(self, *args): 05845 """Assert constraints into the solver. 05846 05847 >>> x = Int('x') 05848 >>> s = Solver() 05849 >>> s.insert(x > 0, x < 2) 05850 >>> s 05851 [x > 0, x < 2] 05852 """ 05853 self.assert_exprs(*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 5912 of file z3py.py.
05912 05913 def model(self): 05914 """Return a model for the last `check()`. 05915 05916 This function raises an exception if 05917 a model is not available (e.g., last `check()` returned unsat). 05918 05919 >>> s = Solver() 05920 >>> a = Int('a') 05921 >>> s.add(a + 2 == 0) 05922 >>> s.check() 05923 sat 05924 >>> s.model() 05925 [a = -2] 05926 """ 05927 try: 05928 return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx) 05929 except Z3Exception: 05930 raise Z3Exception("model is not available")
def param_descrs | ( | self | ) |
Return the parameter description set.
Definition at line 6016 of file z3py.py.
06016 06017 def param_descrs(self): 06018 """Return the parameter description set.""" 06019 return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx)
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 5766 of file z3py.py.
05766 05767 def pop(self, num=1): 05768 """Backtrack \c num backtracking points. 05769 05770 >>> x = Int('x') 05771 >>> s = Solver() 05772 >>> s.add(x > 0) 05773 >>> s 05774 [x > 0] 05775 >>> s.push() 05776 >>> s.add(x < 1) 05777 >>> s 05778 [x > 0, x < 1] 05779 >>> s.check() 05780 unsat 05781 >>> s.pop() 05782 >>> s.check() 05783 sat 05784 >>> s 05785 [x > 0] 05786 """ 05787 Z3_solver_pop(self.ctx.ref(), self.solver, num)
def proof | ( | self | ) |
Return a proof for the last `check()`. Proof construction must be enabled.
Definition at line 5963 of file z3py.py.
05963 05964 def proof(self): 05965 """Return a proof for the last `check()`. Proof construction must be enabled.""" 05966 return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
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 5744 of file z3py.py.
Referenced by Solver.reset().
05744 05745 def push(self): 05746 """Create a backtracking point. 05747 05748 >>> x = Int('x') 05749 >>> s = Solver() 05750 >>> s.add(x > 0) 05751 >>> s 05752 [x > 0] 05753 >>> s.push() 05754 >>> s.add(x < 1) 05755 >>> s 05756 [x > 0, x < 1] 05757 >>> s.check() 05758 unsat 05759 >>> s.pop() 05760 >>> s.check() 05761 sat 05762 >>> s 05763 [x > 0] 05764 """ 05765 Z3_solver_push(self.ctx.ref(), self.solver)
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 5999 of file z3py.py.
05999 06000 def reason_unknown(self): 06001 """Return a string describing why the last `check()` returned `unknown`. 06002 06003 >>> x = Int('x') 06004 >>> s = SimpleSolver() 06005 >>> s.add(2**x == 4) 06006 >>> s.check() 06007 unknown 06008 >>> s.reason_unknown() 06009 '(incomplete (theory arithmetic))' 06010 """ 06011 return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver)
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 5788 of file z3py.py.
05788 05789 def reset(self): 05790 """Remove all asserted constraints and backtracking points created using `push()`. 05791 05792 >>> x = Int('x') 05793 >>> s = Solver() 05794 >>> s.add(x > 0) 05795 >>> s 05796 [x > 0] 05797 >>> s.reset() 05798 >>> s 05799 [] 05800 """ 05801 Z3_solver_reset(self.ctx.ref(), self.solver)
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 5732 of file z3py.py.
05732 05733 def set(self, *args, **keys): 05734 """Set a configuration option. The method `help()` return a string containing all available options. 05735 05736 >>> s = Solver() 05737 >>> # The option MBQI can be set using three different approaches. 05738 >>> s.set(mbqi=True) 05739 >>> s.set('MBQI', True) 05740 >>> s.set(':mbqi', True) 05741 """ 05742 p = args2params(args, keys, self.ctx) 05743 Z3_solver_set_params(self.ctx.ref(), self.solver, p.params)
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 6024 of file z3py.py.
Referenced by Fixedpoint.__repr__().
06024 06025 def sexpr(self): 06026 """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format. 06027 06028 >>> x = Int('x') 06029 >>> s = Solver() 06030 >>> s.add(x > 0) 06031 >>> s.add(x < 2) 06032 >>> r = s.sexpr() 06033 """ 06034 return Z3_solver_to_string(self.ctx.ref(), self.solver)
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 5981 of file z3py.py.
05981 05982 def statistics(self): 05983 """Return statistics for the last `check()`. 05984 05985 >>> s = SimpleSolver() 05986 >>> x = Int('x') 05987 >>> s.add(x > 0) 05988 >>> s.check() 05989 sat 05990 >>> st = s.statistics() 05991 >>> st.get_key_value('final checks') 05992 1 05993 >>> len(st) > 0 05994 True 05995 >>> st[0] != 0 05996 True 05997 """ 05998 return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx)
def to_smt2 | ( | self | ) |
return SMTLIB2 formatted benchmark for solver's assertions
Definition at line 6035 of file z3py.py.
06035 06036 def to_smt2(self): 06037 """return SMTLIB2 formatted benchmark for solver's assertions""" 06038 es = self.assertions() 06039 sz = len(es) 06040 sz1 = sz 06041 if sz1 > 0: 06042 sz1 -= 1 06043 v = (Ast * sz1)() 06044 for i in range(sz1): 06045 v[i] = es[i].as_ast() 06046 if sz > 0: 06047 e = es[sz1].as_ast() 06048 else: 06049 e = BoolVal(True, self.ctx).as_ast() 06050 return Z3_benchmark_to_smtlib_string(self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e) 06051 06052
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 5931 of file z3py.py.
05931 05932 def unsat_core(self): 05933 """Return a subset (as an AST vector) of the assumptions provided to the last check(). 05934 05935 These are the assumptions Z3 used in the unsatisfiability proof. 05936 Assumptions are available in Z3. They are used to extract unsatisfiable cores. 05937 They may be also used to "retract" assumptions. Note that, assumptions are not really 05938 "soft constraints", but they can be used to implement them. 05939 05940 >>> p1, p2, p3 = Bools('p1 p2 p3') 05941 >>> x, y = Ints('x y') 05942 >>> s = Solver() 05943 >>> s.add(Implies(p1, x > 0)) 05944 >>> s.add(Implies(p2, y > x)) 05945 >>> s.add(Implies(p2, y < 1)) 05946 >>> s.add(Implies(p3, y > -3)) 05947 >>> s.check(p1, p2, p3) 05948 unsat 05949 >>> core = s.unsat_core() 05950 >>> len(core) 05951 2 05952 >>> p1 in core 05953 True 05954 >>> p2 in core 05955 True 05956 >>> p3 in core 05957 False 05958 >>> # "Retracting" p2 05959 >>> s.check(p1, p3) 05960 sat 05961 """ 05962 return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx)
Definition at line 5718 of file z3py.py.
Referenced by ArithRef::__add__(), BitVecRef::__add__(), BitVecRef::__and__(), FuncDeclRef::__call__(), ArithRef::__div__(), BitVecRef::__div__(), ExprRef::__eq__(), Probe::__eq__(), ArithRef::__ge__(), BitVecRef::__ge__(), Probe::__ge__(), ArrayRef::__getitem__(), ApplyResult::__getitem__(), ArithRef::__gt__(), BitVecRef::__gt__(), Probe::__gt__(), BitVecRef::__invert__(), ArithRef::__le__(), BitVecRef::__le__(), Probe::__le__(), BitVecRef::__lshift__(), ArithRef::__lt__(), BitVecRef::__lt__(), Probe::__lt__(), ArithRef::__mod__(), BitVecRef::__mod__(), ArithRef::__mul__(), BitVecRef::__mul__(), ExprRef::__ne__(), Probe::__ne__(), ArithRef::__neg__(), BitVecRef::__neg__(), BitVecRef::__or__(), ArithRef::__pow__(), ArithRef::__radd__(), BitVecRef::__radd__(), BitVecRef::__rand__(), ArithRef::__rdiv__(), BitVecRef::__rdiv__(), BitVecRef::__rlshift__(), ArithRef::__rmod__(), BitVecRef::__rmod__(), ArithRef::__rmul__(), BitVecRef::__rmul__(), BitVecRef::__ror__(), ArithRef::__rpow__(), BitVecRef::__rrshift__(), BitVecRef::__rshift__(), ArithRef::__rsub__(), BitVecRef::__rsub__(), BitVecRef::__rxor__(), ArithRef::__sub__(), BitVecRef::__sub__(), BitVecRef::__xor__(), DatatypeSortRef::accessor(), Fixedpoint::add_rule(), Tactic::apply(), AlgebraicNumRef::approx(), ExprRef::arg(), ApplyResult::as_expr(), Solver::assert_and_track(), Solver::assert_exprs(), Fixedpoint::assert_exprs(), Solver::assertions(), QuantifierRef::body(), BoolSortRef::cast(), DatatypeSortRef::constructor(), ApplyResult::convert_model(), ExprRef::decl(), RatNumRef::denominator(), FuncDeclRef::domain(), ArraySortRef::domain(), Fixedpoint::get_answer(), Fixedpoint::get_assertions(), Fixedpoint::get_cover_delta(), Fixedpoint::get_rules(), SortRef::kind(), Solver::model(), SortRef::name(), FuncDeclRef::name(), QuantifierRef::no_pattern(), RatNumRef::numerator(), Solver::param_descrs(), Fixedpoint::param_descrs(), Tactic::param_descrs(), Fixedpoint::parse_file(), Fixedpoint::parse_string(), QuantifierRef::pattern(), Solver::proof(), FuncDeclRef::range(), ArraySortRef::range(), DatatypeSortRef::recognizer(), Solver::set(), Fixedpoint::set(), Tactic::solver(), ExprRef::sort(), BoolRef::sort(), QuantifierRef::sort(), ArithRef::sort(), BitVecRef::sort(), ArrayRef::sort(), DatatypeRef::sort(), Solver::statistics(), Fixedpoint::statistics(), Solver::to_smt2(), Solver::unsat_core(), Fixedpoint::update_rule(), QuantifierRef::var_name(), and QuantifierRef::var_sort().
Definition at line 5718 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().