Z3
 
Loading...
Searching...
No Matches
Solver Class Reference
+ 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)
 
 root (self, t)
 
 next (self, t)
 
 solve_for (self, t)
 
 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)
 
- Public Member Functions inherited from Z3PPObject
 use_pp (self)
 

Data Fields

 ctx = _get_ctx(ctx)
 
int backtrack_level = 4000000000
 
 solver = None
 
 cube_vs = AstVector(None, self.ctx)
 

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

Constructor & Destructor Documentation

◆ __init__()

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

Definition at line 6983 of file z3py.py.

6983 def __init__(self, solver=None, ctx=None, logFile=None):
6984 assert solver is None or ctx is not None
6985 self.ctx = _get_ctx(ctx)
6986 self.backtrack_level = 4000000000
6987 self.solver = None
6988 if solver is None:
6989 self.solver = Z3_mk_solver(self.ctx.ref())
6990 else:
6991 self.solver = solver
6992 Z3_solver_inc_ref(self.ctx.ref(), self.solver)
6993 if logFile is not None:
6994 self.set("smtlib2_log", logFile)
6995
Z3_solver Z3_API Z3_mk_solver(Z3_context c)
Create a new solver. This solver is a "combined solver" (see combined_solver module) that internally ...
void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s)
Increment the reference counter of the given solver.

◆ __del__()

__del__ ( self)

Definition at line 6996 of file z3py.py.

6996 def __del__(self):
6997 if self.solver is not None and self.ctx.ref() is not None and Z3_solver_dec_ref is not None:
6998 Z3_solver_dec_ref(self.ctx.ref(), self.solver)
6999
void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s)
Decrement the reference counter of the given solver.

Member Function Documentation

◆ __copy__()

__copy__ ( self)

Definition at line 7464 of file z3py.py.

7464 def __copy__(self):
7465 return self.translate(self.ctx)
7466

◆ __deepcopy__()

__deepcopy__ ( self,
memo = {} )

Definition at line 7467 of file z3py.py.

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

◆ __enter__()

__enter__ ( self)

Definition at line 7000 of file z3py.py.

7000 def __enter__(self):
7001 self.push()
7002 return self
7003

◆ __exit__()

__exit__ ( self,
* exc_info )

Definition at line 7004 of file z3py.py.

7004 def __exit__(self, *exc_info):
7005 self.pop()
7006

◆ __iadd__()

__iadd__ ( self,
fml )

Definition at line 7126 of file z3py.py.

7126 def __iadd__(self, fml):
7127 self.add(fml)
7128 return self
7129

◆ __repr__()

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

Definition at line 7447 of file z3py.py.

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

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

7115 def add(self, *args):
7116 """Assert constraints into the solver.
7117
7118 >>> x = Int('x')
7119 >>> s = Solver()
7120 >>> s.add(x > 0, x < 2)
7121 >>> s
7122 [x > 0, x < 2]
7123 """
7124 self.assert_exprs(*args)
7125

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

7130 def append(self, *args):
7131 """Assert constraints into the solver.
7132
7133 >>> x = Int('x')
7134 >>> s = Solver()
7135 >>> s.append(x > 0, x < 2)
7136 >>> s
7137 [x > 0, x < 2]
7138 """
7139 self.assert_exprs(*args)
7140

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

7152 def assert_and_track(self, a, p):
7153 """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
7154
7155 If `p` is a string, it will be automatically converted into a Boolean constant.
7156
7157 >>> x = Int('x')
7158 >>> p3 = Bool('p3')
7159 >>> s = Solver()
7160 >>> s.set(unsat_core=True)
7161 >>> s.assert_and_track(x > 0, 'p1')
7162 >>> s.assert_and_track(x != 1, 'p2')
7163 >>> s.assert_and_track(x < 0, p3)
7164 >>> print(s.check())
7165 unsat
7166 >>> c = s.unsat_core()
7167 >>> len(c)
7168 2
7169 >>> Bool('p1') in c
7170 True
7171 >>> Bool('p2') in c
7172 False
7173 >>> p3 in c
7174 True
7175 """
7176 if isinstance(p, str):
7177 p = Bool(p, self.ctx)
7178 _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
7179 _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
7180 Z3_solver_assert_and_track(self.ctx.ref(), self.solver, a.as_ast(), p.as_ast())
7181
void Z3_API Z3_solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p)
Assert a constraint a into the solver, and track it (in the unsat) core using the Boolean constant p.

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

