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

Constructor & Destructor Documentation

◆ __init__()

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

Definition at line 6949 of file z3py.py.

6949 def __init__(self, solver=None, ctx=None, logFile=None):
6950 assert solver is None or ctx is not None
6951 self.ctx = _get_ctx(ctx)
6952 self.backtrack_level = 4000000000
6953 self.solver = None
6954 if solver is None:
6955 self.solver = Z3_mk_solver(self.ctx.ref())
6956 else:
6957 self.solver = solver
6958 Z3_solver_inc_ref(self.ctx.ref(), self.solver)
6959 if logFile is not None:
6960 self.set("smtlib2_log", logFile)
6961
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 6962 of file z3py.py.

6962 def __del__(self):
6963 if self.solver is not None and self.ctx.ref() is not None and Z3_solver_dec_ref is not None:
6964 Z3_solver_dec_ref(self.ctx.ref(), self.solver)
6965
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 7424 of file z3py.py.

7424 def __copy__(self):
7425 return self.translate(self.ctx)
7426

◆ __deepcopy__()

__deepcopy__ ( self,
memo = {} )

Definition at line 7427 of file z3py.py.

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

◆ __enter__()

__enter__ ( self)

Definition at line 6966 of file z3py.py.

6966 def __enter__(self):
6967 self.push()
6968 return self
6969

◆ __exit__()

__exit__ ( self,
* exc_info )

Definition at line 6970 of file z3py.py.

6970 def __exit__(self, *exc_info):
6971 self.pop()
6972

◆ __iadd__()

__iadd__ ( self,
fml )

Definition at line 7092 of file z3py.py.

7092 def __iadd__(self, fml):
7093 self.add(fml)
7094 return self
7095

◆ __repr__()

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

Definition at line 7407 of file z3py.py.

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

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

7081 def add(self, *args):
7082 """Assert constraints into the solver.
7083
7084 >>> x = Int('x')
7085 >>> s = Solver()
7086 >>> s.add(x > 0, x < 2)
7087 >>> s
7088 [x > 0, x < 2]
7089 """
7090 self.assert_exprs(*args)
7091

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

7096 def append(self, *args):
7097 """Assert constraints into the solver.
7098
7099 >>> x = Int('x')
7100 >>> s = Solver()
7101 >>> s.append(x > 0, x < 2)
7102 >>> s
7103 [x > 0, x < 2]
7104 """
7105 self.assert_exprs(*args)
7106

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

7118 def assert_and_track(self, a, p):
7119 """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
7120
7121 If `p` is a string, it will be automatically converted into a Boolean constant.
7122
7123 >>> x = Int('x')
7124 >>> p3 = Bool('p3')
7125 >>> s = Solver()
7126 >>> s.set(unsat_core=True)
7127 >>> s.assert_and_track(x > 0, 'p1')
7128 >>> s.assert_and_track(x != 1, 'p2')
7129 >>> s.assert_and_track(x < 0, p3)
7130 >>> print(s.check())
7131 unsat
7132 >>> c = s.unsat_core()
7133 >>> len(c)
7134 2
7135 >>> Bool('p1') in c
7136 True
7137 >>> Bool('p2') in c
7138 False
7139 >>> p3 in c
7140 True
7141 """
7142 if isinstance(p, str):
7143 p = Bool(p, self.ctx)
7144 _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
7145 _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
7146 Z3_solver_assert_and_track(self.ctx.ref(), self.solver, a.as_ast(), p.as_ast())
7147
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 7062 of file z3py.py.

7062 def assert_exprs(self, *args):
7063 """Assert constraints into the solver.
7064
7065 >>> x = Int('x')
7066 >>> s = Solver()
7067 >>> s.assert_exprs(x > 0, x < 2)
7068 >>> s
7069 [x > 0, x < 2]
7070 """
7071 args = _get_args(args)
7072 s = BoolSort(self.ctx)
7073 for arg in args:
7074 if isinstance(arg, Goal) or isinstance(arg, AstVector):
7075 for f in arg:
7076 Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast())
7077 else:
7078 arg = s.cast(arg)
7079 Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast())
7080
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 7324 of file z3py.py.

