Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Data Fields
Solver Class Reference
+ 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

Data Fields

 ctx
 solver

Detailed Description

Solver API provides methods for implementing the main SMT 2.0 commands: push, pop, check, get-model, etc.

Definition at line 5715 of file z3py.py.


Constructor & Destructor Documentation

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)

Definition at line 5728 of file z3py.py.

05728 
05729     def __del__(self):
05730         if self.solver != None:
05731             Z3_solver_dec_ref(self.ctx.ref(), self.solver)


Member Function Documentation

def __repr__ (   self)
Return a formatted string with all added constraints.

Definition at line 6020 of file z3py.py.

06020 
06021     def __repr__(self):
06022         """Return a formatted string with all added constraints."""
06023         return obj_to_string(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)


Field Documentation

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().

 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines