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

Constructor & Destructor Documentation

◆ __init__()

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

Definition at line 7020 of file z3py.py.

7020 def __init__(self, solver=None, ctx=None, logFile=None):
7021 assert solver is None or ctx is not None
7022 self.ctx = _get_ctx(ctx)
7023 self.backtrack_level = 4000000000
7024 self.solver = None
7025 if solver is None:
7026 self.solver = Z3_mk_solver(self.ctx.ref())
7027 else:
7028 self.solver = solver
7029 Z3_solver_inc_ref(self.ctx.ref(), self.solver)
7030 if logFile is not None:
7031 self.set("smtlib2_log", logFile)
7032
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 7033 of file z3py.py.

7033 def __del__(self):
7034 if self.solver is not None and self.ctx.ref() is not None and Z3_solver_dec_ref is not None:
7035 Z3_solver_dec_ref(self.ctx.ref(), self.solver)
7036
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 7519 of file z3py.py.

7519 def __copy__(self):
7520 return self.translate(self.ctx)
7521

◆ __deepcopy__()

__deepcopy__ ( self,
memo = {} )

Definition at line 7522 of file z3py.py.

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

◆ __enter__()

__enter__ ( self)

Definition at line 7037 of file z3py.py.

7037 def __enter__(self):
7038 self.push()
7039 return self
7040

◆ __exit__()

__exit__ ( self,
* exc_info )

Definition at line 7041 of file z3py.py.

7041 def __exit__(self, *exc_info):
7042 self.pop()
7043

◆ __iadd__()

__iadd__ ( self,
fml )

Definition at line 7163 of file z3py.py.

7163 def __iadd__(self, fml):
7164 self.add(fml)
7165 return self
7166

◆ __repr__()

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

Definition at line 7502 of file z3py.py.

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

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

7152 def add(self, *args):
7153 """Assert constraints into the solver.
7154
7155 >>> x = Int('x')
7156 >>> s = Solver()
7157 >>> s.add(x > 0, x < 2)
7158 >>> s
7159 [x > 0, x < 2]
7160 """
7161 self.assert_exprs(*args)
7162

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

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

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

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

7133 def assert_exprs(self, *args):
7134 """Assert constraints into the solver.
7135
7136 >>> x = Int('x')
7137 >>> s = Solver()
7138 >>> s.assert_exprs(x > 0, x < 2)
7139 >>> s
7140 [x > 0, x < 2]
7141 """
7142 args = _get_args(args)
7143 s = BoolSort(self.ctx)
7144 for arg in args:
7145 if isinstance(arg, Goal) or isinstance(arg, AstVector):
7146 for f in arg:
7147 Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast())
7148 else:
7149 arg = s.cast(arg)
7150 Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast())
7151
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 7419 of file z3py.py.

7419 def assertions(self):
7420 """Return an AST vector containing all added constraints.
7421
7422 >>> s = Solver()
7423 >>> s.assertions()
7424 []
7425 >>> a = Int('a')
7426 >>> s.add(a > 0)
7427 >>> s.add(a < 10)
7428 >>> s.assertions()
7429 [a > 0, a < 10]
7430 """
7431 return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
7432
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 7219 of file z3py.py.

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

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

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

7368 def cube_vars(self):
7369 """Access the set of variables that were touched by the most recently generated cube.
7370 This set of variables can be used as a starting point for additional cubes.
7371 The idea is that variables that appear in clauses that are reduced by the most recent
7372 cube are likely more useful to cube on."""
7373 return self.cube_vs
7374

◆ dimacs()

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

Definition at line 7537 of file z3py.py.

7537 def dimacs(self, include_names=True):
7538 """Return a textual representation of the solver in DIMACS format."""
7539 return Z3_solver_to_dimacs_string(self.ctx.ref(), self.solver, include_names)
7540
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 7391 of file z3py.py.

7391 def explain_congruent(self, a, b):
7392 """Explain congruence of a and b relative to the current search state"""
7393 a = _py2expr(a, self.ctx)
7394 b = _py2expr(b, self.ctx)
7395 return _to_expr_ref(Z3_solver_congruence_explain(self.ctx.ref(), self.solver, a.ast, b.ast), self.ctx)
7396
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 7339 of file z3py.py.

7339 def from_file(self, filename):
7340 """Parse assertions from a file"""
7341 Z3_solver_from_file(self.ctx.ref(), self.solver, filename)
7342
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 7343 of file z3py.py.

7343 def from_string(self, s):
7344 """Parse assertions from a string"""
7345 Z3_solver_from_string(self.ctx.ref(), self.solver, s)
7346
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 7494 of file z3py.py.

7494 def help(self):
7495 """Display a string describing all available options."""
7496 print(Z3_solver_get_help(self.ctx.ref(), self.solver))
7497
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 7267 of file z3py.py.

7267 def import_model_converter(self, other):
7268 """Import model converter from other into the current solver"""
7269 Z3_solver_import_model_converter(self.ctx.ref(), other.solver, self.solver)
7270

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

