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 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
 

Detailed Description

Solver API provides methods for implementing the main SMT 2.0 commands:
push, pop, check, get-model, etc.

Definition at line 6888 of file z3py.py.

Constructor & Destructor Documentation

◆ __init__()

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

Definition at line 6894 of file z3py.py.

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

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

7332 def __copy__(self):
7333 return self.translate(self.ctx)
7334

◆ __deepcopy__()

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 7335 of file z3py.py.

7335 def __deepcopy__(self, memo={}):
7336 return self.translate(self.ctx)
7337

◆ __iadd__()

def __iadd__ (   self,
  fml 
)

Definition at line 7030 of file z3py.py.

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

◆ __repr__()

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

Definition at line 7315 of file z3py.py.

7315 def __repr__(self):
7316 """Return a formatted string with all added constraints."""
7317 return obj_to_string(self)
7318

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

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

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

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

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

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

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

7239 def assertions(self):
7240 """Return an AST vector containing all added constraints.
7241
7242 >>> s = Solver()
7243 >>> s.assertions()
7244 []
7245 >>> a = Int('a')
7246 >>> s.add(a > 0)
7247 >>> s.add(a < 10)
7248 >>> s.assertions()
7249 [a > 0, a < 10]
7250 """
7251 return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
7252
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 7086 of file z3py.py.

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

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

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

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

◆ dimacs()

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

Definition at line 7350 of file z3py.py.

7350 def dimacs(self, include_names=True):
7351 """Return a textual representation of the solver in DIMACS format."""
7352 return Z3_solver_to_dimacs_string(self.ctx.ref(), self.solver, include_names)
7353
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 7199 of file z3py.py.

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

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

7307 def help(self):
7308 """Display a string describing all available options."""
7309 print(Z3_solver_get_help(self.ctx.ref(), self.solver))
7310
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 7134 of file z3py.py.

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

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

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

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

◆ non_units()

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

Definition at line 7258 of file z3py.py.

7258 def non_units(self):
7259 """Return an AST vector containing all atomic formulas in solver state that are not units.
7260 """
7261 return AstVector(Z3_solver_get_non_units(self.ctx.ref(), self.solver), self.ctx)
7262
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 6968 of file z3py.py.

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

7311 def param_descrs(self):
7312 """Return the parameter description set."""
7313 return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx)
7314
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 6946 of file z3py.py.

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

7235 def proof(self):
7236 """Return a proof for the last `check()`. Proof construction must be enabled."""
7237 return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
7238
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 6924 of file z3py.py.

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

7294 def reason_unknown(self):
7295 """Return a string describing why the last `check()` returned `unknown`.
7296
7297 >>> x = Int('x')
7298 >>> s = SimpleSolver()
7299 >>> s.add(2**x == 4)
7300 >>> s.check()
7301 unknown
7302 >>> s.reason_unknown()
7303 '(incomplete (theory arithmetic))'
7304 """
7305 return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver)
7306
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 6986 of file z3py.py.

6986 def reset(self):
6987 """Remove all asserted constraints and backtracking points created using `push()`.
6988
6989 >>> x = Int('x')
6990 >>> s = Solver()
6991 >>> s.add(x > 0)
6992 >>> s
6993 [x > 0]
6994 >>> s.reset()
6995 >>> s
6996 []
6997 """
6998 Z3_solver_reset(self.ctx.ref(), self.solver)
6999
void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)
Remove all assertions from the solver.

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

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

7338 def sexpr(self):
7339 """Return a formatted string (in Lisp-like format) with all added constraints.
7340 We say the string is in s-expression format.
7341
7342 >>> x = Int('x')
7343 >>> s = Solver()
7344 >>> s.add(x > 0)
7345 >>> s.add(x < 2)
7346 >>> r = s.sexpr()
7347 """
7348 return Z3_solver_to_string(self.ctx.ref(), self.solver)
7349
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 7276 of file z3py.py.

7276 def statistics(self):
7277 """Return statistics for the last `check()`.
7278
7279 >>> s = SimpleSolver()
7280 >>> x = Int('x')
7281 >>> s.add(x > 0)
7282 >>> s.check()
7283 sat
7284 >>> st = s.statistics()
7285 >>> st.get_key_value('final checks')
7286 1
7287 >>> len(st) > 0
7288 True
7289 >>> st[0] != 0
7290 True
7291 """
7292 return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx)
7293
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 7354 of file z3py.py.

7354 def to_smt2(self):
7355 """return SMTLIB2 formatted benchmark for solver's assertions"""
7356 es = self.assertions()
7357 sz = len(es)
7358 sz1 = sz
7359 if sz1 > 0:
7360 sz1 -= 1
7361 v = (Ast * sz1)()
7362 for i in range(sz1):
7363 v[i] = es[i].as_ast()
7364 if sz > 0:
7365 e = es[sz1].as_ast()
7366 else:
7367 e = BoolVal(True, self.ctx).as_ast()
7369 self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e,
7370 )
7371
7372
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 7271 of file z3py.py.

7271 def trail(self):
7272 """Return trail of the solver state after a check() call.
7273 """
7274 return AstVector(Z3_solver_get_trail(self.ctx.ref(), self.solver), self.ctx)
7275
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 7263 of file z3py.py.

7263 def trail_levels(self):
7264 """Return trail and decision levels of the solver state after a check() call.
7265 """
7266 trail = self.trail()
7267 levels = (ctypes.c_uint * len(trail))()
7268 Z3_solver_get_levels(self.ctx.ref(), self.solver, trail.vector, len(trail), levels)
7269 return trail, levels
7270
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 7319 of file z3py.py.

7319 def translate(self, target):
7320 """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
7321
7322 >>> c1 = Context()
7323 >>> c2 = Context()
7324 >>> s1 = Solver(ctx=c1)
7325 >>> s2 = s1.translate(c2)
7326 """
7327 if z3_debug():
7328 _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
7329 solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref())
7330 return Solver(solver, target)
7331
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 7253 of file z3py.py.

7253 def units(self):
7254 """Return an AST vector containing all currently inferred units.
7255 """
7256 return AstVector(Z3_solver_get_units(self.ctx.ref(), self.solver), self.ctx)
7257
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 7138 of file z3py.py.

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

◆ ctx

ctx

Definition at line 6896 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__(), 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(), 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.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 7214 of file z3py.py.

Referenced by Solver.cube_vars().

◆ solver

solver