7096 def assert_exprs(self, *args):
7097 """Assert constraints into the solver.
7098
7099 >>> x = Int('x')
7100 >>> s = Solver()
7101 >>> s.assert_exprs(x > 0, x < 2)
7102 >>> s
7103 [x > 0, x < 2]
7104 """
7105 args = _get_args(args)
7106 s = BoolSort(self.ctx)
7107 for arg in args:
7108 if isinstance(arg, Goal) or isinstance(arg, AstVector):
7109 for f in arg:
7110 Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast())
7111 else:
7112 arg = s.cast(arg)
7113 Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast())
7114
void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a)
Assert a constraint into the solver.

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

7364 def assertions(self):
7365 """Return an AST vector containing all added constraints.
7366
7367 >>> s = Solver()
7368 >>> s.assertions()
7369 []
7370 >>> a = Int('a')
7371 >>> s.add(a > 0)
7372 >>> s.add(a < 10)
7373 >>> s.assertions()
7374 [a > 0, a < 10]
7375 """
7376 return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
7377
Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s)
Return the set of asserted formulas on the solver.

◆ 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()
unknown

Definition at line 7182 of file z3py.py.

7182 def check(self, *assumptions):
7183 """Check whether the assertions in the given solver plus the optional assumptions are consistent or not.
7184
7185 >>> x = Int('x')
7186 >>> s = Solver()
7187 >>> s.check()
7188 sat
7189 >>> s.add(x > 0, x < 2)
7190 >>> s.check()
7191 sat
7192 >>> s.model().eval(x)
7193 1
7194 >>> s.add(x < 1)
7195 >>> s.check()
7196 unsat
7197 >>> s.reset()
7198 >>> s.add(2**x == 4)
7199 >>> s.check()
7200 unknown
7201 """
7202 s = BoolSort(self.ctx)
7203 assumptions = _get_args(assumptions)
7204 num = len(assumptions)
7205 _assumptions = (Ast * num)()
7206 for i in range(num):
7207 _assumptions[i] = s.cast(assumptions[i]).as_ast()
7208 r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions)
7209 return CheckSatResult(r)
7210
Z3_lbool Z3_API Z3_solver_check_assumptions(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[])
Check whether the assertions in the given solver and optional assumptions are consistent or not.

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

7273 def consequences(self, assumptions, variables):
7274 """Determine fixed values for the variables based on the solver state and assumptions.
7275 >>> s = Solver()
7276 >>> a, b, c, d = Bools('a b c d')
7277 >>> s.add(Implies(a,b), Implies(b, c))
7278 >>> s.consequences([a],[b,c,d])
7279 (sat, [Implies(a, b), Implies(a, c)])
7280 >>> s.consequences([Not(c),d],[a,b,c,d])
7281 (sat, [Implies(d, d), Implies(Not(c), Not(c)), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))])
7282 """
7283 if isinstance(assumptions, list):
7284 _asms = AstVector(None, self.ctx)
7285 for a in assumptions:
7286 _asms.push(a)
7287 assumptions = _asms
7288 if isinstance(variables, list):
7289 _vars = AstVector(None, self.ctx)
7290 for a in variables:
7291 _vars.push(a)
7292 variables = _vars
7293 _z3_assert(isinstance(assumptions, AstVector), "ast vector expected")
7294 _z3_assert(isinstance(variables, AstVector), "ast vector expected")
7295 consequences = AstVector(None, self.ctx)
7296 r = Z3_solver_get_consequences(self.ctx.ref(), self.solver, assumptions.vector,
7297 variables.vector, consequences.vector)
7298 sz = len(consequences)
7299 consequences = [consequences[i] for i in range(sz)]
7300 return CheckSatResult(r), consequences
7301
Z3_lbool Z3_API Z3_solver_get_consequences(Z3_context c, Z3_solver s, Z3_ast_vector assumptions, Z3_ast_vector variables, Z3_ast_vector consequences)
retrieve consequences from solver that determine values of the supplied function symbols.

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

