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)
 
 explain_congruent (self, a, b)
 
 solve_for1 (self, t)
 
 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)
 
- 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 7005 of file z3py.py.

Constructor & Destructor Documentation

◆ __init__()

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

Definition at line 7011 of file z3py.py.

7011 def __init__(self, solver=None, ctx=None, logFile=None):
7012 assert solver is None or ctx is not None
7013 self.ctx = _get_ctx(ctx)
7014 self.backtrack_level = 4000000000
7015 self.solver = None
7016 if solver is None:
7017 self.solver = Z3_mk_solver(self.ctx.ref())
7018 else:
7019 self.solver = solver
7020 Z3_solver_inc_ref(self.ctx.ref(), self.solver)
7021 if logFile is not None:
7022 self.set("smtlib2_log", logFile)
7023
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 7024 of file z3py.py.

7024 def __del__(self):
7025 if self.solver is not None and self.ctx.ref() is not None and Z3_solver_dec_ref is not None:
7026 Z3_solver_dec_ref(self.ctx.ref(), self.solver)
7027
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 7510 of file z3py.py.

7510 def __copy__(self):
7511 return self.translate(self.ctx)
7512

◆ __deepcopy__()

__deepcopy__ ( self,
memo = {} )

Definition at line 7513 of file z3py.py.

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

◆ __enter__()

__enter__ ( self)

Definition at line 7028 of file z3py.py.

7028 def __enter__(self):
7029 self.push()
7030 return self
7031

◆ __exit__()

__exit__ ( self,
* exc_info )

Definition at line 7032 of file z3py.py.

7032 def __exit__(self, *exc_info):
7033 self.pop()
7034

◆ __iadd__()

__iadd__ ( self,
fml )

Definition at line 7154 of file z3py.py.

7154 def __iadd__(self, fml):
7155 self.add(fml)
7156 return self
7157

◆ __repr__()

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

Definition at line 7493 of file z3py.py.

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

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

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

Referenced by __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 7158 of file z3py.py.

7158 def append(self, *args):
7159 """Assert constraints into the solver.
7160
7161 >>> x = Int('x')
7162 >>> s = Solver()
7163 >>> s.append(x > 0, x < 2)
7164 >>> s
7165 [x > 0, x < 2]
7166 """
7167 self.assert_exprs(*args)
7168

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

7180 def assert_and_track(self, a, p):
7181 """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
7182
7183 If `p` is a string, it will be automatically converted into a Boolean constant.
7184
7185 >>> x = Int('x')
7186 >>> p3 = Bool('p3')
7187 >>> s = Solver()
7188 >>> s.set(unsat_core=True)
7189 >>> s.assert_and_track(x > 0, 'p1')
7190 >>> s.assert_and_track(x != 1, 'p2')
7191 >>> s.assert_and_track(x < 0, p3)
7192 >>> print(s.check())
7193 unsat
7194 >>> c = s.unsat_core()
7195 >>> len(c)
7196 2
7197 >>> Bool('p1') in c
7198 True
7199 >>> Bool('p2') in c
7200 False
7201 >>> p3 in c
7202 True
7203 """
7204 if isinstance(p, str):
7205 p = Bool(p, self.ctx)
7206 _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
7207 _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
7208 Z3_solver_assert_and_track(self.ctx.ref(), self.solver, a.as_ast(), p.as_ast())
7209
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 7124 of file z3py.py.

7124 def assert_exprs(self, *args):
7125 """Assert constraints into the solver.
7126
7127 >>> x = Int('x')
7128 >>> s = Solver()
7129 >>> s.assert_exprs(x > 0, x < 2)
7130 >>> s
7131 [x > 0, x < 2]
7132 """
7133 args = _get_args(args)
7134 s = BoolSort(self.ctx)
7135 for arg in args:
7136 if isinstance(arg, Goal) or isinstance(arg, AstVector):
7137 for f in arg:
7138 Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast())
7139 else:
7140 arg = s.cast(arg)
7141 Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast())
7142
void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a)
Assert a constraint into the solver.

Referenced by add(), append(), and 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 7410 of file z3py.py.

7410 def assertions(self):
7411 """Return an AST vector containing all added constraints.
7412
7413 >>> s = Solver()
7414 >>> s.assertions()
7415 []
7416 >>> a = Int('a')
7417 >>> s.add(a > 0)
7418 >>> s.add(a < 10)
7419 >>> s.assertions()
7420 [a > 0, a < 10]
7421 """
7422 return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
7423
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 7210 of file z3py.py.

