Z3
 
Loading...
Searching...
No Matches
Public Member Functions | Data Fields
Solver Class Reference
+ Inheritance diagram for Solver:

Public Member Functions

def __init__ (self, solver=None, ctx=None, logFile=None)
 
def __del__ (self)
 
def set (self, *args, **keys)
 
def push (self)
 
def pop (self, num=1)
 
def num_scopes (self)
 
def reset (self)
 
def assert_exprs (self, *args)
 
def add (self, *args)
 
def __iadd__ (self, fml)
 
def append (self, *args)
 
def insert (self, *args)
 
def assert_and_track (self, a, p)
 
def check (self, *assumptions)
 
def model (self)
 
def import_model_converter (self, other)
 
def unsat_core (self)
 
def consequences (self, assumptions, variables)
 
def from_file (self, filename)
 
def from_string (self, s)
 
def cube (self, vars=None)
 
def cube_vars (self)
 
def root (self, t)
 
def next (self, t)
 
def proof (self)
 
def assertions (self)
 
def units (self)
 
def non_units (self)
 
def trail_levels (self)
 
def trail (self)
 
def statistics (self)
 
def reason_unknown (self)
 
def help (self)
 
def param_descrs (self)
 
def __repr__ (self)
 
def translate (self, target)
 
def __copy__ (self)
 
def __deepcopy__ (self, memo={})
 
def sexpr (self)
 
def dimacs (self, include_names=True)
 
def to_smt2 (self)
 
- Public Member Functions inherited from Z3PPObject
def use_pp (self)
 

Data Fields

 ctx
 
 backtrack_level
 
 solver
 
 cube_vs
 

Additional Inherited Members

- Protected Member Functions inherited from Z3PPObject
def _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 6897 of file z3py.py.

Constructor & Destructor Documentation

◆ __init__()

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

Definition at line 6903 of file z3py.py.

6903 def __init__(self, solver=None, ctx=None, logFile=None):
6904 assert solver is None or ctx is not None
6905 self.ctx = _get_ctx(ctx)
6906 self.backtrack_level = 4000000000
6907 self.solver = None
6908 if solver is None:
6909 self.solver = Z3_mk_solver(self.ctx.ref())
6910 else:
6911 self.solver = solver
6912 Z3_solver_inc_ref(self.ctx.ref(), self.solver)
6913 if logFile is not None:
6914 self.set("smtlib2_log", logFile)
6915
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__()

def __del__ (   self)

Definition at line 6916 of file z3py.py.

6916 def __del__(self):
6917 if self.solver is not None and self.ctx.ref() is not None and Z3_solver_dec_ref is not None:
6918 Z3_solver_dec_ref(self.ctx.ref(), self.solver)
6919
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__()

def __copy__ (   self)

Definition at line 7357 of file z3py.py.

7357 def __copy__(self):
7358 return self.translate(self.ctx)
7359

◆ __deepcopy__()

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 7360 of file z3py.py.

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

◆ __iadd__()

def __iadd__ (   self,
  fml 
)

Definition at line 7039 of file z3py.py.

7039 def __iadd__(self, fml):
7040 self.add(fml)
7041 return self
7042

◆ __repr__()

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

Definition at line 7340 of file z3py.py.

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

◆ add()

def add (   self,
args 
)
Assert constraints into the solver.

>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0, x < 2)
>>> s
[x > 0, x < 2]

Definition at line 7028 of file z3py.py.

7028 def add(self, *args):
7029 """Assert constraints into the solver.
7030
7031 >>> x = Int('x')
7032 >>> s = Solver()
7033 >>> s.add(x > 0, x < 2)
7034 >>> s
7035 [x > 0, x < 2]
7036 """
7037 self.assert_exprs(*args)
7038

Referenced by Solver.__iadd__(), Fixedpoint.__iadd__(), and Optimize.__iadd__().

◆ append()

def append (   self,
args 
)
Assert constraints into the solver.

>>> x = Int('x')
>>> s = Solver()
>>> s.append(x > 0, x < 2)
>>> s
[x > 0, x < 2]

Definition at line 7043 of file z3py.py.

7043 def append(self, *args):
7044 """Assert constraints into the solver.
7045
7046 >>> x = Int('x')
7047 >>> s = Solver()
7048 >>> s.append(x > 0, x < 2)
7049 >>> s
7050 [x > 0, x < 2]
7051 """
7052 self.assert_exprs(*args)
7053

◆ assert_and_track()

def assert_and_track (   self,
  a,
  p 
)
Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.

If `p` is a string, it will be automatically converted into a Boolean constant.