7310 def cube(self, vars=None):
7311 """Get set of cubes
7312 The method takes an optional set of variables that restrict which
7313 variables may be used as a starting point for cubing.
7314 If vars is not None, then the first case split is based on a variable in
7315 this set.
7316 """
7317 self.cube_vs = AstVector(None, self.ctx)
7318 if vars is not None:
7319 for v in vars:
7320 self.cube_vs.push(v)
7321 while True:
7322 lvl = self.backtrack_level
7323 self.backtrack_level = 4000000000
7324 r = AstVector(Z3_solver_cube(self.ctx.ref(), self.solver, self.cube_vs.vector, lvl), self.ctx)
7325 if (len(r) == 1 and is_false(r[0])):
7326 return
7327 yield r
7328 if (len(r) == 0):
7329 return
7330
Z3_ast_vector Z3_API Z3_solver_cube(Z3_context c, Z3_solver s, Z3_ast_vector vars, unsigned backtrack_level)
extract a next cube for a solver. The last cube is the constant true or false. The number of (non-con...

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

7331 def cube_vars(self):
7332 """Access the set of variables that were touched by the most recently generated cube.
7333 This set of variables can be used as a starting point for additional cubes.
7334 The idea is that variables that appear in clauses that are reduced by the most recent
7335 cube are likely more useful to cube on."""
7336 return self.cube_vs
7337

◆ dimacs()

dimacs ( self,
include_names = True )
Return a textual representation of the solver in DIMACS format.

Definition at line 7482 of file z3py.py.

7482 def dimacs(self, include_names=True):
7483 """Return a textual representation of the solver in DIMACS format."""
7484 return Z3_solver_to_dimacs_string(self.ctx.ref(), self.solver, include_names)
7485
Z3_string Z3_API Z3_solver_to_dimacs_string(Z3_context c, Z3_solver s, bool include_names)
Convert a solver into a DIMACS formatted string.

◆ from_file()

from_file ( self,
filename )
Parse assertions from a file

Definition at line 7302 of file z3py.py.

7302 def from_file(self, filename):
7303 """Parse assertions from a file"""
7304 Z3_solver_from_file(self.ctx.ref(), self.solver, filename)
7305
void Z3_API Z3_solver_from_file(Z3_context c, Z3_solver s, Z3_string file_name)
load solver assertions from a file.

◆ from_string()

from_string ( self,
s )
Parse assertions from a string

Definition at line 7306 of file z3py.py.

7306 def from_string(self, s):
7307 """Parse assertions from a string"""
7308 Z3_solver_from_string(self.ctx.ref(), self.solver, s)
7309
void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string str)
load solver assertions from a string.

◆ help()

help ( self)
Display a string describing all available options.

Definition at line 7439 of file z3py.py.

7439 def help(self):
7440 """Display a string describing all available options."""
7441 print(Z3_solver_get_help(self.ctx.ref(), self.solver))
7442
Z3_string Z3_API Z3_solver_get_help(Z3_context c, Z3_solver s)
Return a string describing all solver available parameters.

◆ import_model_converter()

import_model_converter ( self,
other )
Import model converter from other into the current solver

Definition at line 7230 of file z3py.py.

7230 def import_model_converter(self, other):
7231 """Import model converter from other into the current solver"""
7232 Z3_solver_import_model_converter(self.ctx.ref(), other.solver, self.solver)
7233

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

7141 def insert(self, *args):
7142 """Assert constraints into the solver.
7143
7144 >>> x = Int('x')
7145 >>> s = Solver()
7146 >>> s.insert(x > 0, x < 2)
7147 >>> s
7148 [x > 0, x < 2]
7149 """
7150 self.assert_exprs(*args)
7151

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

7234 def interrupt(self):
7235 """Interrupt the execution of the solver object.
7236 Remarks: This ensures that the interrupt applies only
7237 to the given solver object and it applies only if it is running.
7238 """
7239 Z3_solver_interrupt(self.ctx.ref(), self.solver)
7240
void Z3_API Z3_solver_interrupt(Z3_context c, Z3_solver s)
Solver local interrupt. Normally you should use Z3_interrupt to cancel solvers because only one solve...

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