7210 def check(self, *assumptions):
7211 """Check whether the assertions in the given solver plus the optional assumptions are consistent or not.
7212
7213 >>> x = Int('x')
7214 >>> s = Solver()
7215 >>> s.check()
7216 sat
7217 >>> s.add(x > 0, x < 2)
7218 >>> s.check()
7219 sat
7220 >>> s.model().eval(x)
7221 1
7222 >>> s.add(x < 1)
7223 >>> s.check()
7224 unsat
7225 >>> s.reset()
7226 >>> s.add(2**x == 4)
7227 >>> s.check()
7228 unknown
7229 """
7230 s = BoolSort(self.ctx)
7231 assumptions = _get_args(assumptions)
7232 num = len(assumptions)
7233 _assumptions = (Ast * num)()
7234 for i in range(num):
7235 _assumptions[i] = s.cast(assumptions[i]).as_ast()
7236 r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions)
7237 return CheckSatResult(r)
7238
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 7301 of file z3py.py.

7301 def consequences(self, assumptions, variables):
7302 """Determine fixed values for the variables based on the solver state and assumptions.
7303 >>> s = Solver()
7304 >>> a, b, c, d = Bools('a b c d')
7305 >>> s.add(Implies(a,b), Implies(b, c))
7306 >>> s.consequences([a],[b,c,d])
7307 (sat, [Implies(a, b), Implies(a, c)])
7308 >>> s.consequences([Not(c),d],[a,b,c,d])
7309 (sat, [Implies(d, d), Implies(Not(c), Not(c)), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))])
7310 """
7311 if isinstance(assumptions, list):
7312 _asms = AstVector(None, self.ctx)
7313 for a in assumptions:
7314 _asms.push(a)
7315 assumptions = _asms
7316 if isinstance(variables, list):
7317 _vars = AstVector(None, self.ctx)
7318 for a in variables:
7319 _vars.push(a)
7320 variables = _vars
7321 _z3_assert(isinstance(assumptions, AstVector), "ast vector expected")
7322 _z3_assert(isinstance(variables, AstVector), "ast vector expected")
7323 consequences = AstVector(None, self.ctx)
7324 r = Z3_solver_get_consequences(self.ctx.ref(), self.solver, assumptions.vector,
7325 variables.vector, consequences.vector)
7326 sz = len(consequences)
7327 consequences = [consequences[i] for i in range(sz)]
7328 return CheckSatResult(r), consequences
7329
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 7338 of file z3py.py.

7338 def cube(self, vars=None):
7339 """Get set of cubes
7340 The method takes an optional set of variables that restrict which
7341 variables may be used as a starting point for cubing.
7342 If vars is not None, then the first case split is based on a variable in
7343 this set.
7344 """
7345 self.cube_vs = AstVector(None, self.ctx)
7346 if vars is not None:
7347 for v in vars:
7348 self.cube_vs.push(v)
7349 while True:
7350 lvl = self.backtrack_level
7351 self.backtrack_level = 4000000000
7352 r = AstVector(Z3_solver_cube(self.ctx.ref(), self.solver, self.cube_vs.vector, lvl), self.ctx)
7353 if (len(r) == 1 and is_false(r[0])):
7354 return
7355 yield r
7356 if (len(r) == 0):
7357 return
7358
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 7359 of file z3py.py.

7359 def cube_vars(self):
7360 """Access the set of variables that were touched by the most recently generated cube.
7361 This set of variables can be used as a starting point for additional cubes.
7362 The idea is that variables that appear in clauses that are reduced by the most recent
7363 cube are likely more useful to cube on."""
7364 return self.cube_vs
7365

◆ dimacs()

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

Definition at line 7528 of file z3py.py.

7528 def dimacs(self, include_names=True):
7529 """Return a textual representation of the solver in DIMACS format."""
7530 return Z3_solver_to_dimacs_string(self.ctx.ref(), self.solver, include_names)
7531
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.

◆ explain_congruent()

explain_congruent ( self,
a,
b )
Explain congruence of a and b relative to the current search state

Definition at line 7382 of file z3py.py.

7382 def explain_congruent(self, a, b):
7383 """Explain congruence of a and b relative to the current search state"""
7384 a = _py2expr(a, self.ctx)
7385 b = _py2expr(b, self.ctx)
7386 return _to_expr_ref(Z3_solver_congruence_explain(self.ctx.ref(), self.solver, a.ast, b.ast), self.ctx)
7387
Z3_ast Z3_API Z3_solver_congruence_explain(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast b)
retrieve explanation for congruence.