7324 def assertions(self):
7325 """Return an AST vector containing all added constraints.
7326
7327 >>> s = Solver()
7328 >>> s.assertions()
7329 []
7330 >>> a = Int('a')
7331 >>> s.add(a > 0)
7332 >>> s.add(a < 10)
7333 >>> s.assertions()
7334 [a > 0, a < 10]
7335 """
7336 return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
7337
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 7148 of file z3py.py.

7148 def check(self, *assumptions):
7149 """Check whether the assertions in the given solver plus the optional assumptions are consistent or not.
7150
7151 >>> x = Int('x')
7152 >>> s = Solver()
7153 >>> s.check()
7154 sat
7155 >>> s.add(x > 0, x < 2)
7156 >>> s.check()
7157 sat
7158 >>> s.model().eval(x)
7159 1
7160 >>> s.add(x < 1)
7161 >>> s.check()
7162 unsat
7163 >>> s.reset()
7164 >>> s.add(2**x == 4)
7165 >>> s.check()
7166 unknown
7167 """
7168 s = BoolSort(self.ctx)
7169 assumptions = _get_args(assumptions)
7170 num = len(assumptions)
7171 _assumptions = (Ast * num)()
7172 for i in range(num):
7173 _assumptions[i] = s.cast(assumptions[i]).as_ast()
7174 r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions)
7175 return CheckSatResult(r)
7176
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 7239 of file z3py.py.

7239 def consequences(self, assumptions, variables):
7240 """Determine fixed values for the variables based on the solver state and assumptions.
7241 >>> s = Solver()
7242 >>> a, b, c, d = Bools('a b c d')
7243 >>> s.add(Implies(a,b), Implies(b, c))
7244 >>> s.consequences([a],[b,c,d])
7245 (sat, [Implies(a, b), Implies(a, c)])
7246 >>> s.consequences([Not(c),d],[a,b,c,d])
7247 (sat, [Implies(d, d), Implies(Not(c), Not(c)), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))])
7248 """
7249 if isinstance(assumptions, list):
7250 _asms = AstVector(None, self.ctx)
7251 for a in assumptions:
7252 _asms.push(a)
7253 assumptions = _asms
7254 if isinstance(variables, list):
7255 _vars = AstVector(None, self.ctx)
7256 for a in variables:
7257 _vars.push(a)
7258 variables = _vars
7259 _z3_assert(isinstance(assumptions, AstVector), "ast vector expected")
7260 _z3_assert(isinstance(variables, AstVector), "ast vector expected")
7261 consequences = AstVector(None, self.ctx)
7262 r = Z3_solver_get_consequences(self.ctx.ref(), self.solver, assumptions.vector,
7263 variables.vector, consequences.vector)
7264 sz = len(consequences)
7265 consequences = [consequences[i] for i in range(sz)]
7266 return CheckSatResult(r), consequences
7267
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 7276 of file z3py.py.

7276 def cube(self, vars=None):
7277 """Get set of cubes
7278 The method takes an optional set of variables that restrict which
7279 variables may be used as a starting point for cubing.
7280 If vars is not None, then the first case split is based on a variable in
7281 this set.
7282 """
7283 self.cube_vs = AstVector(None, self.ctx)
7284 if vars is not None:
7285 for v in vars:
7286 self.cube_vs.push(v)
7287 while True:
7288 lvl = self.backtrack_level
7289 self.backtrack_level = 4000000000
7290 r = AstVector(Z3_solver_cube(self.ctx.ref(), self.solver, self.cube_vs.vector, lvl), self.ctx)
7291 if (len(r) == 1 and is_false(r[0])):
7292 return
7293 yield r
7294 if (len(r) == 0):
7295 return
7296
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 7297 of file z3py.py.

7297 def cube_vars(self):
7298 """Access the set of variables that were touched by the most recently generated cube.
7299 This set of variables can be used as a starting point for additional cubes.
7300 The idea is that variables that appear in clauses that are reduced by the most recent
7301 cube are likely more useful to cube on."""
7302 return self.cube_vs
7303

◆ dimacs()

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

Definition at line 7442 of file z3py.py.

7442 def dimacs(self, include_names=True):
7443 """Return a textual representation of the solver in DIMACS format."""
7444 return Z3_solver_to_dimacs_string(self.ctx.ref(), self.solver, include_names)
7445
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 7268 of file z3py.py.

7268 def from_file(self, filename):
7269 """Parse assertions from a file"""
7270 Z3_solver_from_file(self.ctx.ref(), self.solver, filename)
7271
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 7272 of file z3py.py.

7272 def from_string(self, s):
7273 """Parse assertions from a string"""
7274 Z3_solver_from_string(self.ctx.ref(), self.solver, s)
7275
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 7399 of file z3py.py.

7399 def help(self):
7400 """Display a string describing all available options."""
7401 print(Z3_solver_get_help(self.ctx.ref(), self.solver))
7402
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 7196 of file z3py.py.

7196 def import_model_converter(self, other):
7197 """Import model converter from other into the current solver"""
7198 Z3_solver_import_model_converter(self.ctx.ref(), other.solver, self.solver)
7199

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

7107 def insert(self, *args):
7108 """Assert constraints into the solver.
7109
7110 >>> x = Int('x')
7111 >>> s = Solver()
7112 >>> s.insert(x > 0, x < 2)
7113 >>> s
7114 [x > 0, x < 2]
7115 """
7116 self.assert_exprs(*args)
7117

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

7200 def interrupt(self):
7201 """Interrupt the execution of the solver object.
7202 Remarks: This ensures that the interrupt applies only
7203 to the given solver object and it applies only if it is running.
7204 """
7205 Z3_solver_interrupt(self.ctx.ref(), self.solver)
7206
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 7177 of file z3py.py.

7177 def model(self):
7178 """Return a model for the last `check()`.
7179
7180 This function raises an exception if
7181 a model is not available (e.g., last `check()` returned unsat).
7182
7183 >>> s = Solver()
7184 >>> a = Int('a')
7185 >>> s.add(a + 2 == 0)
7186 >>> s.check()
7187 sat
7188 >>> s.model()
7189 [a = -2]
7190 """
7191 try:
7192 return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx)
7193 except Z3Exception:
7194 raise Z3Exception("model is not available")
7195
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.sexpr(), ModelRef.translate(), and ModelRef.update_value().

◆ next()

next ( self,
t )

Definition at line 7312 of file z3py.py.

7312 def next(self, t):
7313 t = _py2expr(t, self.ctx)
7314 """Retrieve congruence closure sibling of the term t relative to the current search state
7315 The function primarily works for SimpleSolver. Terms and variables that are
7316 eliminated during pre-processing are not visible to the congruence closure.
7317 """
7318 return _to_expr_ref(Z3_solver_congruence_next(self.ctx.ref(), self.solver, t.ast), self.ctx)
7319
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 7343 of file z3py.py.

7343 def non_units(self):
7344 """Return an AST vector containing all atomic formulas in solver state that are not units.
7345 """
7346 return AstVector(Z3_solver_get_non_units(self.ctx.ref(), self.solver), self.ctx)
7347
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 7030 of file z3py.py.

7030 def num_scopes(self):
7031 """Return the current number of backtracking points.
7032
7033 >>> s = Solver()
7034 >>> s.num_scopes()
7035 0
7036 >>> s.push()
7037 >>> s.num_scopes()
7038 1
7039 >>> s.push()
7040 >>> s.num_scopes()
7041 2
7042 >>> s.pop()
7043 >>> s.num_scopes()
7044 1
7045 """
7046 return Z3_solver_get_num_scopes(self.ctx.ref(), self.solver)
7047
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 7403 of file z3py.py.

7403 def param_descrs(self):
7404 """Return the parameter description set."""
7405 return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx)
7406
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 7008 of file z3py.py.