7178 def insert(self, *args):
7179 """Assert constraints into the solver.
7180
7181 >>> x = Int('x')
7182 >>> s = Solver()
7183 >>> s.insert(x > 0, x < 2)
7184 >>> s
7185 [x > 0, x < 2]
7186 """
7187 self.assert_exprs(*args)
7188

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

7271 def interrupt(self):
7272 """Interrupt the execution of the solver object.
7273 Remarks: This ensures that the interrupt applies only
7274 to the given solver object and it applies only if it is running.
7275 """
7276 Z3_solver_interrupt(self.ctx.ref(), self.solver)
7277
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 7248 of file z3py.py.

7248 def model(self):
7249 """Return a model for the last `check()`.
7250
7251 This function raises an exception if
7252 a model is not available (e.g., last `check()` returned unsat).
7253
7254 >>> s = Solver()
7255 >>> a = Int('a')
7256 >>> s.add(a + 2 == 0)
7257 >>> s.check()
7258 sat
7259 >>> s.model()
7260 [a = -2]
7261 """
7262 try:
7263 return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx)
7264 except Z3Exception:
7265 raise Z3Exception("model is not available")
7266
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 7383 of file z3py.py.

7383 def next(self, t):
7384 """Retrieve congruence closure sibling of the term t relative to the current search state
7385 The function primarily works for SimpleSolver. Terms and variables that are
7386 eliminated during pre-processing are not visible to the congruence closure.
7387 """
7388 t = _py2expr(t, self.ctx)
7389 return _to_expr_ref(Z3_solver_congruence_next(self.ctx.ref(), self.solver, t.ast), self.ctx)
7390
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 7438 of file z3py.py.

7438 def non_units(self):
7439 """Return an AST vector containing all atomic formulas in solver state that are not units.
7440 """
7441 return AstVector(Z3_solver_get_non_units(self.ctx.ref(), self.solver), self.ctx)
7442
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 7101 of file z3py.py.

7101 def num_scopes(self):
7102 """Return the current number of backtracking points.
7103
7104 >>> s = Solver()
7105 >>> s.num_scopes()
7106 0
7107 >>> s.push()
7108 >>> s.num_scopes()
7109 1
7110 >>> s.push()
7111 >>> s.num_scopes()
7112 2
7113 >>> s.pop()
7114 >>> s.num_scopes()
7115 1
7116 """
7117 return Z3_solver_get_num_scopes(self.ctx.ref(), self.solver)
7118
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 7498 of file z3py.py.

7498 def param_descrs(self):
7499 """Return the parameter description set."""
7500 return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx)
7501
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 7079 of file z3py.py.

7079 def pop(self, num=1):
7080 """Backtrack \\c num backtracking points.
7081
7082 >>> x = Int('x')
7083 >>> s = Solver()
7084 >>> s.add(x > 0)
7085 >>> s
7086 [x > 0]
7087 >>> s.push()
7088 >>> s.add(x < 1)
7089 >>> s
7090 [x > 0, x < 1]
7091 >>> s.check()
7092 unsat
7093 >>> s.pop()
7094 >>> s.check()
7095 sat
7096 >>> s
7097 [x > 0]
7098 """
7099 Z3_solver_pop(self.ctx.ref(), self.solver, num)
7100
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 7415 of file z3py.py.

7415 def proof(self):
7416 """Return a proof for the last `check()`. Proof construction must be enabled."""
7417 return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
7418
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 7057 of file z3py.py.

7057 def push(self):
7058 """Create a backtracking point.
7059
7060 >>> x = Int('x')
7061 >>> s = Solver()
7062 >>> s.add(x > 0)
7063 >>> s
7064 [x > 0]
7065 >>> s.push()
7066 >>> s.add(x < 1)
7067 >>> s
7068 [x > 0, x < 1]
7069 >>> s.check()
7070 unsat
7071 >>> s.pop()
7072 >>> s.check()
7073 sat
7074 >>> s
7075 [x > 0]
7076 """
7077 Z3_solver_push(self.ctx.ref(), self.solver)
7078
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 7481 of file z3py.py.

7481 def reason_unknown(self):
7482 """Return a string describing why the last `check()` returned `unknown`.
7483
7484 >>> x = Int('x')
7485 >>> s = SimpleSolver()
7486 >>> s.add(2**x == 4)
7487 >>> s.check()
7488 unknown
7489 >>> s.reason_unknown()
7490 '(incomplete (theory arithmetic))'
7491 """
7492 return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver)
7493
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 7119 of file z3py.py.

7119 def reset(self):
7120 """Remove all asserted constraints and backtracking points created using `push()`.
7121
7122 >>> x = Int('x')
7123 >>> s = Solver()
7124 >>> s.add(x > 0)
7125 >>> s
7126 [x > 0]
7127 >>> s.reset()
7128 >>> s
7129 []
7130 """
7131 Z3_solver_reset(self.ctx.ref(), self.solver)
7132
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 7375 of file z3py.py.

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

