Inheritance diagram for Solver:

Public Member Functions
	__init__ (self, solver=None, ctx=None, logFile=None)

	__del__ (self)

	__enter__ (self)

	__exit__ (self, *exc_info)

	set (self, args, *keys)

	push (self)

	pop (self, num=1)

	num_scopes (self)

	reset (self)

	assert_exprs (self, *args)

	add (self, *args)

	__iadd__ (self, fml)

	append (self, *args)

	insert (self, *args)

	assert_and_track (self, a, p)

	check (self, *assumptions)

	model (self)

	import_model_converter (self, other)

	interrupt (self)

	unsat_core (self)

	consequences (self, assumptions, variables)

	from_file (self, filename)

	from_string (self, s)

	cube (self, vars=None)

	cube_vars (self)

	congruence_root (self, t)

	congruence_next (self, t)

	congruence_explain (self, a, b)

	solve_for (self, ts)

	proof (self)

	assertions (self)

	units (self)

	non_units (self)

	trail_levels (self)

	set_initial_value (self, var, value)

	trail (self)

	statistics (self)

	reason_unknown (self)

	help (self)

	param_descrs (self)

	__repr__ (self)

	translate (self, target)

	__copy__ (self)

	__deepcopy__ (self, memo={})

	sexpr (self)

	dimacs (self, include_names=True)

	to_smt2 (self)

	solutions (self, t)

Public Member Functions inherited from Z3PPObject
	use_pp (self)

Data Fields
	ctx

	backtrack_level

	solver

	cube_vs

Additional Inherited Members
Protected Member Functions inherited from Z3PPObject
	_repr_html_ (self)

Detailed Description

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

Definition at line 7548 of file z3py.py.

Constructor & Destructor Documentation

◆ init()

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

Definition at line 7554 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)
 

◆ del()

__del__ ( self )

Definition at line 7567 of file z3py.py.

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

Member Function Documentation

◆ copy()

__copy__ ( self )

Definition at line 8048 of file z3py.py.

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

◆ deepcopy()

__deepcopy__	(	self,
		memo = `{}`
	)

Definition at line 8051 of file z3py.py.

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

◆ enter()

__enter__ ( self )

Definition at line 7571 of file z3py.py.

    def __enter__(self):
        self.push()
        return self
 

◆ exit()

__exit__	(		self,
		*	exc_info
	)

Definition at line 7575 of file z3py.py.

    def __exit__(self, *exc_info):
        self.pop()
 

◆ iadd()

__iadd__	(	self,
		fml
	)

Definition at line 7697 of file z3py.py.

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

◆ repr()

__repr__ ( self )

Return a formatted string with all added constraints.

Definition at line 8031 of file z3py.py.

    def __repr__(self):
        """Return a formatted string with all added constraints."""
        return obj_to_string(self)
 

◆ add()

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 7686 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)
 

Referenced by Solver.__iadd__().

◆ append()

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 7701 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)
 

◆ assert_and_track()

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

◆ assert_exprs()

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 7667 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]
        """
        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())
 

Referenced by Goal.add(), Solver.add(), Goal.append(), Solver.append(), Goal.insert(), and Solver.insert().

◆ assertions()

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

    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)
 

◆ check()

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

Definition at line 7753 of file z3py.py.

    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()
        sat
        """
        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)
 

◆ congruence_explain()

congruence_explain	(	self,
		a,
		b
	)

Explain congruence of a and b relative to the current search state

Definition at line 7925 of file z3py.py.

    def congruence_explain(self, a, b):
        """Explain congruence of a and b relative to the current search state"""
        a = _py2expr(a, self.ctx)
        b = _py2expr(b, self.ctx)
        return _to_expr_ref(Z3_solver_congruence_explain(self.ctx.ref(), self.solver, a.ast, b.ast), self.ctx)
 
 

◆ congruence_next()

congruence_next	(	self,
		t
	)

Retrieve congruence closure sibling of the term t relative to the current search state
The function primarily works for SimpleSolver. Terms and variables that are
eliminated during pre-processing are not visible to the congruence closure.

Definition at line 7917 of file z3py.py.

    def congruence_next(self, t):
        """Retrieve congruence closure sibling of the term t relative to the current search state
        The function primarily works for SimpleSolver. Terms and variables that are
        eliminated during pre-processing are not visible to the congruence closure.
        """
        t = _py2expr(t, self.ctx)
        return _to_expr_ref(Z3_solver_congruence_next(self.ctx.ref(), self.solver, t.ast), self.ctx)
 