>>> x = Int('x')
>>> p3 = Bool('p3')
>>> s = Solver()
>>> s.set(unsat_core=True)
>>> s.assert_and_track(x > 0,  'p1')
>>> s.assert_and_track(x != 1, 'p2')
>>> s.assert_and_track(x < 0,  p3)
>>> print(s.check())
unsat
>>> c = s.unsat_core()
>>> len(c)
2
>>> Bool('p1') in c
True
>>> Bool('p2') in c
False
>>> p3 in c
True

Definition at line 7065 of file z3py.py.

7065 def assert_and_track(self, a, p):
7066 """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
7067
7068 If `p` is a string, it will be automatically converted into a Boolean constant.
7069
7070 >>> x = Int('x')
7071 >>> p3 = Bool('p3')
7072 >>> s = Solver()
7073 >>> s.set(unsat_core=True)
7074 >>> s.assert_and_track(x > 0, 'p1')
7075 >>> s.assert_and_track(x != 1, 'p2')
7076 >>> s.assert_and_track(x < 0, p3)
7077 >>> print(s.check())
7078 unsat
7079 >>> c = s.unsat_core()
7080 >>> len(c)
7081 2
7082 >>> Bool('p1') in c
7083 True
7084 >>> Bool('p2') in c
7085 False
7086 >>> p3 in c
7087 True
7088 """
7089 if isinstance(p, str):
7090 p = Bool(p, self.ctx)
7091 _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
7092 _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
7093 Z3_solver_assert_and_track(self.ctx.ref(), self.solver, a.as_ast(), p.as_ast())
7094
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()

def assert_exprs (   self,
args 
)
Assert constraints into the solver.

>>> x = Int('x')
>>> s = Solver()
>>> s.assert_exprs(x > 0, x < 2)
>>> s
[x > 0, x < 2]

Definition at line 7009 of file z3py.py.

7009 def assert_exprs(self, *args):
7010 """Assert constraints into the solver.
7011
7012 >>> x = Int('x')
7013 >>> s = Solver()
7014 >>> s.assert_exprs(x > 0, x < 2)
7015 >>> s
7016 [x > 0, x < 2]
7017 """
7018 args = _get_args(args)
7019 s = BoolSort(self.ctx)
7020 for arg in args:
7021 if isinstance(arg, Goal) or isinstance(arg, AstVector):
7022 for f in arg:
7023 Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast())
7024 else:
7025 arg = s.cast(arg)
7026 Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast())
7027
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(), Fixedpoint.add(), Optimize.add(), Goal.append(), Solver.append(), Fixedpoint.append(), Goal.insert(), Solver.insert(), and Fixedpoint.insert().

◆ assertions()

def assertions (   self)
Return an AST vector containing all added constraints.

>>> s = Solver()
>>> s.assertions()
[]
>>> a = Int('a')
>>> s.add(a > 0)
>>> s.add(a < 10)
>>> s.assertions()
[a > 0, a < 10]

Definition at line 7264 of file z3py.py.

7264 def assertions(self):
7265 """Return an AST vector containing all added constraints.
7266
7267 >>> s = Solver()
7268 >>> s.assertions()
7269 []
7270 >>> a = Int('a')
7271 >>> s.add(a > 0)
7272 >>> s.add(a < 10)
7273 >>> s.assertions()
7274 [a > 0, a < 10]
7275 """
7276 return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
7277
Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s)
Return the set of asserted formulas on the solver.

Referenced by Solver.to_smt2().

◆ check()

def check (   self,
assumptions 
)
Check whether the assertions in the given solver plus the optional assumptions are consistent or not.

>>> x = Int('x')
>>> s = Solver()
>>> s.check()
sat
>>> s.add(x > 0, x < 2)
>>> s.check()
sat
>>> s.model().eval(x)
1
>>> s.add(x < 1)
>>> s.check()
unsat
>>> s.reset()
>>> s.add(2**x == 4)
>>> s.check()
unknown

Definition at line 7095 of file z3py.py.

7095 def check(self, *assumptions):
7096 """Check whether the assertions in the given solver plus the optional assumptions are consistent or not.
7097
7098 >>> x = Int('x')
7099 >>> s = Solver()
7100 >>> s.check()
7101 sat
7102 >>> s.add(x > 0, x < 2)
7103 >>> s.check()
7104 sat
7105 >>> s.model().eval(x)
7106 1
7107 >>> s.add(x < 1)
7108 >>> s.check()
7109 unsat
7110 >>> s.reset()
7111 >>> s.add(2**x == 4)
7112 >>> s.check()
7113 unknown
7114 """
7115 s = BoolSort(self.ctx)
7116 assumptions = _get_args(assumptions)
7117 num = len(assumptions)
7118 _assumptions = (Ast * num)()
7119 for i in range(num):
7120 _assumptions[i] = s.cast(assumptions[i]).as_ast()
7121 r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions)
7122 return CheckSatResult(r)
7123
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.

