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

Constructor & Destructor Documentation

◆ __init__()

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

Definition at line 6895 of file z3py.py.

6895 def __init__(self, solver=None, ctx=None, logFile=None):
6896 assert solver is None or ctx is not None
6897 self.ctx = _get_ctx(ctx)
6898 self.backtrack_level = 4000000000
6899 self.solver = None
6900 if solver is None:
6901 self.solver = Z3_mk_solver(self.ctx.ref())
6902 else:
6903 self.solver = solver
6904 Z3_solver_inc_ref(self.ctx.ref(), self.solver)
6905 if logFile is not None:
6906 self.set("smtlib2_log", logFile)
6907
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 6908 of file z3py.py.

6908 def __del__(self):
6909 if self.solver is not None and self.ctx.ref() is not None and Z3_solver_dec_ref is not None:
6910 Z3_solver_dec_ref(self.ctx.ref(), self.solver)
6911
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 7349 of file z3py.py.

7349 def __copy__(self):
7350 return self.translate(self.ctx)
7351

◆ __deepcopy__()

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 7352 of file z3py.py.

7352 def __deepcopy__(self, memo={}):
7353 return self.translate(self.ctx)
7354

◆ __iadd__()

def __iadd__ (   self,
  fml 
)

Definition at line 7031 of file z3py.py.

7031 def __iadd__(self, fml):
7032 self.add(fml)
7033 return self
7034

◆ __repr__()

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

Definition at line 7332 of file z3py.py.

7332 def __repr__(self):
7333 """Return a formatted string with all added constraints."""
7334 return obj_to_string(self)
7335

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

7020 def add(self, *args):
7021 """Assert constraints into the solver.
7022
7023 >>> x = Int('x')
7024 >>> s = Solver()
7025 >>> s.add(x > 0, x < 2)
7026 >>> s
7027 [x > 0, x < 2]
7028 """
7029 self.assert_exprs(*args)
7030

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

7035 def append(self, *args):
7036 """Assert constraints into the solver.
7037
7038 >>> x = Int('x')
7039 >>> s = Solver()
7040 >>> s.append(x > 0, x < 2)
7041 >>> s
7042 [x > 0, x < 2]
7043 """
7044 self.assert_exprs(*args)
7045

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

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

7001 def assert_exprs(self, *args):
7002 """Assert constraints into the solver.
7003
7004 >>> x = Int('x')
7005 >>> s = Solver()
7006 >>> s.assert_exprs(x > 0, x < 2)
7007 >>> s
7008 [x > 0, x < 2]
7009 """
7010 args = _get_args(args)
7011 s = BoolSort(self.ctx)
7012 for arg in args:
7013 if isinstance(arg, Goal) or isinstance(arg, AstVector):
7014 for f in arg:
7015 Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast())
7016 else:
7017 arg = s.cast(arg)
7018 Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast())
7019
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 7256 of file z3py.py.

7256 def assertions(self):
7257 """Return an AST vector containing all added constraints.
7258
7259 >>> s = Solver()
7260 >>> s.assertions()
7261 []
7262 >>> a = Int('a')
7263 >>> s.add(a > 0)
7264 >>> s.add(a < 10)
7265 >>> s.assertions()
7266 [a > 0, a < 10]
7267 """
7268 return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
7269
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 7087 of file z3py.py.

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

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

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

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

◆ dimacs()

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

Definition at line 7367 of file z3py.py.

7367 def dimacs(self, include_names=True):
7368 """Return a textual representation of the solver in DIMACS format."""
7369 return Z3_solver_to_dimacs_string(self.ctx.ref(), self.solver, include_names)
7370
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 7200 of file z3py.py.

7200 def from_file(self, filename):
7201 """Parse assertions from a file"""
7202 Z3_solver_from_file(self.ctx.ref(), self.solver, filename)
7203
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 7204 of file z3py.py.

7204 def from_string(self, s):
7205 """Parse assertions from a string"""
7206 Z3_solver_from_string(self.ctx.ref(), self.solver, s)
7207
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 7324 of file z3py.py.

7324 def help(self):
7325 """Display a string describing all available options."""
7326 print(Z3_solver_get_help(self.ctx.ref(), self.solver))
7327
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 7135 of file z3py.py.