7008 def pop(self, num=1):
7009 """Backtrack \\c num backtracking points.
7010
7011 >>> x = Int('x')
7012 >>> s = Solver()
7013 >>> s.add(x > 0)
7014 >>> s
7015 [x > 0]
7016 >>> s.push()
7017 >>> s.add(x < 1)
7018 >>> s
7019 [x > 0, x < 1]
7020 >>> s.check()
7021 unsat
7022 >>> s.pop()
7023 >>> s.check()
7024 sat
7025 >>> s
7026 [x > 0]
7027 """
7028 Z3_solver_pop(self.ctx.ref(), self.solver, num)
7029
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 7320 of file z3py.py.

7320 def proof(self):
7321 """Return a proof for the last `check()`. Proof construction must be enabled."""
7322 return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
7323
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 6986 of file z3py.py.

6986 def push(self):
6987 """Create a backtracking point.
6988
6989 >>> x = Int('x')
6990 >>> s = Solver()
6991 >>> s.add(x > 0)
6992 >>> s
6993 [x > 0]
6994 >>> s.push()
6995 >>> s.add(x < 1)
6996 >>> s
6997 [x > 0, x < 1]
6998 >>> s.check()
6999 unsat
7000 >>> s.pop()
7001 >>> s.check()
7002 sat
7003 >>> s
7004 [x > 0]
7005 """
7006 Z3_solver_push(self.ctx.ref(), self.solver)
7007
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 7386 of file z3py.py.

7386 def reason_unknown(self):
7387 """Return a string describing why the last `check()` returned `unknown`.
7388
7389 >>> x = Int('x')
7390 >>> s = SimpleSolver()
7391 >>> s.add(2**x == 4)
7392 >>> s.check()
7393 unknown
7394 >>> s.reason_unknown()
7395 '(incomplete (theory arithmetic))'
7396 """
7397 return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver)
7398
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 7048 of file z3py.py.

7048 def reset(self):
7049 """Remove all asserted constraints and backtracking points created using `push()`.
7050
7051 >>> x = Int('x')
7052 >>> s = Solver()
7053 >>> s.add(x > 0)
7054 >>> s
7055 [x > 0]
7056 >>> s.reset()
7057 >>> s
7058 []
7059 """
7060 Z3_solver_reset(self.ctx.ref(), self.solver)
7061
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 7304 of file z3py.py.

7304 def root(self, t):
7305 t = _py2expr(t, self.ctx)
7306 """Retrieve congruence closure root of the term t relative to the current search state
7307 The function primarily works for SimpleSolver. Terms and variables that are
7308 eliminated during pre-processing are not visible to the congruence closure.
7309 """
7310 return _to_expr_ref(Z3_solver_congruence_root(self.ctx.ref(), self.solver, t.ast), self.ctx)
7311
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 6973 of file z3py.py.

6973 def set(self, *args, **keys):
6974 """Set a configuration option.
6975 The method `help()` return a string containing all available options.
6976
6977 >>> s = Solver()
6978 >>> # The option MBQI can be set using three different approaches.
6979 >>> s.set(mbqi=True)
6980 >>> s.set('MBQI', True)
6981 >>> s.set(':mbqi', True)
6982 """
6983 p = args2params(args, keys, self.ctx)
6984 Z3_solver_set_params(self.ctx.ref(), self.solver, p.params)
6985
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 7356 of file z3py.py.

7356 def set_initial_value(self, var, value):
7357 """initialize the solver's state by setting the initial value of var to value
7358 """
7359 s = var.sort()
7360 value = s.cast(value)
7361 Z3_solver_set_initial_value(self.ctx.ref(), self.solver, var.ast, value.ast)
7362
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 7430 of file z3py.py.