◆ congruence_root()

congruence_root	(	self,
		t
	)

Retrieve congruence closure root of the term t relative to the current search state
The function primarily works for SimpleSolver. Terms and variables that are
eliminated during pre-processing are not visible to the congruence closure.

Definition at line 7909 of file z3py.py.

    def congruence_root(self, t):
        """Retrieve congruence closure root of the term t relative to the current search state
        The function primarily works for SimpleSolver. Terms and variables that are
        eliminated during pre-processing are not visible to the congruence closure.
        """
        t = _py2expr(t, self.ctx)
        return _to_expr_ref(Z3_solver_congruence_root(self.ctx.ref(), self.solver, t.ast), self.ctx)
 

◆ consequences()

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

◆ cube()

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

◆ cube_vars()

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

◆ dimacs()

dimacs	(	self,
		include_names = `True`
	)

Return a textual representation of the solver in DIMACS format.

Definition at line 8059 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)
 

◆ from_file()

from_file	(	self,
		filename
	)

Parse assertions from a file

Definition at line 7873 of file z3py.py.

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

◆ from_string()

from_string	(	self,
		s
	)

Parse assertions from a string

Definition at line 7877 of file z3py.py.

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

◆ help()

help ( self )

Display a string describing all available options.

Definition at line 8023 of file z3py.py.

    def help(self):
        """Display a string describing all available options."""
        print(Z3_solver_get_help(self.ctx.ref(), self.solver))
 

◆ import_model_converter()

import_model_converter	(	self,
		other
	)

Import model converter from other into the current solver

Definition at line 7801 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)
 

◆ insert()

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 7712 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)
 

◆ interrupt()

interrupt ( self )

Interrupt the execution of the solver object.
Remarks: This ensures that the interrupt applies only
to the given solver object and it applies only if it is running.

Definition at line 7805 of file z3py.py.

    def interrupt(self):
        """Interrupt the execution of the solver object.
        Remarks: This ensures that the interrupt applies only
        to the given solver object and it applies only if it is running.
        """
        Z3_solver_interrupt(self.ctx.ref(), self.solver)
 

◆ model()

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 7782 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")
 

Referenced by ModelRef.__del__(), ModelRef.__getitem__(), ModelRef.__len__(), ModelRef.decls(), ModelRef.eval(), ModelRef.get_interp(), ModelRef.get_sort(), ModelRef.get_universe(), ModelRef.num_sorts(), ModelRef.project(), ModelRef.project_with_witness(), ModelRef.sexpr(), ModelRef.translate(), and ModelRef.update_value().

◆ non_units()

non_units ( self )

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

Definition at line 7967 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)
 

◆ num_scopes()

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 7635 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)
 

◆ param_descrs()

param_descrs ( self )

Return the parameter description set.

Definition at line 8027 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)
 

◆ pop()

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 7613 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)
 

Referenced by Solver.__exit__().

◆ proof()

proof ( self )

Return a proof for the last `check()`. Proof construction must be enabled.

Definition at line 7944 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)
 

◆ push()

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

    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)
 

Referenced by Solver.__enter__().

◆ reason_unknown()

reason_unknown ( self )

Return a string describing why the last `check()` returned `unknown`.

>>> x = Int('x')
>>> s = SimpleSolver()
>>> s.add(x == 2**x)
>>> s.check()
unknown
>>> s.reason_unknown()
'(incomplete (theory arithmetic))'