Referenced by Solver.model().

◆ consequences()

def consequences (   self,
  assumptions,
  variables 
)
Determine fixed values for the variables based on the solver state and assumptions.
>>> s = Solver()
>>> a, b, c, d = Bools('a b c d')
>>> s.add(Implies(a,b), Implies(b, c))
>>> s.consequences([a],[b,c,d])
(sat, [Implies(a, b), Implies(a, c)])
>>> s.consequences([Not(c),d],[a,b,c,d])
(sat, [Implies(d, d), Implies(Not(c), Not(c)), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))])

Definition at line 7179 of file z3py.py.

7179 def consequences(self, assumptions, variables):
7180 """Determine fixed values for the variables based on the solver state and assumptions.
7181 >>> s = Solver()
7182 >>> a, b, c, d = Bools('a b c d')
7183 >>> s.add(Implies(a,b), Implies(b, c))
7184 >>> s.consequences([a],[b,c,d])
7185 (sat, [Implies(a, b), Implies(a, c)])
7186 >>> s.consequences([Not(c),d],[a,b,c,d])
7187 (sat, [Implies(d, d), Implies(Not(c), Not(c)), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))])
7188 """
7189 if isinstance(assumptions, list):
7190 _asms = AstVector(None, self.ctx)
7191 for a in assumptions:
7192 _asms.push(a)
7193 assumptions = _asms
7194 if isinstance(variables, list):
7195 _vars = AstVector(None, self.ctx)
7196 for a in variables:
7197 _vars.push(a)
7198 variables = _vars
7199 _z3_assert(isinstance(assumptions, AstVector), "ast vector expected")
7200 _z3_assert(isinstance(variables, AstVector), "ast vector expected")
7201 consequences = AstVector(None, self.ctx)
7202 r = Z3_solver_get_consequences(self.ctx.ref(), self.solver, assumptions.vector,
7203 variables.vector, consequences.vector)
7204 sz = len(consequences)
7205 consequences = [consequences[i] for i in range(sz)]
7206 return CheckSatResult(r), consequences
7207
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()

def cube (   self,
  vars = None 
)
Get set of cubes
The method takes an optional set of variables that restrict which
variables may be used as a starting point for cubing.
If vars is not None, then the first case split is based on a variable in
this set.

Definition at line 7216 of file z3py.py.

7216 def cube(self, vars=None):
7217 """Get set of cubes
7218 The method takes an optional set of variables that restrict which
7219 variables may be used as a starting point for cubing.
7220 If vars is not None, then the first case split is based on a variable in
7221 this set.
7222 """
7223 self.cube_vs = AstVector(None, self.ctx)
7224 if vars is not None:
7225 for v in vars:
7226 self.cube_vs.push(v)
7227 while True:
7228 lvl = self.backtrack_level
7229 self.backtrack_level = 4000000000
7230 r = AstVector(Z3_solver_cube(self.ctx.ref(), self.solver, self.cube_vs.vector, lvl), self.ctx)
7231 if (len(r) == 1 and is_false(r[0])):
7232 return
7233 yield r
7234 if (len(r) == 0):
7235 return
7236
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()

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

Definition at line 7237 of file z3py.py.

7237 def cube_vars(self):
7238 """Access the set of variables that were touched by the most recently generated cube.
7239 This set of variables can be used as a starting point for additional cubes.
7240 The idea is that variables that appear in clauses that are reduced by the most recent
7241 cube are likely more useful to cube on."""
7242 return self.cube_vs
7243

◆ dimacs()

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

Definition at line 7375 of file z3py.py.

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

def from_file (   self,
  filename 
)
Parse assertions from a file

Definition at line 7208 of file z3py.py.

7208 def from_file(self, filename):
7209 """Parse assertions from a file"""
7210 Z3_solver_from_file(self.ctx.ref(), self.solver, filename)
7211
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()

def from_string (   self,
  s 
)
Parse assertions from a string

Definition at line 7212 of file z3py.py.

7212 def from_string(self, s):
7213 """Parse assertions from a string"""
7214 Z3_solver_from_string(self.ctx.ref(), self.solver, s)
7215
void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string file_name)
load solver assertions from a string.

◆ help()

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

Definition at line 7332 of file z3py.py.

7332 def help(self):
7333 """Display a string describing all available options."""
7334 print(Z3_solver_get_help(self.ctx.ref(), self.solver))
7335
Z3_string Z3_API Z3_solver_get_help(Z3_context c, Z3_solver s)
Return a string describing all solver available parameters.

Referenced by Solver.set().

◆ import_model_converter()

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

Definition at line 7143 of file z3py.py.