7211 def model(self):
7212 """Return a model for the last `check()`.
7213
7214 This function raises an exception if
7215 a model is not available (e.g., last `check()` returned unsat).
7216
7217 >>> s = Solver()
7218 >>> a = Int('a')
7219 >>> s.add(a + 2 == 0)
7220 >>> s.check()
7221 sat
7222 >>> s.model()
7223 [a = -2]
7224 """
7225 try:
7226 return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx)
7227 except Z3Exception:
7228 raise Z3Exception("model is not available")
7229
Z3_model Z3_API Z3_solver_get_model(Z3_context c, Z3_solver s)
Retrieve the model for the last Z3_solver_check or Z3_solver_check_assumptions.

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

◆ next()

next ( self,
t )

Definition at line 7346 of file z3py.py.

7346 def next(self, t):
7347 t = _py2expr(t, self.ctx)
7348 """Retrieve congruence closure sibling of the term t relative to the current search state
7349 The function primarily works for SimpleSolver. Terms and variables that are
7350 eliminated during pre-processing are not visible to the congruence closure.
7351 """
7352 return _to_expr_ref(Z3_solver_congruence_next(self.ctx.ref(), self.solver, t.ast), self.ctx)
7353
Z3_ast Z3_API Z3_solver_congruence_next(Z3_context c, Z3_solver s, Z3_ast a)
retrieve the next expression in the congruence class. The set of congruent siblings form a cyclic lis...

◆ non_units()

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

Definition at line 7383 of file z3py.py.

7383 def non_units(self):
7384 """Return an AST vector containing all atomic formulas in solver state that are not units.
7385 """
7386 return AstVector(Z3_solver_get_non_units(self.ctx.ref(), self.solver), self.ctx)
7387
Z3_ast_vector Z3_API Z3_solver_get_non_units(Z3_context c, Z3_solver s)
Return the set of non units in the solver state.

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

7064 def num_scopes(self):
7065 """Return the current number of backtracking points.
7066
7067 >>> s = Solver()
7068 >>> s.num_scopes()
7069 0
7070 >>> s.push()
7071 >>> s.num_scopes()
7072 1
7073 >>> s.push()
7074 >>> s.num_scopes()
7075 2
7076 >>> s.pop()
7077 >>> s.num_scopes()
7078 1
7079 """
7080 return Z3_solver_get_num_scopes(self.ctx.ref(), self.solver)
7081
unsigned Z3_API Z3_solver_get_num_scopes(Z3_context c, Z3_solver s)
Return the number of backtracking points.

◆ param_descrs()

param_descrs ( self)
Return the parameter description set.

Definition at line 7443 of file z3py.py.

7443 def param_descrs(self):
7444 """Return the parameter description set."""
7445 return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx)
7446
Z3_param_descrs Z3_API Z3_solver_get_param_descrs(Z3_context c, Z3_solver s)
Return the parameter description set for the given solver object.

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

7042 def pop(self, num=1):
7043 """Backtrack \\c num backtracking points.
7044
7045 >>> x = Int('x')
7046 >>> s = Solver()
7047 >>> s.add(x > 0)
7048 >>> s
7049 [x > 0]
7050 >>> s.push()
7051 >>> s.add(x < 1)
7052 >>> s
7053 [x > 0, x < 1]
7054 >>> s.check()
7055 unsat
7056 >>> s.pop()
7057 >>> s.check()
7058 sat
7059 >>> s
7060 [x > 0]
7061 """
7062 Z3_solver_pop(self.ctx.ref(), self.solver, num)
7063
void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n)
Backtrack n backtracking points.

Referenced by Solver.__exit__().

◆ proof()

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

Definition at line 7360 of file z3py.py.

7360 def proof(self):
7361 """Return a proof for the last `check()`. Proof construction must be enabled."""
7362 return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
7363
Z3_ast Z3_API Z3_solver_get_proof(Z3_context c, Z3_solver s)
Retrieve the proof for the last Z3_solver_check or Z3_solver_check_assumptions.

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

7020 def push(self):
7021 """Create a backtracking point.
7022
7023 >>> x = Int('x')
7024 >>> s = Solver()
7025 >>> s.add(x > 0)
7026 >>> s
7027 [x > 0]
7028 >>> s.push()
7029 >>> s.add(x < 1)
7030 >>> s
7031 [x > 0, x < 1]
7032 >>> s.check()
7033 unsat
7034 >>> s.pop()
7035 >>> s.check()
7036 sat
7037 >>> s
7038 [x > 0]
7039 """
7040 Z3_solver_push(self.ctx.ref(), self.solver)
7041
void Z3_API Z3_solver_push(Z3_context c, Z3_solver s)
Create a backtracking point.

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(2**x == 4)
>>> s.check()
unknown
>>> s.reason_unknown()
'(incomplete (theory arithmetic))'