Definition at line 8010 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(x == 2**x)
        >>> s.check()
        unknown
        >>> s.reason_unknown()
        '(incomplete (theory arithmetic))'
        """
        return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver)
 

◆ reset()

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 7653 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)
 

◆ set()

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 7578 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)
 

◆ set_initial_value()

set_initial_value	(	self,
		var,
		value
	)

initialize the solver's state by setting the initial value of var to value

Definition at line 7980 of file z3py.py.

    def set_initial_value(self, var, value):
        """initialize the solver's state by setting the initial value of var to value
        """
        s = var.sort()
        value = s.cast(value)
        Z3_solver_set_initial_value(self.ctx.ref(), self.solver, var.ast, value.ast)
 

◆ sexpr()

sexpr ( self )

Return a formatted string (in Lisp-like format) with all added constraints.

Definition at line 8054 of file z3py.py.

    def sexpr(self):
        """Return a formatted string (in Lisp-like format) with all added constraints.
        """
        return Z3_solver_to_string(self.ctx.ref(), self.solver)
 

◆ solutions()

solutions	(	self,
		t
	)

Returns an iterator over solutions that satisfy the constraints.

The parameter `t` is an expression whose values should be returned.

>>> s = Solver()
>>> x, y, z = Ints("x y z")
>>> s.add(x * x == 4)
>>> print(list(s.solutions(x)))
[-2, 2]
>>> s.reset()
>>> s.add(x >= 0, x < 10)
>>> print(list(s.solutions(x)))
[0, 1, 2, 3, 4, 5, 6, 7, 8, 9]
>>> s.reset()
>>> s.add(x >= 0, y < 10, y == 2*x)
>>> print(list(s.solutions([x, y])))
[[0, 0], [1, 2], [2, 4], [3, 6], [4, 8]]

Definition at line 8081 of file z3py.py.

    def solutions(self, t):
        """Returns an iterator over solutions that satisfy the constraints.
 
        The parameter `t` is an expression whose values should be returned.
 
        >>> s = Solver()
        >>> x, y, z = Ints("x y z")
        >>> s.add(x * x == 4)
        >>> print(list(s.solutions(x)))
        [-2, 2]
        >>> s.reset()
        >>> s.add(x >= 0, x < 10)
        >>> print(list(s.solutions(x)))
        [0, 1, 2, 3, 4, 5, 6, 7, 8, 9]
        >>> s.reset()
        >>> s.add(x >= 0, y < 10, y == 2*x)
        >>> print(list(s.solutions([x, y])))
        [[0, 0], [1, 2], [2, 4], [3, 6], [4, 8]]
        """
        s = Solver()
        s.add(self.assertions())
        t = _get_args(t)
        if isinstance(t, (list, tuple)):
            while s.check() == sat:
                result = [s.model().eval(t_, model_completion=True) for t_ in t]
                yield result
                s.add(Or(t_ != result_ for t_, result_ in zip(t, result)))
        else:
            while s.check() == sat:
                result = s.model().eval(t, model_completion=True)
                yield result
                s.add(t != result)
 
 

◆ solve_for()

solve_for	(	self,
		ts
	)

Retrieve a solution for t relative to linear equations maintained in the current state.

Definition at line 7932 of file z3py.py.

    def solve_for(self, ts):
        """Retrieve a solution for t relative to linear equations maintained in the current state."""
        vars = AstVector(ctx=self.ctx);
        terms = AstVector(ctx=self.ctx);
        guards = AstVector(ctx=self.ctx);
        for t in ts:
            t = _py2expr(t, self.ctx)                
            vars.push(t)
        Z3_solver_solve_for(self.ctx.ref(), self.solver, vars.vector, terms.vector, guards.vector)
        return [(vars[i], terms[i], guards[i]) for i in range(len(vars))]
 
 

◆ statistics()

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 7992 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)
 

◆ to_smt2()

to_smt2 ( self )

return SMTLIB2 formatted benchmark for solver's assertions

Definition at line 8063 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,
        )
 

◆ trail()

trail ( self )

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

Definition at line 7987 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)
 

◆ trail_levels()

trail_levels ( self )

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

Definition at line 7972 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
 

◆ translate()

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

    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)
 

Referenced by AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), FuncInterp.__deepcopy__(), and ModelRef.__deepcopy__().

◆ units()

units ( self )

Return an AST vector containing all currently inferred units.

Definition at line 7962 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)
 

◆ unsat_core()

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

backtrack_level

Definition at line 7557 of file z3py.py.

◆ ctx

ctx

Definition at line 7556 of file z3py.py.

Referenced by ArithRef.__add__(), BitVecRef.__add__(), BitVecRef.__and__(), FuncDeclRef.__call__(), AstMap.__contains__(), AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), AstRef.__deepcopy__(), Datatype.__deepcopy__(), ParamsRef.__deepcopy__(), ParamDescrsRef.__deepcopy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), AstMap.__deepcopy__(), FuncEntry.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), Statistics.__deepcopy__(), Context.__del__(), AstRef.__del__(), ScopedConstructor.__del__(), ScopedConstructorList.__del__(), ParamsRef.__del__(), ParamDescrsRef.__del__(), Goal.__del__(), AstVector.__del__(), AstMap.__del__(), FuncEntry.__del__(), FuncInterp.__del__(), ModelRef.__del__(), Statistics.__del__(), Solver.__del__(), ArithRef.__div__(), BitVecRef.__div__(), ExprRef.__eq__(), ArithRef.__ge__(), BitVecRef.__ge__(), AstVector.__getitem__(), ModelRef.__getitem__(), Statistics.__getitem__(), AstMap.__getitem__(), ArithRef.__gt__(), BitVecRef.__gt__(), BitVecRef.__invert__(), ArithRef.__le__(), BitVecRef.__le__(), AstVector.__len__(), AstMap.__len__(), ModelRef.__len__(), Statistics.__len__(), BitVecRef.__lshift__(), ArithRef.__lt__(), BitVecRef.__lt__(), ArithRef.__mod__(), BitVecRef.__mod__(), BoolRef.__mul__(), ArithRef.__mul__(), BitVecRef.__mul__(), ExprRef.__ne__(), ArithRef.__neg__(), BitVecRef.__neg__(), BitVecRef.__or__(), ArithRef.__pow__(), ArithRef.__radd__(), BitVecRef.__radd__(), BitVecRef.__rand__(), ArithRef.__rdiv__(), BitVecRef.__rdiv__(), ParamsRef.__repr__(), ParamDescrsRef.__repr__(), AstMap.__repr__(), Statistics.__repr__(), BitVecRef.__rlshift__(), ArithRef.__rmod__(), BitVecRef.__rmod__(), ArithRef.__rmul__(), BitVecRef.__rmul__(), BitVecRef.__ror__(), ArithRef.__rpow__(), BitVecRef.__rrshift__(), BitVecRef.__rshift__(), ArithRef.__rsub__(), BitVecRef.__rsub__(), BitVecRef.__rxor__(), AstVector.__setitem__(), AstMap.__setitem__(), ArithRef.__sub__(), BitVecRef.__sub__(), BitVecRef.__xor__(), DatatypeSortRef.accessor(), ExprRef.arg(), FuncEntry.arg_value(), FuncInterp.arity(), Goal.as_expr(), Solver.assert_and_track(), Goal.assert_exprs(), Solver.assert_exprs(), QuantifierRef.body(), FiniteSetSortRef.cast(), Solver.check(), Goal.convert_model(), AstRef.ctx_ref(), ExprRef.decl(), ModelRef.decls(), ArrayRef.default(), RatNumRef.denominator(), Goal.depth(), Goal.dimacs(), FuncDeclRef.domain(), ArraySortRef.domain_n(), FuncInterp.else_value(), FuncInterp.entry(), AstMap.erase(), ModelRef.eval(), Goal.get(), ParamDescrsRef.get_documentation(), ModelRef.get_interp(), Statistics.get_key_value(), ParamDescrsRef.get_kind(), ParamDescrsRef.get_name(), ModelRef.get_sort(), ModelRef.get_universe(), Goal.inconsistent(), AstMap.keys(), Statistics.keys(), Solver.model(), SortRef.name(), QuantifierRef.no_pattern(), FuncEntry.num_args(), FuncInterp.num_entries(), Solver.num_scopes(), ModelRef.num_sorts(), FuncDeclRef.params(), QuantifierRef.pattern(), AlgebraicNumRef.poly(), Solver.pop(), Goal.prec(), ModelRef.project(), ModelRef.project_with_witness(), Solver.push(), AstVector.push(), QuantifierRef.qid(), FuncDeclRef.range(), ArraySortRef.range(), DatatypeSortRef.recognizer(), Context.ref(), AstMap.reset(), Solver.reset(), AstVector.resize(), Solver.set(), ParamsRef.set(), Goal.sexpr(), AstVector.sexpr(), ModelRef.sexpr(), ParamDescrsRef.size(), Goal.size(), QuantifierRef.skolem_id(), AstVector.translate(), AstRef.translate(), Goal.translate(), ModelRef.translate(), ExprRef.update(), DatatypeRef.update_field(), ParamsRef.validate(), FuncEntry.value(), QuantifierRef.var_name(), and QuantifierRef.var_sort().

◆ cube_vs

cube_vs

Definition at line 7888 of file z3py.py.

◆ solver

solver

Definition at line 7558 of file z3py.py.

Referenced by Solver.__del__(), Solver.assert_and_track(), Solver.assert_exprs(), Solver.check(), Solver.model(), Solver.num_scopes(), Solver.pop(), Solver.push(), Solver.reset(), and Solver.set().

Public Member Functions

Data Fields

Additional Inherited Members