Solver Class Reference

Inheritance diagram for Solver:

Public Member Functions
def	__init__
def	__del__ (self)
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	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	proof (self)
def	assertions (self)
def	units (self)
def	non_units (self)
def	trail_levels (self)
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)
Public Member Functions inherited from Z3PPObject
def	use_pp (self)

Data Fields
	ctx
	backtrack_level
	solver
	cube_vs

Detailed Description

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

Definition at line 6798 of file z3py.py.

Constructor & Destructor Documentation

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

Definition at line 6804 of file z3py.py.

    def __init__(self, solver=None, ctx=None, logFile=None):
        assert solver is None or ctx is not None
        self.ctx = _get_ctx(ctx)
        self.backtrack_level = 4000000000
        self.solver = None
        if solver is None:
            self.solver = Z3_mk_solver(self.ctx.ref())
        else:
            self.solver = solver
        Z3_solver_inc_ref(self.ctx.ref(), self.solver)
        if logFile is not None:
            self.set("smtlib2_log", logFile)

def __del__

(

self

)

Definition at line 6817 of file z3py.py.

    def __del__(self):
        if self.solver is not None and self.ctx.ref() is not None:
            Z3_solver_dec_ref(self.ctx.ref(), self.solver)

Member Function Documentation

def __copy__

(

self

)

Definition at line 7242 of file z3py.py.

    def __copy__(self):
        return self.translate(self.ctx)

def __deepcopy__	(		self,
			memo = {}
	)

Definition at line 7245 of file z3py.py.

    def __deepcopy__(self, memo={}):
        return self.translate(self.ctx)

def __iadd__	(		self,
			fml
	)

Definition at line 6940 of file z3py.py.

    def __iadd__(self, fml):
        self.add(fml)
        return self

def __repr__

(

self

)

Return a formatted string with all added constraints.

Definition at line 7225 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 6929 of file z3py.py.

Referenced by Solver.__iadd__(), Fixedpoint.__iadd__(), and Optimize.__iadd__().

    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 6944 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 6966 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 6910 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 7149 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().eval(x)