7135 def import_model_converter(self, other):
7136 """Import model converter from other into the current solver"""
7137 Z3_solver_import_model_converter(self.ctx.ref(), other.solver, self.solver)
7138
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 7046 of file z3py.py.

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

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

7116 def model(self):
7117 """Return a model for the last `check()`.
7118
7119 This function raises an exception if
7120 a model is not available (e.g., last `check()` returned unsat).
7121
7122 >>> s = Solver()
7123 >>> a = Int('a')
7124 >>> s.add(a + 2 == 0)
7125 >>> s.check()
7126 sat
7127 >>> s.model()
7128 [a = -2]
7129 """
7130 try:
7131 return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx)
7132 except Z3Exception:
7133 raise Z3Exception("model is not available")
7134
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 7244 of file z3py.py.

7244 def next(self, t):
7245 t = _py2expr(t, self.ctx)
7246 """Retrieve congruence closure sibling 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_next(self.ctx.ref(), self.solver, t.ast), self.ctx)
7251
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 7275 of file z3py.py.

7275 def non_units(self):
7276 """Return an AST vector containing all atomic formulas in solver state that are not units.
7277 """
7278 return AstVector(Z3_solver_get_non_units(self.ctx.ref(), self.solver), self.ctx)
7279
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 6969 of file z3py.py.

6969 def num_scopes(self):
6970 """Return the current number of backtracking points.
6971
6972 >>> s = Solver()
6973 >>> s.num_scopes()
6974 0
6975 >>> s.push()
6976 >>> s.num_scopes()
6977 1
6978 >>> s.push()
6979 >>> s.num_scopes()
6980 2
6981 >>> s.pop()
6982 >>> s.num_scopes()
6983 1
6984 """
6985 return Z3_solver_get_num_scopes(self.ctx.ref(), self.solver)
6986
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 7328 of file z3py.py.

7328 def param_descrs(self):
7329 """Return the parameter description set."""
7330 return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx)
7331
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 6947 of file z3py.py.

6947 def pop(self, num=1):
6948 """Backtrack \\c num backtracking points.
6949
6950 >>> x = Int('x')
6951 >>> s = Solver()
6952 >>> s.add(x > 0)
6953 >>> s
6954 [x > 0]
6955 >>> s.push()
6956 >>> s.add(x < 1)
6957 >>> s
6958 [x > 0, x < 1]
6959 >>> s.check()
6960 unsat
6961 >>> s.pop()
6962 >>> s.check()
6963 sat
6964 >>> s
6965 [x > 0]
6966 """
6967 Z3_solver_pop(self.ctx.ref(), self.solver, num)
6968
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 7252 of file z3py.py.

7252 def proof(self):
7253 """Return a proof for the last `check()`. Proof construction must be enabled."""
7254 return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
7255
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 6925 of file z3py.py.

6925 def push(self):
6926 """Create a backtracking point.
6927
6928 >>> x = Int('x')
6929 >>> s = Solver()
6930 >>> s.add(x > 0)
6931 >>> s
6932 [x > 0]
6933 >>> s.push()
6934 >>> s.add(x < 1)
6935 >>> s
6936 [x > 0, x < 1]
6937 >>> s.check()
6938 unsat
6939 >>> s.pop()
6940 >>> s.check()
6941 sat
6942 >>> s
6943 [x > 0]
6944 """
6945 Z3_solver_push(self.ctx.ref(), self.solver)
6946
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 7311 of file z3py.py.

7311 def reason_unknown(self):
7312 """Return a string describing why the last `check()` returned `unknown`.
7313
7314 >>> x = Int('x')
7315 >>> s = SimpleSolver()
7316 >>> s.add(2**x == 4)
7317 >>> s.check()
7318 unknown
7319 >>> s.reason_unknown()
7320 '(incomplete (theory arithmetic))'
7321 """
7322 return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver)
7323
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 6987 of file z3py.py.

6987 def reset(self):
6988 """Remove all asserted constraints and backtracking points created using `push()`.
6989
6990 >>> x = Int('x')
6991 >>> s = Solver()
6992 >>> s.add(x > 0)
6993 >>> s
6994 [x > 0]
6995 >>> s.reset()
6996 >>> s
6997 []
6998 """
6999 Z3_solver_reset(self.ctx.ref(), self.solver)
7000
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 7236 of file z3py.py.

7236 def root(self, t):
7237 t = _py2expr(t, self.ctx)
7238 """Retrieve congruence closure root of the term t relative to the current search state
7239 The function primarily works for SimpleSolver. Terms and variables that are
7240 eliminated during pre-processing are not visible to the congruence closure.
7241 """
7242 return _to_expr_ref(Z3_solver_congruence_root(self.ctx.ref(), self.solver, t.ast), self.ctx)
7243
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 6912 of file z3py.py.

6912 def set(self, *args, **keys):
6913 """Set a configuration option.
6914 The method `help()` return a string containing all available options.
6915
6916 >>> s = Solver()
6917 >>> # The option MBQI can be set using three different approaches.
6918 >>> s.set(mbqi=True)
6919 >>> s.set('MBQI', True)
6920 >>> s.set(':mbqi', True)
6921 """
6922 p = args2params(args, keys, self.ctx)
6923 Z3_solver_set_params(self.ctx.ref(), self.solver, p.params)
6924
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 7355 of file z3py.py.

7355 def sexpr(self):
7356 """Return a formatted string (in Lisp-like format) with all added constraints.
7357 We say the string is in s-expression format.
7358
7359 >>> x = Int('x')
7360 >>> s = Solver()
7361 >>> s.add(x > 0)
7362 >>> s.add(x < 2)
7363 >>> r = s.sexpr()
7364 """
7365 return Z3_solver_to_string(self.ctx.ref(), self.solver)
7366
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 7293 of file z3py.py.

7293 def statistics(self):
7294 """Return statistics for the last `check()`.
7295
7296 >>> s = SimpleSolver()
7297 >>> x = Int('x')
7298 >>> s.add(x > 0)
7299 >>> s.check()
7300 sat
7301 >>> st = s.statistics()
7302 >>> st.get_key_value('final checks')
7303 1
7304 >>> len(st) > 0
7305 True
7306 >>> st[0] != 0
7307 True
7308 """
7309 return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx)
7310
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 7371 of file z3py.py.

7371 def to_smt2(self):
7372 """return SMTLIB2 formatted benchmark for solver's assertions"""
7373 es = self.assertions()
7374 sz = len(es)
7375 sz1 = sz
7376 if sz1 > 0:
7377 sz1 -= 1
7378 v = (Ast * sz1)()
7379 for i in range(sz1):
7380 v[i] = es[i].as_ast()
7381 if sz > 0:
7382 e = es[sz1].as_ast()
7383 else:
7384 e = BoolVal(True, self.ctx).as_ast()
7386 self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e,
7387 )
7388
7389
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 7288 of file z3py.py.