7143 def import_model_converter(self, other):
7144 """Import model converter from other into the current solver"""
7145 Z3_solver_import_model_converter(self.ctx.ref(), other.solver, self.solver)
7146
void Z3_API Z3_solver_import_model_converter(Z3_context ctx, Z3_solver src, Z3_solver dst)
Ad-hoc method for importing model conversion from solver.

◆ insert()

def insert (   self,
args 
)
Assert constraints into the solver.

>>> x = Int('x')
>>> s = Solver()
>>> s.insert(x > 0, x < 2)
>>> s
[x > 0, x < 2]

Definition at line 7054 of file z3py.py.

7054 def insert(self, *args):
7055 """Assert constraints into the solver.
7056
7057 >>> x = Int('x')
7058 >>> s = Solver()
7059 >>> s.insert(x > 0, x < 2)
7060 >>> s
7061 [x > 0, x < 2]
7062 """
7063 self.assert_exprs(*args)
7064

◆ model()

def model (   self)
Return a model for the last `check()`.

This function raises an exception if
a model is not available (e.g., last `check()` returned unsat).

>>> s = Solver()
>>> a = Int('a')
>>> s.add(a + 2 == 0)
>>> s.check()
sat
>>> s.model()
[a = -2]

Definition at line 7124 of file z3py.py.

7124 def model(self):
7125 """Return a model for the last `check()`.
7126
7127 This function raises an exception if
7128 a model is not available (e.g., last `check()` returned unsat).
7129
7130 >>> s = Solver()
7131 >>> a = Int('a')
7132 >>> s.add(a + 2 == 0)
7133 >>> s.check()
7134 sat
7135 >>> s.model()
7136 [a = -2]
7137 """
7138 try:
7139 return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx)
7140 except Z3Exception:
7141 raise Z3Exception("model is not available")
7142
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(), FuncInterp.translate(), ModelRef.translate(), and ModelRef.update_value().

◆ next()

def next (   self,
  t 
)

Definition at line 7252 of file z3py.py.

7252 def next(self, t):
7253 t = _py2expr(t, self.ctx)
7254 """Retrieve congruence closure sibling of the term t relative to the current search state
7255 The function primarily works for SimpleSolver. Terms and variables that are
7256 eliminated during pre-processing are not visible to the congruence closure.
7257 """
7258 return _to_expr_ref(Z3_solver_congruence_next(self.ctx.ref(), self.solver, t.ast), self.ctx)
7259
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()

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

Definition at line 7283 of file z3py.py.

7283 def non_units(self):
7284 """Return an AST vector containing all atomic formulas in solver state that are not units.
7285 """
7286 return AstVector(Z3_solver_get_non_units(self.ctx.ref(), self.solver), self.ctx)
7287
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()

def num_scopes (   self)
Return the current number of backtracking points.

>>> s = Solver()
>>> s.num_scopes()
0
>>> s.push()
>>> s.num_scopes()
1
>>> s.push()
>>> s.num_scopes()
2
>>> s.pop()
>>> s.num_scopes()
1

Definition at line 6977 of file z3py.py.

6977 def num_scopes(self):
6978 """Return the current number of backtracking points.
6979
6980 >>> s = Solver()
6981 >>> s.num_scopes()
6982 0
6983 >>> s.push()
6984 >>> s.num_scopes()
6985 1
6986 >>> s.push()
6987 >>> s.num_scopes()
6988 2
6989 >>> s.pop()
6990 >>> s.num_scopes()
6991 1
6992 """
6993 return Z3_solver_get_num_scopes(self.ctx.ref(), self.solver)
6994
unsigned Z3_API Z3_solver_get_num_scopes(Z3_context c, Z3_solver s)
Return the number of backtracking points.

◆ param_descrs()

def param_descrs (   self)
Return the parameter description set.

Definition at line 7336 of file z3py.py.

7336 def param_descrs(self):
7337 """Return the parameter description set."""
7338 return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx)
7339
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()

def pop (   self,
  num = 1 
)
Backtrack \\c num backtracking points.

>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0)
>>> s
[x > 0]
>>> s.push()
>>> s.add(x < 1)
>>> s
[x > 0, x < 1]
>>> s.check()
unsat
>>> s.pop()
>>> s.check()
sat
>>> s
[x > 0]

Definition at line 6955 of file z3py.py.

6955 def pop(self, num=1):
6956 """Backtrack \\c num backtracking points.
6957
6958 >>> x = Int('x')
6959 >>> s = Solver()
6960 >>> s.add(x > 0)
6961 >>> s
6962 [x > 0]
6963 >>> s.push()
6964 >>> s.add(x < 1)
6965 >>> s
6966 [x > 0, x < 1]
6967 >>> s.check()
6968 unsat
6969 >>> s.pop()
6970 >>> s.check()
6971 sat
6972 >>> s
6973 [x > 0]
6974 """
6975 Z3_solver_pop(self.ctx.ref(), self.solver, num)
6976
void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n)
Backtrack n backtracking points.