7430 def sexpr(self):
7431 """Return a formatted string (in Lisp-like format) with all added constraints.
7432 We say the string is in s-expression format.
7433
7434 >>> x = Int('x')
7435 >>> s = Solver()
7436 >>> s.add(x > 0)
7437 >>> s.add(x < 2)
7438 >>> r = s.sexpr()
7439 """
7440 return Z3_solver_to_string(self.ctx.ref(), self.solver)
7441
Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s)
Convert a solver into a string.

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

7368 def statistics(self):
7369 """Return statistics for the last `check()`.
7370
7371 >>> s = SimpleSolver()
7372 >>> x = Int('x')
7373 >>> s.add(x > 0)
7374 >>> s.check()
7375 sat
7376 >>> st = s.statistics()
7377 >>> st.get_key_value('final checks')
7378 1
7379 >>> len(st) > 0
7380 True
7381 >>> st[0] != 0
7382 True
7383 """
7384 return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx)
7385
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 7446 of file z3py.py.

7446 def to_smt2(self):
7447 """return SMTLIB2 formatted benchmark for solver's assertions"""
7448 es = self.assertions()
7449 sz = len(es)
7450 sz1 = sz
7451 if sz1 > 0:
7452 sz1 -= 1
7453 v = (Ast * sz1)()
7454 for i in range(sz1):
7455 v[i] = es[i].as_ast()
7456 if sz > 0:
7457 e = es[sz1].as_ast()
7458 else:
7459 e = BoolVal(True, self.ctx).as_ast()
7461 self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e,
7462 )
7463
7464
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 7363 of file z3py.py.

7363 def trail(self):
7364 """Return trail of the solver state after a check() call.
7365 """
7366 return AstVector(Z3_solver_get_trail(self.ctx.ref(), self.solver), self.ctx)
7367
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 7348 of file z3py.py.

7348 def trail_levels(self):
7349 """Return trail and decision levels of the solver state after a check() call.
7350 """
7351 trail = self.trail()
7352 levels = (ctypes.c_uint * len(trail))()
7353 Z3_solver_get_levels(self.ctx.ref(), self.solver, trail.vector, len(trail), levels)
7354 return trail, levels
7355
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 7411 of file z3py.py.

7411 def translate(self, target):
7412 """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
7413
7414 >>> c1 = Context()
7415 >>> c2 = Context()
7416 >>> s1 = Solver(ctx=c1)
7417 >>> s2 = s1.translate(c2)
7418 """
7419 if z3_debug():
7420 _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
7421 solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref())
7422 return Solver(solver, target)
7423
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 7338 of file z3py.py.

7338 def units(self):
7339 """Return an AST vector containing all currently inferred units.
7340 """
7341 return AstVector(Z3_solver_get_units(self.ctx.ref(), self.solver), self.ctx)
7342
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 7207 of file z3py.py.

7207 def unsat_core(self):
7208 """Return a subset (as an AST vector) of the assumptions provided to the last check().
7209
7210 These are the assumptions Z3 used in the unsatisfiability proof.
7211 Assumptions are available in Z3. They are used to extract unsatisfiable cores.
7212 They may be also used to "retract" assumptions. Note that, assumptions are not really
7213 "soft constraints", but they can be used to implement them.
7214
7215 >>> p1, p2, p3 = Bools('p1 p2 p3')
7216 >>> x, y = Ints('x y')
7217 >>> s = Solver()
7218 >>> s.add(Implies(p1, x > 0))
7219 >>> s.add(Implies(p2, y > x))
7220 >>> s.add(Implies(p2, y < 1))
7221 >>> s.add(Implies(p3, y > -3))
7222 >>> s.check(p1, p2, p3)
7223 unsat
7224 >>> core = s.unsat_core()
7225 >>> len(core)
7226 2
7227 >>> p1 in core
7228 True
7229 >>> p2 in core
7230 True
7231 >>> p3 in core
7232 False
7233 >>> # "Retracting" p2
7234 >>> s.check(p1, p3)
7235 sat
7236 """
7237 return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx)
7238
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 6952 of file z3py.py.

◆ ctx

ctx = _get_ctx(ctx)

Definition at line 6951 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(), 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 7283 of file z3py.py.

◆ solver