Definition at line 7426 of file z3py.py.

7426 def reason_unknown(self):
7427 """Return a string describing why the last `check()` returned `unknown`.
7428
7429 >>> x = Int('x')
7430 >>> s = SimpleSolver()
7431 >>> s.add(2**x == 4)
7432 >>> s.check()
7433 unknown
7434 >>> s.reason_unknown()
7435 '(incomplete (theory arithmetic))'
7436 """
7437 return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver)
7438
Z3_string Z3_API Z3_solver_get_reason_unknown(Z3_context c, Z3_solver s)
Return a brief justification for an "unknown" result (i.e., Z3_L_UNDEF) for the commands Z3_solver_ch...

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

7082 def reset(self):
7083 """Remove all asserted constraints and backtracking points created using `push()`.
7084
7085 >>> x = Int('x')
7086 >>> s = Solver()
7087 >>> s.add(x > 0)
7088 >>> s
7089 [x > 0]
7090 >>> s.reset()
7091 >>> s
7092 []
7093 """
7094 Z3_solver_reset(self.ctx.ref(), self.solver)
7095
void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)
Remove all assertions from the solver.

◆ root()

root ( self,
t )

Definition at line 7338 of file z3py.py.

7338 def root(self, t):
7339 t = _py2expr(t, self.ctx)
7340 """Retrieve congruence closure root of the term t relative to the current search state
7341 The function primarily works for SimpleSolver. Terms and variables that are
7342 eliminated during pre-processing are not visible to the congruence closure.
7343 """
7344 return _to_expr_ref(Z3_solver_congruence_root(self.ctx.ref(), self.solver, t.ast), self.ctx)
7345
Z3_ast Z3_API Z3_solver_congruence_root(Z3_context c, Z3_solver s, Z3_ast a)
retrieve the congruence closure root of an expression. The root is retrieved relative to the state wh...

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

7007 def set(self, *args, **keys):
7008 """Set a configuration option.
7009 The method `help()` return a string containing all available options.
7010
7011 >>> s = Solver()
7012 >>> # The option MBQI can be set using three different approaches.
7013 >>> s.set(mbqi=True)
7014 >>> s.set('MBQI', True)
7015 >>> s.set(':mbqi', True)
7016 """
7017 p = args2params(args, keys, self.ctx)
7018 Z3_solver_set_params(self.ctx.ref(), self.solver, p.params)
7019
void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p)
Set the given solver using the given parameters.

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

7396 def set_initial_value(self, var, value):
7397 """initialize the solver's state by setting the initial value of var to value
7398 """
7399 s = var.sort()
7400 value = s.cast(value)
7401 Z3_solver_set_initial_value(self.ctx.ref(), self.solver, var.ast, value.ast)
7402
void Z3_API Z3_solver_set_initial_value(Z3_context c, Z3_solver s, Z3_ast v, Z3_ast val)
provide an initialization hint to the solver. The initialization hint is used to calibrate an initial...

◆ sexpr()

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

7470 def sexpr(self):
7471 """Return a formatted string (in Lisp-like format) with all added constraints.
7472 We say the string is in s-expression format.
7473
7474 >>> x = Int('x')
7475 >>> s = Solver()
7476 >>> s.add(x > 0)
7477 >>> s.add(x < 2)
7478 >>> r = s.sexpr()
7479 """
7480 return Z3_solver_to_string(self.ctx.ref(), self.solver)
7481
Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s)
Convert a solver into a string.

◆ solve_for()

solve_for ( self,
t )

Definition at line 7354 of file z3py.py.

7354 def solve_for(self, t):
7355 t = _py2expr(t, self.ctx)
7356 """Retrieve a solution for t relative to linear equations maintained in the current state.
7357 The function primarily works for SimpleSolver and when there is a solution using linear arithmetic."""
7358 return _to_expr_ref(Z3_solver_solve_for(self.ctx.ref(), self.solver, t.ast), self.ctx)
7359
Z3_ast Z3_API Z3_solver_solve_for(Z3_context c, Z3_solver s, Z3_ast t)
retrieve a 'solution' for t as defined by equalities in maintained by solvers. At this point,...

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