◆ proof()

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

Definition at line 7260 of file z3py.py.

7260 def proof(self):
7261 """Return a proof for the last `check()`. Proof construction must be enabled."""
7262 return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
7263
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()

def push (   self)
Create a backtracking point.

>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0)
>>> s
[x > 0]
>>> s.push()
>>> s.add(x < 1)
>>> s
[x > 0, x < 1]
>>> s.check()
unsat
>>> s.pop()
>>> s.check()
sat
>>> s
[x > 0]

Definition at line 6933 of file z3py.py.

6933 def push(self):
6934 """Create a backtracking point.
6935
6936 >>> x = Int('x')
6937 >>> s = Solver()
6938 >>> s.add(x > 0)
6939 >>> s
6940 [x > 0]
6941 >>> s.push()
6942 >>> s.add(x < 1)
6943 >>> s
6944 [x > 0, x < 1]
6945 >>> s.check()
6946 unsat
6947 >>> s.pop()
6948 >>> s.check()
6949 sat
6950 >>> s
6951 [x > 0]
6952 """
6953 Z3_solver_push(self.ctx.ref(), self.solver)
6954
void Z3_API Z3_solver_push(Z3_context c, Z3_solver s)
Create a backtracking point.

◆ reason_unknown()

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

7319 def reason_unknown(self):
7320 """Return a string describing why the last `check()` returned `unknown`.
7321
7322 >>> x = Int('x')
7323 >>> s = SimpleSolver()
7324 >>> s.add(2**x == 4)
7325 >>> s.check()
7326 unknown
7327 >>> s.reason_unknown()
7328 '(incomplete (theory arithmetic))'
7329 """
7330 return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver)
7331
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()

def reset (   self)
Remove all asserted constraints and backtracking points created using `push()`.

>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0)
>>> s
[x > 0]
>>> s.reset()
>>> s
[]

Definition at line 6995 of file z3py.py.

6995 def reset(self):
6996 """Remove all asserted constraints and backtracking points created using `push()`.
6997
6998 >>> x = Int('x')
6999 >>> s = Solver()
7000 >>> s.add(x > 0)
7001 >>> s
7002 [x > 0]
7003 >>> s.reset()
7004 >>> s
7005 []
7006 """
7007 Z3_solver_reset(self.ctx.ref(), self.solver)
7008
void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)
Remove all assertions from the solver.

◆ root()

def root (   self,
  t 
)

Definition at line 7244 of file z3py.py.

7244 def root(self, t):
7245 t = _py2expr(t, self.ctx)
7246 """Retrieve congruence closure root of the term t relative to the current search state
7247 The function primarily works for SimpleSolver. Terms and variables that are
7248 eliminated during pre-processing are not visible to the congruence closure.
7249 """
7250 return _to_expr_ref(Z3_solver_congruence_root(self.ctx.ref(), self.solver, t.ast), self.ctx)
7251
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()

def set (   self,
args,
**  keys 
)
Set a configuration option.
The method `help()` return a string containing all available options.

>>> s = Solver()
>>> # The option MBQI can be set using three different approaches.
>>> s.set(mbqi=True)
>>> s.set('MBQI', True)
>>> s.set(':mbqi', True)

Definition at line 6920 of file z3py.py.

6920 def set(self, *args, **keys):
6921 """Set a configuration option.
6922 The method `help()` return a string containing all available options.
6923
6924 >>> s = Solver()
6925 >>> # The option MBQI can be set using three different approaches.
6926 >>> s.set(mbqi=True)
6927 >>> s.set('MBQI', True)
6928 >>> s.set(':mbqi', True)
6929 """
6930 p = args2params(args, keys, self.ctx)
6931 Z3_solver_set_params(self.ctx.ref(), self.solver, p.params)
6932
void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p)
Set the given solver using the given parameters.

◆ sexpr()

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

7363 def sexpr(self):
7364 """Return a formatted string (in Lisp-like format) with all added constraints.
7365 We say the string is in s-expression format.
7366
7367 >>> x = Int('x')
7368 >>> s = Solver()
7369 >>> s.add(x > 0)
7370 >>> s.add(x < 2)
7371 >>> r = s.sexpr()
7372 """
7373 return Z3_solver_to_string(self.ctx.ref(), self.solver)
7374
Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s)
Convert a solver into a string.

Referenced by Fixedpoint.__repr__(), and Optimize.__repr__().

◆ statistics()

def statistics (   self)
Return statistics for the last `check()`.