◆ from_file()

from_file ( self,
filename )
Parse assertions from a file

Definition at line 7330 of file z3py.py.

7330 def from_file(self, filename):
7331 """Parse assertions from a file"""
7332 Z3_solver_from_file(self.ctx.ref(), self.solver, filename)
7333
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 7334 of file z3py.py.

7334 def from_string(self, s):
7335 """Parse assertions from a string"""
7336 Z3_solver_from_string(self.ctx.ref(), self.solver, s)
7337
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 7485 of file z3py.py.

7485 def help(self):
7486 """Display a string describing all available options."""
7487 print(Z3_solver_get_help(self.ctx.ref(), self.solver))
7488
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 7258 of file z3py.py.

7258 def import_model_converter(self, other):
7259 """Import model converter from other into the current solver"""
7260 Z3_solver_import_model_converter(self.ctx.ref(), other.solver, self.solver)
7261

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

7169 def insert(self, *args):
7170 """Assert constraints into the solver.
7171
7172 >>> x = Int('x')
7173 >>> s = Solver()
7174 >>> s.insert(x > 0, x < 2)
7175 >>> s
7176 [x > 0, x < 2]
7177 """
7178 self.assert_exprs(*args)
7179

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

7262 def interrupt(self):
7263 """Interrupt the execution of the solver object.
7264 Remarks: This ensures that the interrupt applies only
7265 to the given solver object and it applies only if it is running.
7266 """
7267 Z3_solver_interrupt(self.ctx.ref(), self.solver)
7268
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 7239 of file z3py.py.

7239 def model(self):
7240 """Return a model for the last `check()`.
7241
7242 This function raises an exception if
7243 a model is not available (e.g., last `check()` returned unsat).
7244
7245 >>> s = Solver()
7246 >>> a = Int('a')
7247 >>> s.add(a + 2 == 0)
7248 >>> s.check()
7249 sat
7250 >>> s.model()
7251 [a = -2]
7252 """
7253 try:
7254 return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx)
7255 except Z3Exception:
7256 raise Z3Exception("model is not available")
7257
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.

◆ next()

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

7374 def next(self, t):
7375 """Retrieve congruence closure sibling of the term t relative to the current search state
7376 The function primarily works for SimpleSolver. Terms and variables that are
7377 eliminated during pre-processing are not visible to the congruence closure.
7378 """
7379 t = _py2expr(t, self.ctx)
7380 return _to_expr_ref(Z3_solver_congruence_next(self.ctx.ref(), self.solver, t.ast), self.ctx)
7381
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 7429 of file z3py.py.

7429 def non_units(self):
7430 """Return an AST vector containing all atomic formulas in solver state that are not units.
7431 """
7432 return AstVector(Z3_solver_get_non_units(self.ctx.ref(), self.solver), self.ctx)
7433
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 7092 of file z3py.py.

7092 def num_scopes(self):
7093 """Return the current number of backtracking points.
7094
7095 >>> s = Solver()
7096 >>> s.num_scopes()
7097 0
7098 >>> s.push()
7099 >>> s.num_scopes()
7100 1
7101 >>> s.push()
7102 >>> s.num_scopes()
7103 2
7104 >>> s.pop()
7105 >>> s.num_scopes()
7106 1
7107 """
7108 return Z3_solver_get_num_scopes(self.ctx.ref(), self.solver)
7109
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 7489 of file z3py.py.

7489 def param_descrs(self):
7490 """Return the parameter description set."""
7491 return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx)
7492
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 7070 of file z3py.py.

7070 def pop(self, num=1):
7071 """Backtrack \\c num backtracking points.
7072
7073 >>> x = Int('x')
7074 >>> s = Solver()
7075 >>> s.add(x > 0)
7076 >>> s
7077 [x > 0]
7078 >>> s.push()
7079 >>> s.add(x < 1)
7080 >>> s
7081 [x > 0, x < 1]
7082 >>> s.check()
7083 unsat
7084 >>> s.pop()
7085 >>> s.check()
7086 sat
7087 >>> s
7088 [x > 0]
7089 """
7090 Z3_solver_pop(self.ctx.ref(), self.solver, num)
7091
void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n)
Backtrack n backtracking points.

Referenced by __exit__().

◆ proof()

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

Definition at line 7406 of file z3py.py.

7406 def proof(self):
7407 """Return a proof for the last `check()`. Proof construction must be enabled."""
7408 return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
7409
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 7048 of file z3py.py.