7408 def statistics(self):
7409 """Return statistics for the last `check()`.
7410
7411 >>> s = SimpleSolver()
7412 >>> x = Int('x')
7413 >>> s.add(x > 0)
7414 >>> s.check()
7415 sat
7416 >>> st = s.statistics()
7417 >>> st.get_key_value('final checks')
7418 1
7419 >>> len(st) > 0
7420 True
7421 >>> st[0] != 0
7422 True
7423 """
7424 return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx)
7425
Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s)
Return statistics for the given solver.

◆ to_smt2()

to_smt2 ( self)
return SMTLIB2 formatted benchmark for solver's assertions

Definition at line 7486 of file z3py.py.

7486 def to_smt2(self):
7487 """return SMTLIB2 formatted benchmark for solver's assertions"""
7488 es = self.assertions()
7489 sz = len(es)
7490 sz1 = sz
7491 if sz1 > 0:
7492 sz1 -= 1
7493 v = (Ast * sz1)()
7494 for i in range(sz1):
7495 v[i] = es[i].as_ast()
7496 if sz > 0:
7497 e = es[sz1].as_ast()
7498 else:
7499 e = BoolVal(True, self.ctx).as_ast()
7501 self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e,
7502 )
7503
7504
Z3_string Z3_API Z3_benchmark_to_smtlib_string(Z3_context c, Z3_string name, Z3_string logic, Z3_string status, Z3_string attributes, unsigned num_assumptions, Z3_ast const assumptions[], Z3_ast formula)
Convert the given benchmark into SMT-LIB formatted string.

◆ trail()

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

Definition at line 7403 of file z3py.py.

7403 def trail(self):
7404 """Return trail of the solver state after a check() call.
7405 """
7406 return AstVector(Z3_solver_get_trail(self.ctx.ref(), self.solver), self.ctx)
7407
Z3_ast_vector Z3_API Z3_solver_get_trail(Z3_context c, Z3_solver s)
Return the trail modulo model conversion, in order of decision level The decision level can be retrie...

◆ trail_levels()

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

Definition at line 7388 of file z3py.py.

7388 def trail_levels(self):
7389 """Return trail and decision levels of the solver state after a check() call.
7390 """
7391 trail = self.trail()
7392 levels = (ctypes.c_uint * len(trail))()
7393 Z3_solver_get_levels(self.ctx.ref(), self.solver, trail.vector, len(trail), levels)
7394 return trail, levels
7395
void Z3_API Z3_solver_get_levels(Z3_context c, Z3_solver s, Z3_ast_vector literals, unsigned sz, unsigned levels[])
retrieve the decision depth of Boolean literals (variables or their negations). Assumes a check-sat c...

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

7451 def translate(self, target):
7452 """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
7453
7454 >>> c1 = Context()
7455 >>> c2 = Context()
7456 >>> s1 = Solver(ctx=c1)
7457 >>> s2 = s1.translate(c2)
7458 """
7459 if z3_debug():
7460 _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
7461 solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref())
7462 return Solver(solver, target)
7463
Z3_solver Z3_API Z3_solver_translate(Z3_context source, Z3_solver s, Z3_context target)
Copy a solver s from the context source to the context target.

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

◆ units()

units ( self)
Return an AST vector containing all currently inferred units.

Definition at line 7378 of file z3py.py.

7378 def units(self):
7379 """Return an AST vector containing all currently inferred units.
7380 """
7381 return AstVector(Z3_solver_get_units(self.ctx.ref(), self.solver), self.ctx)
7382
Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s)
Return the set of units modulo model conversion.

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