>>> s = SimpleSolver()
>>> x = Int('x')
>>> s.add(x > 0)
>>> s.check()
sat
>>> st = s.statistics()
>>> st.get_key_value('final checks')
1
>>> len(st) > 0
True
>>> st[0] != 0
True

Definition at line 7301 of file z3py.py.

7301 def statistics(self):
7302 """Return statistics for the last `check()`.
7303
7304 >>> s = SimpleSolver()
7305 >>> x = Int('x')
7306 >>> s.add(x > 0)
7307 >>> s.check()
7308 sat
7309 >>> st = s.statistics()
7310 >>> st.get_key_value('final checks')
7311 1
7312 >>> len(st) > 0
7313 True
7314 >>> st[0] != 0
7315 True
7316 """
7317 return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx)
7318
Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s)
Return statistics for the given solver.

◆ to_smt2()

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

Definition at line 7379 of file z3py.py.

7379 def to_smt2(self):
7380 """return SMTLIB2 formatted benchmark for solver's assertions"""
7381 es = self.assertions()
7382 sz = len(es)
7383 sz1 = sz
7384 if sz1 > 0:
7385 sz1 -= 1
7386 v = (Ast * sz1)()
7387 for i in range(sz1):
7388 v[i] = es[i].as_ast()
7389 if sz > 0:
7390 e = es[sz1].as_ast()
7391 else:
7392 e = BoolVal(True, self.ctx).as_ast()
7394 self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e,
7395 )
7396
7397
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()

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

Definition at line 7296 of file z3py.py.

7296 def trail(self):
7297 """Return trail of the solver state after a check() call.
7298 """
7299 return AstVector(Z3_solver_get_trail(self.ctx.ref(), self.solver), self.ctx)
7300
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...

Referenced by Solver.trail_levels().

◆ trail_levels()

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

Definition at line 7288 of file z3py.py.

7288 def trail_levels(self):
7289 """Return trail and decision levels of the solver state after a check() call.
7290 """
7291 trail = self.trail()
7292 levels = (ctypes.c_uint * len(trail))()
7293 Z3_solver_get_levels(self.ctx.ref(), self.solver, trail.vector, len(trail), levels)
7294 return trail, levels
7295
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()

def translate (   self,
  target 
)
Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.

>>> c1 = Context()
>>> c2 = Context()
>>> s1 = Solver(ctx=c1)
>>> s2 = s1.translate(c2)

Definition at line 7344 of file z3py.py.

7344 def translate(self, target):
7345 """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
7346
7347 >>> c1 = Context()
7348 >>> c2 = Context()
7349 >>> s1 = Solver(ctx=c1)
7350 >>> s2 = s1.translate(c2)
7351 """
7352 if z3_debug():
7353 _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
7354 solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref())
7355 return Solver(solver, target)
7356
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__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), Solver.__copy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), and Solver.__deepcopy__().

◆ units()

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

Definition at line 7278 of file z3py.py.

7278 def units(self):
7279 """Return an AST vector containing all currently inferred units.
7280 """
7281 return AstVector(Z3_solver_get_units(self.ctx.ref(), self.solver), self.ctx)
7282
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()

def unsat_core (   self)
Return a subset (as an AST vector) of the assumptions provided to the last check().

These are the assumptions Z3 used in the unsatisfiability proof.
Assumptions are available in Z3. They are used to extract unsatisfiable cores.
They may be also used to "retract" assumptions. Note that, assumptions are not really
"soft constraints", but they can be used to implement them.

>>> p1, p2, p3 = Bools('p1 p2 p3')
>>> x, y       = Ints('x y')
>>> s          = Solver()
>>> s.add(Implies(p1, x > 0))
>>> s.add(Implies(p2, y > x))
>>> s.add(Implies(p2, y < 1))
>>> s.add(Implies(p3, y > -3))
>>> s.check(p1, p2, p3)
unsat
>>> core = s.unsat_core()
>>> len(core)
2
>>> p1 in core
True
>>> p2 in core
True
>>> p3 in core
False
>>> # "Retracting" p2
>>> s.check(p1, p3)
sat

Definition at line 7147 of file z3py.py.

7147 def unsat_core(self):
7148 """Return a subset (as an AST vector) of the assumptions provided to the last check().
7149
7150 These are the assumptions Z3 used in the unsatisfiability proof.
7151 Assumptions are available in Z3. They are used to extract unsatisfiable cores.
7152 They may be also used to "retract" assumptions. Note that, assumptions are not really
7153 "soft constraints", but they can be used to implement them.
7154
7155 >>> p1, p2, p3 = Bools('p1 p2 p3')
7156 >>> x, y = Ints('x y')
7157 >>> s = Solver()
7158 >>> s.add(Implies(p1, x > 0))
7159 >>> s.add(Implies(p2, y > x))
7160 >>> s.add(Implies(p2, y < 1))
7161 >>> s.add(Implies(p3, y > -3))
7162 >>> s.check(p1, p2, p3)
7163 unsat
7164 >>> core = s.unsat_core()
7165 >>> len(core)
7166 2
7167 >>> p1 in core
7168 True
7169 >>> p2 in core
7170 True
7171 >>> p3 in core
7172 False
7173 >>> # "Retracting" p2
7174 >>> s.check(p1, p3)
7175 sat
7176 """
7177 return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx)
7178
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