7048 def push(self):
7049 """Create a backtracking point.
7050
7051 >>> x = Int('x')
7052 >>> s = Solver()
7053 >>> s.add(x > 0)
7054 >>> s
7055 [x > 0]
7056 >>> s.push()
7057 >>> s.add(x < 1)
7058 >>> s
7059 [x > 0, x < 1]
7060 >>> s.check()
7061 unsat
7062 >>> s.pop()
7063 >>> s.check()
7064 sat
7065 >>> s
7066 [x > 0]
7067 """
7068 Z3_solver_push(self.ctx.ref(), self.solver)
7069
void Z3_API Z3_solver_push(Z3_context c, Z3_solver s)
Create a backtracking point.

Referenced by __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 7472 of file z3py.py.

7472 def reason_unknown(self):
7473 """Return a string describing why the last `check()` returned `unknown`.
7474
7475 >>> x = Int('x')
7476 >>> s = SimpleSolver()
7477 >>> s.add(2**x == 4)
7478 >>> s.check()
7479 unknown
7480 >>> s.reason_unknown()
7481 '(incomplete (theory arithmetic))'
7482 """
7483 return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver)
7484
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 7110 of file z3py.py.

7110 def reset(self):
7111 """Remove all asserted constraints and backtracking points created using `push()`.
7112
7113 >>> x = Int('x')
7114 >>> s = Solver()
7115 >>> s.add(x > 0)
7116 >>> s
7117 [x > 0]
7118 >>> s.reset()
7119 >>> s
7120 []
7121 """
7122 Z3_solver_reset(self.ctx.ref(), self.solver)
7123
void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)
Remove all assertions from the solver.

◆ root()

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

7366 def root(self, t):
7367 """Retrieve congruence closure root of the term t relative to the current search state
7368 The function primarily works for SimpleSolver. Terms and variables that are
7369 eliminated during pre-processing are not visible to the congruence closure.
7370 """
7371 t = _py2expr(t, self.ctx)
7372 return _to_expr_ref(Z3_solver_congruence_root(self.ctx.ref(), self.solver, t.ast), self.ctx)
7373
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 7035 of file z3py.py.

7035 def set(self, *args, **keys):
7036 """Set a configuration option.
7037 The method `help()` return a string containing all available options.
7038
7039 >>> s = Solver()
7040 >>> # The option MBQI can be set using three different approaches.
7041 >>> s.set(mbqi=True)
7042 >>> s.set('MBQI', True)
7043 >>> s.set(':mbqi', True)
7044 """
7045 p = args2params(args, keys, self.ctx)
7046 Z3_solver_set_params(self.ctx.ref(), self.solver, p.params)
7047
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 7442 of file z3py.py.

7442 def set_initial_value(self, var, value):
7443 """initialize the solver's state by setting the initial value of var to value
7444 """
7445 s = var.sort()
7446 value = s.cast(value)
7447 Z3_solver_set_initial_value(self.ctx.ref(), self.solver, var.ast, value.ast)
7448
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 7516 of file z3py.py.

7516 def sexpr(self):
7517 """Return a formatted string (in Lisp-like format) with all added constraints.
7518 We say the string is in s-expression format.
7519
7520 >>> x = Int('x')
7521 >>> s = Solver()
7522 >>> s.add(x > 0)
7523 >>> s.add(x < 2)
7524 >>> r = s.sexpr()
7525 """
7526 return Z3_solver_to_string(self.ctx.ref(), self.solver)
7527
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,
ts )
Retrieve a solution for t relative to linear equations maintained in the current state.

Definition at line 7394 of file z3py.py.

7394 def solve_for(self, ts):
7395 """Retrieve a solution for t relative to linear equations maintained in the current state."""
7396 vars = AstVector(ctx=self.ctx);
7397 terms = AstVector(ctx=self.ctx);
7398 guards = AstVector(ctx=self.ctx);
7399 for t in ts:
7400 t = _py2expr(t, self.ctx)
7401 vars.push(t)
7402 Z3_solver_solve_for(self.ctx.ref(), self.solver, vars.vector, terms.vector, guards.vector)
7403 return [(vars[i], terms[i], guards[i]) for i in range(len(vars))]
7404
7405
void Z3_API Z3_solver_solve_for(Z3_context c, Z3_solver s, Z3_ast_vector variables, Z3_ast_vector terms, Z3_ast_vector guards)
retrieve a 'solution' for variables as defined by equalities in maintained by solvers....

◆ solve_for1()