7044 def set(self, *args, **keys):
7045 """Set a configuration option.
7046 The method `help()` return a string containing all available options.
7047
7048 >>> s = Solver()
7049 >>> # The option MBQI can be set using three different approaches.
7050 >>> s.set(mbqi=True)
7051 >>> s.set('MBQI', True)
7052 >>> s.set(':mbqi', True)
7053 """
7054 p = args2params(args, keys, self.ctx)
7055 Z3_solver_set_params(self.ctx.ref(), self.solver, p.params)
7056
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 7451 of file z3py.py.

7451 def set_initial_value(self, var, value):
7452 """initialize the solver's state by setting the initial value of var to value
7453 """
7454 s = var.sort()
7455 value = s.cast(value)
7456 Z3_solver_set_initial_value(self.ctx.ref(), self.solver, var.ast, value.ast)
7457
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 7525 of file z3py.py.

7525 def sexpr(self):
7526 """Return a formatted string (in Lisp-like format) with all added constraints.
7527 We say the string is in s-expression format.
7528
7529 >>> x = Int('x')
7530 >>> s = Solver()
7531 >>> s.add(x > 0)
7532 >>> s.add(x < 2)
7533 >>> r = s.sexpr()
7534 """
7535 return Z3_solver_to_string(self.ctx.ref(), self.solver)
7536
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 7403 of file z3py.py.

7403 def solve_for(self, ts):
7404 """Retrieve a solution for t relative to linear equations maintained in the current state."""
7405 vars = AstVector(ctx=self.ctx);
7406 terms = AstVector(ctx=self.ctx);
7407 guards = AstVector(ctx=self.ctx);
7408 for t in ts:
7409 t = _py2expr(t, self.ctx)
7410 vars.push(t)
7411 Z3_solver_solve_for(self.ctx.ref(), self.solver, vars.vector, terms.vector, guards.vector)
7412 return [(vars[i], terms[i], guards[i]) for i in range(len(vars))]
7413
7414
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 7397 of file z3py.py.

7397 def solve_for1(self, t):
7398 """Retrieve a solution for t relative to linear equations maintained in the current state.
7399 The function primarily works for SimpleSolver and when there is a solution using linear arithmetic."""
7400 t = _py2expr(t, self.ctx)
7401 return _to_expr_ref(Z3_solver_solve_for1(self.ctx.ref(), self.solver, t.ast), self.ctx)
7402

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

7463 def statistics(self):
7464 """Return statistics for the last `check()`.
7465
7466 >>> s = SimpleSolver()
7467 >>> x = Int('x')
7468 >>> s.add(x > 0)
7469 >>> s.check()
7470 sat
7471 >>> st = s.statistics()
7472 >>> st.get_key_value('final checks')
7473 1
7474 >>> len(st) > 0
7475 True
7476 >>> st[0] != 0
7477 True
7478 """
7479 return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx)
7480
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 7541 of file z3py.py.

7541 def to_smt2(self):
7542 """return SMTLIB2 formatted benchmark for solver's assertions"""
7543 es = self.assertions()
7544 sz = len(es)
7545 sz1 = sz
7546 if sz1 > 0:
7547 sz1 -= 1
7548 v = (Ast * sz1)()
7549 for i in range(sz1):
7550 v[i] = es[i].as_ast()
7551 if sz > 0:
7552 e = es[sz1].as_ast()
7553 else:
7554 e = BoolVal(True, self.ctx).as_ast()
7556 self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e,
7557 )
7558
7559
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 7458 of file z3py.py.

7458 def trail(self):
7459 """Return trail of the solver state after a check() call.
7460 """
7461 return AstVector(Z3_solver_get_trail(self.ctx.ref(), self.solver), self.ctx)
7462
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 7443 of file z3py.py.

7443 def trail_levels(self):
7444 """Return trail and decision levels of the solver state after a check() call.
7445 """
7446 trail = self.trail()
7447 levels = (ctypes.c_uint * len(trail))()
7448 Z3_solver_get_levels(self.ctx.ref(), self.solver, trail.vector, len(trail), levels)
7449 return trail, levels
7450
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 7506 of file z3py.py.

7506 def translate(self, target):
7507 """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
7508
7509 >>> c1 = Context()
7510 >>> c2 = Context()
7511 >>> s1 = Solver(ctx=c1)
7512 >>> s2 = s1.translate(c2)
7513 """
7514 if z3_debug():
7515 _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
7516 solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref())
7517 return Solver(solver, target)
7518
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 7433 of file z3py.py.

7433 def units(self):
7434 """Return an AST vector containing all currently inferred units.
7435 """
7436 return AstVector(Z3_solver_get_units(self.ctx.ref(), self.solver), self.ctx)
7437
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 7278 of file z3py.py.

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

◆ ctx

ctx = _get_ctx(ctx)

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

◆ solver

solver = None

Definition at line 7024 of file z3py.py.

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