7241 def unsat_core(self):
7242 """Return a subset (as an AST vector) of the assumptions provided to the last check().
7243
7244 These are the assumptions Z3 used in the unsatisfiability proof.
7245 Assumptions are available in Z3. They are used to extract unsatisfiable cores.
7246 They may be also used to "retract" assumptions. Note that, assumptions are not really
7247 "soft constraints", but they can be used to implement them.
7248
7249 >>> p1, p2, p3 = Bools('p1 p2 p3')
7250 >>> x, y = Ints('x y')
7251 >>> s = Solver()
7252 >>> s.add(Implies(p1, x > 0))
7253 >>> s.add(Implies(p2, y > x))
7254 >>> s.add(Implies(p2, y < 1))
7255 >>> s.add(Implies(p3, y > -3))
7256 >>> s.check(p1, p2, p3)
7257 unsat
7258 >>> core = s.unsat_core()
7259 >>> len(core)
7260 2
7261 >>> p1 in core
7262 True
7263 >>> p2 in core
7264 True
7265 >>> p3 in core
7266 False
7267 >>> # "Retracting" p2
7268 >>> s.check(p1, p3)
7269 sat
7270 """
7271 return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx)
7272
Z3_ast_vector Z3_API Z3_solver_get_unsat_core(Z3_context c, Z3_solver s)
Retrieve the unsat core for the last Z3_solver_check_assumptions The unsat core is a subset of the as...

Field Documentation

◆ backtrack_level

int backtrack_level = 4000000000

Definition at line 6986 of file z3py.py.

◆ ctx

ctx = _get_ctx(ctx)

Definition at line 6985 of file z3py.py.

Referenced by ArithRef.__add__(), BitVecRef.__add__(), BitVecRef.__and__(), FuncDeclRef.__call__(), AstMap.__contains__(), AstRef.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), Goal.__copy__(), ModelRef.__copy__(), AstMap.__deepcopy__(), AstRef.__deepcopy__(), AstVector.__deepcopy__(), Datatype.__deepcopy__(), FuncEntry.__deepcopy__(), FuncInterp.__deepcopy__(), Goal.__deepcopy__(), ModelRef.__deepcopy__(), ParamDescrsRef.__deepcopy__(), ParamsRef.__deepcopy__(), Statistics.__deepcopy__(), AstMap.__del__(), AstRef.__del__(), AstVector.__del__(), Context.__del__(), FuncEntry.__del__(), FuncInterp.__del__(), Goal.__del__(), ModelRef.__del__(), ParamDescrsRef.__del__(), ParamsRef.__del__(), ScopedConstructor.__del__(), ScopedConstructorList.__del__(), Solver.__del__(), Statistics.__del__(), ArithRef.__div__(), BitVecRef.__div__(), ExprRef.__eq__(), ArithRef.__ge__(), BitVecRef.__ge__(), AstMap.__getitem__(), AstVector.__getitem__(), ModelRef.__getitem__(), Statistics.__getitem__(), ArithRef.__gt__(), BitVecRef.__gt__(), BitVecRef.__invert__(), ArithRef.__le__(), BitVecRef.__le__(), AstMap.__len__(), AstVector.__len__(), ModelRef.__len__(), Statistics.__len__(), BitVecRef.__lshift__(), ArithRef.__lt__(), BitVecRef.__lt__(), ArithRef.__mod__(), BitVecRef.__mod__(), ArithRef.__mul__(), BitVecRef.__mul__(), BoolRef.__mul__(), ExprRef.__ne__(), ArithRef.__neg__(), BitVecRef.__neg__(), BitVecRef.__or__(), ArithRef.__pow__(), ArithRef.__radd__(), BitVecRef.__radd__(), BitVecRef.__rand__(), ArithRef.__rdiv__(), BitVecRef.__rdiv__(), AstMap.__repr__(), ParamDescrsRef.__repr__(), ParamsRef.__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__(), AstMap.__setitem__(), AstVector.__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(), 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(), AstVector.push(), Solver.push(), QuantifierRef.qid(), ArraySortRef.range(), FuncDeclRef.range(), DatatypeSortRef.recognizer(), Context.ref(), AstMap.reset(), Solver.reset(), AstVector.resize(), ParamsRef.set(), Solver.set(), AstVector.sexpr(), Goal.sexpr(), ModelRef.sexpr(), Goal.size(), ParamDescrsRef.size(), QuantifierRef.skolem_id(), AstRef.translate(), AstVector.translate(), Goal.translate(), ModelRef.translate(), ParamsRef.validate(), FuncEntry.value(), QuantifierRef.var_name(), and QuantifierRef.var_sort().

◆ cube_vs

cube_vs = AstVector(None, self.ctx)

Definition at line 7317 of file z3py.py.

◆ solver