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 5775 of file z3py.py.

---

Constructor & Destructor Documentation

def __init__	(		self,
			solver = None,
			ctx = None
	)

Definition at line 5778 of file z3py.py.

    def __init__(self, solver=None, ctx=None):
        assert solver == None or ctx != None
        self.ctx    = _get_ctx(ctx)
        self.solver = None
        if solver == None:
            self.solver = Z3_mk_solver(self.ctx.ref())
        else:
            self.solver = solver
        Z3_solver_inc_ref(self.ctx.ref(), self.solver)

def __del__

(

self

)

Definition at line 5788 of file z3py.py.

    def __del__(self):
        if self.solver != None:
            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 6080 of file z3py.py.

    def __repr__(self):
        """Return a formatted string with all added constraints."""
        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 5881 of file z3py.py.

    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]
        """
        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 5892 of file z3py.py.

    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]
        """
        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 5914 of file z3py.py.

    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
        """
        if isinstance(p, str):
            p = Bool(p, self.ctx)
        _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
        _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
        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 5862 of file z3py.py.

Referenced by Solver.add(), Fixedpoint.add(), Optimize.add(), Solver.append(), Fixedpoint.append(), and Fixedpoint.insert().

    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]
        """
        args = _get_args(args)
        s    = BoolSort(self.ctx)
        for arg in args:
            if isinstance(arg, Goal) or isinstance(arg, AstVector):
                for f in arg:
                    Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast())
            else:
                arg = s.cast(arg)
                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 6027 of file z3py.py.

Referenced by Solver.to_smt2().

    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]
        """
        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 5944 of file z3py.py.

Referenced by Solver.model(), Solver.proof(), Solver.reason_unknown(), Solver.statistics(), and Solver.unsat_core().

    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
        """
        assumptions = _get_args(assumptions)
        num = len(assumptions)
        _assumptions = (Ast * num)()
        for i in range(num):
            _assumptions[i] = assumptions[i].as_ast()
        r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions)
        return CheckSatResult(r)

def help

(

self

)

Display a string describing all available options.

Definition at line 6072 of file z3py.py.

Referenced by Solver.set().

    def help(self):
        """Display a string describing all available options."""
        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 5903 of file z3py.py.

    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]
        """
        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 5972 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]
        """
        try:
            return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx)
        except Z3Exception:
            raise Z3Exception("model is not available")

def param_descrs

(

self

)

Return the parameter description set.

Definition at line 6076 of file z3py.py.

    def param_descrs(self):
        """Return the parameter description set."""
        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 5826 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]
        """
        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 6023 of file z3py.py.

    def proof(self):
        """Return a proof for the last `check()`. Proof construction must be enabled."""
        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 5804 of file z3py.py.

Referenced by Solver.reset().

    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]
        """
        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 6059 of file z3py.py.

06059 
06060     def reason_unknown(self):
06061         """Return a string describing why the last `check()` returned `unknown`.
06062         
06063         >>> x = Int('x')
06064         >>> s = SimpleSolver()
06065         >>> s.add(2**x == 4)
06066         >>> s.check()
06067         unknown
06068         >>> s.reason_unknown()
06069         '(incomplete (theory arithmetic))'
06070         """
06071         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 5848 of file z3py.py.

05848 
05849     def reset(self):
05850         """Remove all asserted constraints and backtracking points created using `push()`.
05851         
05852         >>> x = Int('x')
05853         >>> s = Solver()
05854         >>> s.add(x > 0)
05855         >>> s
05856         [x > 0]
05857         >>> s.reset()
05858         >>> s
05859         []
05860         """
05861         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 5792 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)
        """
        p = args2params(args, keys, self.ctx)
        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 6084 of file z3py.py.

Referenced by Fixedpoint.__repr__(), and Optimize.__repr__().

    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()
        """
        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 6041 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
        """
        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 6095 of file z3py.py.

    def to_smt2(self):
        """return SMTLIB2 formatted benchmark for solver's assertions"""
        es = self.assertions()
        sz = len(es)
        sz1 = sz
        if sz1 > 0:
            sz1 -= 1
        v = (Ast * sz1)()
        for i in range(sz1):
            v[i] = es[i].as_ast()
        if sz > 0:
            e = es[sz1].as_ast()
        else:
            e = BoolVal(True, self.ctx).as_ast()
        return Z3_benchmark_to_smtlib_string(self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e)

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.

    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
        """
        return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx)

---

Field Documentation

ctx

Definition at line 5778 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(), Optimize::add_soft(), 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(), ArrayRef::mk_default(), Solver::model(), Optimize::model(), SortRef::name(), FuncDeclRef::name(), QuantifierRef::no_pattern(), RatNumRef::numerator(), Solver::param_descrs(), Fixedpoint::param_descrs(), Optimize::param_descrs(), Tactic::param_descrs(), Fixedpoint::parse_file(), Fixedpoint::parse_string(), QuantifierRef::pattern(), Solver::proof(), Fixedpoint::query(), FuncDeclRef::range(), ArraySortRef::range(), DatatypeSortRef::recognizer(), Solver::set(), Fixedpoint::set(), Optimize::set(), Tactic::solver(), ExprRef::sort(), BoolRef::sort(), QuantifierRef::sort(), ArithRef::sort(), BitVecRef::sort(), ArrayRef::sort(), DatatypeRef::sort(), Solver::statistics(), Fixedpoint::statistics(), Optimize::statistics(), Solver::to_smt2(), Solver::unsat_core(), Fixedpoint::update_rule(), QuantifierRef::var_name(), and QuantifierRef::var_sort().

solver

Definition at line 5778 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().