solve_for1 ( self,
t )
Retrieve a solution for t relative to linear equations maintained in the current state.
The function primarily works for SimpleSolver and when there is a solution using linear arithmetic.

Definition at line 7388 of file z3py.py.

7388 def solve_for1(self, t):
7389 """Retrieve a solution for t relative to linear equations maintained in the current state.
7390 The function primarily works for SimpleSolver and when there is a solution using linear arithmetic."""
7391 t = _py2expr(t, self.ctx)
7392 return _to_expr_ref(Z3_solver_solve_for1(self.ctx.ref(), self.solver, t.ast), self.ctx)
7393

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

7454 def statistics(self):
7455 """Return statistics for the last `check()`.
7456
7457 >>> s = SimpleSolver()
7458 >>> x = Int('x')
7459 >>> s.add(x > 0)
7460 >>> s.check()
7461 sat
7462 >>> st = s.statistics()
7463 >>> st.get_key_value('final checks')
7464 1
7465 >>> len(st) > 0
7466 True
7467 >>> st[0] != 0
7468 True
7469 """
7470 return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx)
7471
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 7532 of file z3py.py.

7532 def to_smt2(self):
7533 """return SMTLIB2 formatted benchmark for solver's assertions"""
7534 es = self.assertions()
7535 sz = len(es)
7536 sz1 = sz
7537 if sz1 > 0:
7538 sz1 -= 1
7539 v = (Ast * sz1)()
7540 for i in range(sz1):
7541 v[i] = es[i].as_ast()
7542 if sz > 0:
7543 e = es[sz1].as_ast()
7544 else:
7545 e = BoolVal(True, self.ctx).as_ast()
7547 self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e,
7548 )
7549
7550
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 7449 of file z3py.py.

7449 def trail(self):
7450 """Return trail of the solver state after a check() call.
7451 """
7452 return AstVector(Z3_solver_get_trail(self.ctx.ref(), self.solver), self.ctx)
7453
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 7434 of file z3py.py.

7434 def trail_levels(self):
7435 """Return trail and decision levels of the solver state after a check() call.
7436 """
7437 trail = self.trail()
7438 levels = (ctypes.c_uint * len(trail))()
7439 Z3_solver_get_levels(self.ctx.ref(), self.solver, trail.vector, len(trail), levels)
7440 return trail, levels
7441
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 7497 of file z3py.py.

7497 def translate(self, target):
7498 """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
7499
7500 >>> c1 = Context()
7501 >>> c2 = Context()
7502 >>> s1 = Solver(ctx=c1)
7503 >>> s2 = s1.translate(c2)
7504 """
7505 if z3_debug():
7506 _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
7507 solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref())
7508 return Solver(solver, target)
7509
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.

◆ units()

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

Definition at line 7424 of file z3py.py.

7424 def units(self):
7425 """Return an AST vector containing all currently inferred units.
7426 """
7427 return AstVector(Z3_solver_get_units(self.ctx.ref(), self.solver), self.ctx)
7428
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 7269 of file z3py.py.

7269 def unsat_core(self):
7270 """Return a subset (as an AST vector) of the assumptions provided to the last check().
7271
7272 These are the assumptions Z3 used in the unsatisfiability proof.
7273 Assumptions are available in Z3. They are used to extract unsatisfiable cores.
7274 They may be also used to "retract" assumptions. Note that, assumptions are not really
7275 "soft constraints", but they can be used to implement them.
7276
7277 >>> p1, p2, p3 = Bools('p1 p2 p3')
7278 >>> x, y = Ints('x y')
7279 >>> s = Solver()
7280 >>> s.add(Implies(p1, x > 0))
7281 >>> s.add(Implies(p2, y > x))
7282 >>> s.add(Implies(p2, y < 1))
7283 >>> s.add(Implies(p3, y > -3))
7284 >>> s.check(p1, p2, p3)
7285 unsat
7286 >>> core = s.unsat_core()
7287 >>> len(core)
7288 2
7289 >>> p1 in core
7290 True
7291 >>> p2 in core
7292 True
7293 >>> p3 in core
7294 False
7295 >>> # "Retracting" p2
7296 >>> s.check(p1, p3)
7297 sat
7298 """
7299 return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx)
7300
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 7014 of file z3py.py.

◆ ctx

ctx = _get_ctx(ctx)

Definition at line 7013 of file z3py.py.

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

◆ cube_vs

cube_vs = AstVector(None, self.ctx)

Definition at line 7345 of file z3py.py.

◆ solver

solver = None

Definition at line 7015 of file z3py.py.

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