1
>>> s.add(x < 1)
>>> s.check()
unsat
>>> s.reset()
>>> s.add(2**x == 4)
>>> s.check()
unknown

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

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

    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))])
        """
        if isinstance(assumptions, list):
            _asms = AstVector(None, self.ctx)
            for a in assumptions:
                _asms.push(a)
            assumptions = _asms
        if isinstance(variables, list):
            _vars = AstVector(None, self.ctx)
            for a in variables:
                _vars.push(a)
            variables = _vars
        _z3_assert(isinstance(assumptions, AstVector), "ast vector expected")
        _z3_assert(isinstance(variables, AstVector), "ast vector expected")
        consequences = AstVector(None, self.ctx)
        r = Z3_solver_get_consequences(self.ctx.ref(), self.solver, assumptions.vector,
                                       variables.vector, consequences.vector)
        sz = len(consequences)
        consequences = [consequences[i] for i in range(sz)]
        return CheckSatResult(r), consequences

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 7117 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.
        """
        self.cube_vs = AstVector(None, self.ctx)
        if vars is not None:
            for v in vars:
                self.cube_vs.push(v)
        while True:
            lvl = self.backtrack_level
            self.backtrack_level = 4000000000
            r = AstVector(Z3_solver_cube(self.ctx.ref(), self.solver, self.cube_vs.vector, lvl), self.ctx)
            if (len(r) == 1 and is_false(r[0])):
                return
            yield r
            if (len(r) == 0):
                return

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 7138 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."""
        return self.cube_vs

def dimacs	(		self,
			include_names = True
	)

Return a textual representation of the solver in DIMACS format.

Definition at line 7260 of file z3py.py.

    def dimacs(self, include_names=True):
        """Return a textual representation of the solver in DIMACS format."""
        return Z3_solver_to_dimacs_string(self.ctx.ref(), self.solver, include_names)

def from_file	(		self,
			filename
	)

Parse assertions from a file

Definition at line 7109 of file z3py.py.

    def from_file(self, filename):
        """Parse assertions from a file"""
        Z3_solver_from_file(self.ctx.ref(), self.solver, filename)

def from_string	(		self,
			s
	)

Parse assertions from a string

Definition at line 7113 of file z3py.py.

    def from_string(self, s):
        """Parse assertions from a string"""
        Z3_solver_from_string(self.ctx.ref(), self.solver, s)

def help

(

self

)

Display a string describing all available options.

Definition at line 7217 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 import_model_converter	(		self,
			other
	)

Import model converter from other into the current solver

Definition at line 7044 of file z3py.py.

    def import_model_converter(self, other):
        """Import model converter from other into the current solver"""
        Z3_solver_import_model_converter(self.ctx.ref(), other.solver, 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 6955 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 7025 of file z3py.py.

Referenced by FuncInterp.translate().

    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 non_units

(

self

)

Return an AST vector containing all atomic formulas in solver state that are not units.

Definition at line 7168 of file z3py.py.

    def non_units(self):
        """Return an AST vector containing all atomic formulas in solver state that are not units.
        """
        return AstVector(Z3_solver_get_non_units(self.ctx.ref(), self.solver), self.ctx)

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

def param_descrs

(

self

)

Return the parameter description set.

Definition at line 7221 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 6856 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 7145 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 6834 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 7204 of file z3py.py.

    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))'
        """
        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 6896 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
        []
        """
        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 6821 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 7248 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 7186 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 7264 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 trail

(

self

)

Return trail of the solver state after a check() call.

Definition at line 7181 of file z3py.py.

    def trail(self):
        """Return trail of the solver state after a check() call.
        """
        return AstVector(Z3_solver_get_trail(self.ctx.ref(), self.solver), self.ctx)

def trail_levels

(

self

)

Return trail and decision levels of the solver state after a check() call.

Definition at line 7173 of file z3py.py.

    def trail_levels(self):
        """Return trail and decision levels of the solver state after a check() call.
        """
        trail = self.trail()
        levels = (ctypes.c_uint * len(trail))()
        Z3_solver_get_levels(self.ctx.ref(), self.solver, trail.vector, len(trail), levels)
        return trail, levels

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

Referenced by Solver.__copy__(), and Solver.__deepcopy__().

    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)
        """
        if z3_debug():
            _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
        solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref())
        return Solver(solver, target)

def units

(

self

)

Return an AST vector containing all currently inferred units.

Definition at line 7163 of file z3py.py.

    def units(self):
        """Return an AST vector containing all currently inferred units.
        """
        return AstVector(Z3_solver_get_units(self.ctx.ref(), self.solver), self.ctx)

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 7048 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

backtrack_level

Definition at line 6807 of file z3py.py.

ctx

Definition at line 6806 of file z3py.py.

Referenced by Solver.__copy__(), Solver.__deepcopy__(), Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), 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(), Optimize.assert_and_track(), Solver.assert_exprs(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Solver.assertions(), Optimize.assertions(), Solver.check(), Solver.consequences(), 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.non_units(), Optimize.objectives(), 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(), Optimize.set_on_model(), Tactic.solver(), Solver.statistics(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), Solver.trail(), Solver.units(), Solver.unsat_core(), Optimize.unsat_core(), and Fixedpoint.update_rule().

cube_vs

Definition at line 7124 of file z3py.py.

Referenced by Solver.cube_vars().

solver

Definition at line 6808 of file z3py.py.

Referenced by Solver.__del__(), Solver.assert_and_track(), Solver.assert_exprs(), Solver.assertions(), Solver.check(), Solver.consequences(), Solver.dimacs(), Solver.from_file(), Solver.from_string(), Solver.help(), Solver.import_model_converter(), Solver.model(), Solver.non_units(), Solver.num_scopes(), Solver.param_descrs(), Solver.pop(), Solver.proof(), Solver.push(), Solver.reason_unknown(), Solver.reset(), Solver.set(), Solver.sexpr(), Solver.statistics(), Solver.trail(), Solver.trail_levels(), Solver.translate(), Solver.units(), and Solver.unsat_core().