backtrack_level

Definition at line 6906 of file z3py.py.

◆ ctx

ctx

Definition at line 6905 of file z3py.py.

Referenced by ArithRef.__add__(), BitVecRef.__add__(), FPRef.__add__(), BitVecRef.__and__(), FuncDeclRef.__call__(), Probe.__call__(), AstMap.__contains__(), AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), Solver.__copy__(), AstRef.__deepcopy__(), Datatype.__deepcopy__(), ParamsRef.__deepcopy__(), ParamDescrsRef.__deepcopy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), AstMap.__deepcopy__(), FuncEntry.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), Statistics.__deepcopy__(), Solver.__deepcopy__(), Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), Context.__del__(), AstRef.__del__(), ScopedConstructor.__del__(), ScopedConstructorList.__del__(), ParamsRef.__del__(), ParamDescrsRef.__del__(), Goal.__del__(), AstVector.__del__(), AstMap.__del__(), FuncEntry.__del__(), FuncInterp.__del__(), ModelRef.__del__(), Statistics.__del__(), Solver.__del__(), Fixedpoint.__del__(), Optimize.__del__(), ApplyResult.__del__(), Tactic.__del__(), Probe.__del__(), ParserContext.__del__(), ArithRef.__div__(), BitVecRef.__div__(), FPRef.__div__(), ExprRef.__eq__(), Probe.__eq__(), ArithRef.__ge__(), BitVecRef.__ge__(), Probe.__ge__(), FPRef.__ge__(), SeqRef.__ge__(), AstVector.__getitem__(), SeqRef.__getitem__(), ModelRef.__getitem__(), Statistics.__getitem__(), ApplyResult.__getitem__(), AstMap.__getitem__(), ArithRef.__gt__(), BitVecRef.__gt__(), Probe.__gt__(), FPRef.__gt__(), SeqRef.__gt__(), BitVecRef.__invert__(), ArithRef.__le__(), BitVecRef.__le__(), Probe.__le__(), FPRef.__le__(), SeqRef.__le__(), CharRef.__le__(), AstVector.__len__(), AstMap.__len__(), ModelRef.__len__(), Statistics.__len__(), ApplyResult.__len__(), BitVecRef.__lshift__(), ArithRef.__lt__(), BitVecRef.__lt__(), Probe.__lt__(), FPRef.__lt__(), SeqRef.__lt__(), ArithRef.__mod__(), BitVecRef.__mod__(), BoolRef.__mul__(), ArithRef.__mul__(), BitVecRef.__mul__(), FPRef.__mul__(), ExprRef.__ne__(), Probe.__ne__(), ArithRef.__neg__(), BitVecRef.__neg__(), BitVecRef.__or__(), ArithRef.__pow__(), ArithRef.__radd__(), BitVecRef.__radd__(), FPRef.__radd__(), BitVecRef.__rand__(), ArithRef.__rdiv__(), BitVecRef.__rdiv__(), FPRef.__rdiv__(), ParamsRef.__repr__(), ParamDescrsRef.__repr__(), AstMap.__repr__(), Statistics.__repr__(), BitVecRef.__rlshift__(), ArithRef.__rmod__(), BitVecRef.__rmod__(), ArithRef.__rmul__(), BitVecRef.__rmul__(), FPRef.__rmul__(), BitVecRef.__ror__(), ArithRef.__rpow__(), BitVecRef.__rrshift__(), BitVecRef.__rshift__(), ArithRef.__rsub__(), BitVecRef.__rsub__(), FPRef.__rsub__(), BitVecRef.__rxor__(), AstVector.__setitem__(), AstMap.__setitem__(), ArithRef.__sub__(), BitVecRef.__sub__(), FPRef.__sub__(), BitVecRef.__xor__(), DatatypeSortRef.accessor(), Fixedpoint.add_cover(), ParserContext.add_decl(), Fixedpoint.add_rule(), Optimize.add_soft(), ParserContext.add_sort(), Tactic.apply(), AlgebraicNumRef.approx(), ExprRef.arg(), FuncEntry.arg_value(), FuncInterp.arity(), Goal.as_expr(), ApplyResult.as_expr(), FPNumRef.as_string(), Solver.assert_and_track(), Optimize.assert_and_track(), Goal.assert_exprs(), Solver.assert_exprs(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Solver.assertions(), Optimize.assertions(), SeqRef.at(), SeqSortRef.basis(), ReSortRef.basis(), QuantifierRef.body(), BoolSortRef.cast(), Solver.check(), Optimize.check(), UserPropagateBase.conflict(), Solver.consequences(), DatatypeSortRef.constructor(), Goal.convert_model(), AstRef.ctx_ref(), UserPropagateBase.ctx_ref(), ExprRef.decl(), ModelRef.decls(), ArrayRef.default(), RatNumRef.denominator(), Goal.depth(), Goal.dimacs(), Solver.dimacs(), ArraySortRef.domain(), FuncDeclRef.domain(), ArraySortRef.domain_n(), FuncInterp.else_value(), FuncInterp.entry(), AstMap.erase(), ModelRef.eval(), FPNumRef.exponent(), FPNumRef.exponent_as_bv(), FPNumRef.exponent_as_long(), Solver.from_file(), Optimize.from_file(), Solver.from_string(), Optimize.from_string(), ParserContext.from_string(), Goal.get(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), ParamDescrsRef.get_documentation(), Fixedpoint.get_ground_sat_answer(), ModelRef.get_interp(), Statistics.get_key_value(), ParamDescrsRef.get_kind(), ParamDescrsRef.get_name(), Fixedpoint.get_num_levels(), Fixedpoint.get_rule_names_along_trace(), Fixedpoint.get_rules(), Fixedpoint.get_rules_along_trace(), ModelRef.get_sort(), ModelRef.get_universe(), Solver.help(), Fixedpoint.help(), Optimize.help(), Tactic.help(), Solver.import_model_converter(), Goal.inconsistent(), CharRef.is_digit(), FPNumRef.isInf(), FPNumRef.isNaN(), FPNumRef.isNegative(), FPNumRef.isNormal(), FPNumRef.isPositive(), FPNumRef.isSubnormal(), FPNumRef.isZero(), AstMap.keys(), Statistics.keys(), SortRef.kind(), Optimize.maximize(), Optimize.minimize(), Solver.model(), Optimize.model(), SortRef.name(), FuncDeclRef.name(), Solver.next(), QuantifierRef.no_pattern(), Solver.non_units(), FuncEntry.num_args(), FuncInterp.num_entries(), Solver.num_scopes(), ModelRef.num_sorts(), RatNumRef.numerator(), Optimize.objectives(), Solver.param_descrs(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), FuncDeclRef.params(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), QuantifierRef.pattern(), AlgebraicNumRef.poly(), Optimize.pop(), Solver.pop(), Goal.prec(), Solver.proof(), Solver.push(), Optimize.push(), AstVector.push(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), FuncDeclRef.range(), ArraySortRef.range(), Solver.reason_unknown(), Fixedpoint.reason_unknown(), Optimize.reason_unknown(), DatatypeSortRef.recognizer(), Context.ref(), Fixedpoint.register_relation(), AstMap.reset(), Solver.reset(), AstVector.resize(), Solver.root(), Solver.set(), Fixedpoint.set(), Optimize.set(), ParamsRef.set(), Optimize.set_on_model(), Fixedpoint.set_predicate_representation(), Goal.sexpr(), AstVector.sexpr(), ModelRef.sexpr(), Solver.sexpr(), Fixedpoint.sexpr(), Optimize.sexpr(), ApplyResult.sexpr(), FPNumRef.sign(), FPNumRef.sign_as_bv(), FPNumRef.significand(), FPNumRef.significand_as_bv(), FPNumRef.significand_as_long(), ParamDescrsRef.size(), Goal.size(), Tactic.solver(), ExprRef.sort(), BoolRef.sort(), QuantifierRef.sort(), ArithRef.sort(), BitVecRef.sort(), ArrayRef.sort(), DatatypeRef.sort(), FiniteDomainRef.sort(), FPRef.sort(), SeqRef.sort(), Solver.statistics(), Fixedpoint.statistics(), Optimize.statistics(), CharRef.to_bv(), CharRef.to_int(), Solver.to_smt2(), Fixedpoint.to_string(), Solver.trail(), Solver.trail_levels(), AstVector.translate(), FuncInterp.translate(), AstRef.translate(), Goal.translate(), ModelRef.translate(), Solver.translate(), Solver.units(), Solver.unsat_core(), Optimize.unsat_core(), Fixedpoint.update_rule(), ParamsRef.validate(), FuncEntry.value(), QuantifierRef.var_name(), and QuantifierRef.var_sort().

◆ cube_vs

cube_vs

Definition at line 7223 of file z3py.py.

Referenced by Solver.cube_vars().

◆ solver

solver