7288 def trail(self):
7289 """Return trail of the solver state after a check() call.
7290 """
7291 return AstVector(Z3_solver_get_trail(self.ctx.ref(), self.solver), self.ctx)
7292
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 7280 of file z3py.py.

7280 def trail_levels(self):
7281 """Return trail and decision levels of the solver state after a check() call.
7282 """
7283 trail = self.trail()
7284 levels = (ctypes.c_uint * len(trail))()
7285 Z3_solver_get_levels(self.ctx.ref(), self.solver, trail.vector, len(trail), levels)
7286 return trail, levels
7287
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 7336 of file z3py.py.

7336 def translate(self, target):
7337 """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
7338
7339 >>> c1 = Context()
7340 >>> c2 = Context()
7341 >>> s1 = Solver(ctx=c1)
7342 >>> s2 = s1.translate(c2)
7343 """
7344 if z3_debug():
7345 _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
7346 solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref())
7347 return Solver(solver, target)
7348
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 7270 of file z3py.py.

7270 def units(self):
7271 """Return an AST vector containing all currently inferred units.
7272 """
7273 return AstVector(Z3_solver_get_units(self.ctx.ref(), self.solver), self.ctx)
7274
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 7139 of file z3py.py.

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

◆ ctx

ctx

Definition at line 6897 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__(), Simplifier.__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__(), Simplifier.__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(), Simplifier.add(), 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(), Simplifier.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(), Simplifier.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(), Simplifier.using_params(), ParamsRef.validate(), FuncEntry.value(), QuantifierRef.var_name(), and QuantifierRef.var_sort().

◆ cube_vs

cube_vs

Definition at line 7215 of file z3py.py.

Referenced by Solver.cube_vars().

◆ solver

solver