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

Constructor & Destructor Documentation

◆ __init__()

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

Definition at line 6804 of file z3py.py.

6804  def __init__(self, solver=None, ctx=None, logFile=None):
6805  assert solver is None or ctx is not None
6806  self.ctx = _get_ctx(ctx)
6807  self.backtrack_level = 4000000000
6808  self.solver = None
6809  if solver is None:
6810  self.solver = Z3_mk_solver(self.ctx.ref())
6811  else:
6812  self.solver = solver
6813  Z3_solver_inc_ref(self.ctx.ref(), self.solver)
6814  if logFile is not None:
6815  self.set("smtlib2_log", logFile)
6816 
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 6817 of file z3py.py.

6817  def __del__(self):
6818  if self.solver is not None and self.ctx.ref() is not None:
6819  Z3_solver_dec_ref(self.ctx.ref(), self.solver)
6820 
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 7242 of file z3py.py.

7242  def __copy__(self):
7243  return self.translate(self.ctx)
7244 

◆ __deepcopy__()

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 7245 of file z3py.py.

7245  def __deepcopy__(self, memo={}):
7246  return self.translate(self.ctx)
7247 

◆ __iadd__()

def __iadd__ (   self,
  fml 
)

Definition at line 6940 of file z3py.py.

6940  def __iadd__(self, fml):
6941  self.add(fml)
6942  return self
6943 

◆ __repr__()

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

Definition at line 7225 of file z3py.py.

7225  def __repr__(self):
7226  """Return a formatted string with all added constraints."""
7227  return obj_to_string(self)
7228 

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

6929  def add(self, *args):
6930  """Assert constraints into the solver.
6931 
6932  >>> x = Int('x')
6933  >>> s = Solver()
6934  >>> s.add(x > 0, x < 2)
6935  >>> s
6936  [x > 0, x < 2]
6937  """
6938  self.assert_exprs(*args)
6939 

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

6944  def append(self, *args):
6945  """Assert constraints into the solver.
6946 
6947  >>> x = Int('x')
6948  >>> s = Solver()
6949  >>> s.append(x > 0, x < 2)
6950  >>> s
6951  [x > 0, x < 2]
6952  """
6953  self.assert_exprs(*args)
6954 

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

6966  def assert_and_track(self, a, p):
6967  """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
6968 
6969  If `p` is a string, it will be automatically converted into a Boolean constant.
6970 
6971  >>> x = Int('x')
6972  >>> p3 = Bool('p3')
6973  >>> s = Solver()
6974  >>> s.set(unsat_core=True)
6975  >>> s.assert_and_track(x > 0, 'p1')
6976  >>> s.assert_and_track(x != 1, 'p2')
6977  >>> s.assert_and_track(x < 0, p3)
6978  >>> print(s.check())
6979  unsat
6980  >>> c = s.unsat_core()
6981  >>> len(c)
6982  2
6983  >>> Bool('p1') in c
6984  True
6985  >>> Bool('p2') in c
6986  False
6987  >>> p3 in c
6988  True
6989  """
6990  if isinstance(p, str):
6991  p = Bool(p, self.ctx)
6992  _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
6993  _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
6994  Z3_solver_assert_and_track(self.ctx.ref(), self.solver, a.as_ast(), p.as_ast())
6995 
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.
def is_const(a)
Definition: z3py.py:1261
def Bool(name, ctx=None)
Definition: z3py.py:1694

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

6910  def assert_exprs(self, *args):
6911  """Assert constraints into the solver.
6912 
6913  >>> x = Int('x')
6914  >>> s = Solver()
6915  >>> s.assert_exprs(x > 0, x < 2)
6916  >>> s
6917  [x > 0, x < 2]
6918  """
6919  args = _get_args(args)
6920  s = BoolSort(self.ctx)
6921  for arg in args:
6922  if isinstance(arg, Goal) or isinstance(arg, AstVector):
6923  for f in arg:
6924  Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast())
6925  else:
6926  arg = s.cast(arg)
6927  Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast())
6928 
void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a)
Assert a constraint into the solver.
def BoolSort(ctx=None)
Definition: z3py.py:1657

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

7149  def assertions(self):
7150  """Return an AST vector containing all added constraints.
7151 
7152  >>> s = Solver()
7153  >>> s.assertions()
7154  []
7155  >>> a = Int('a')
7156  >>> s.add(a > 0)
7157  >>> s.add(a < 10)
7158  >>> s.assertions()
7159  [a > 0, a < 10]
7160  """
7161  return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
7162 
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 6996 of file z3py.py.

6996  def check(self, *assumptions):
6997  """Check whether the assertions in the given solver plus the optional assumptions are consistent or not.
6998 
6999  >>> x = Int('x')
7000  >>> s = Solver()
7001  >>> s.check()
7002  sat
7003  >>> s.add(x > 0, x < 2)
7004  >>> s.check()
7005  sat
7006  >>> s.model().eval(x)
7007  1
7008  >>> s.add(x < 1)
7009  >>> s.check()
7010  unsat
7011  >>> s.reset()
7012  >>> s.add(2**x == 4)
7013  >>> s.check()
7014  unknown
7015  """
7016  s = BoolSort(self.ctx)
7017  assumptions = _get_args(assumptions)
7018  num = len(assumptions)
7019  _assumptions = (Ast * num)()
7020  for i in range(num):
7021  _assumptions[i] = s.cast(assumptions[i]).as_ast()
7022  r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions)
7023  return CheckSatResult(r)
7024 
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.
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3810

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

7080  def consequences(self, assumptions, variables):
7081  """Determine fixed values for the variables based on the solver state and assumptions.
7082  >>> s = Solver()
7083  >>> a, b, c, d = Bools('a b c d')
7084  >>> s.add(Implies(a,b), Implies(b, c))
7085  >>> s.consequences([a],[b,c,d])
7086  (sat, [Implies(a, b), Implies(a, c)])
7087  >>> s.consequences([Not(c),d],[a,b,c,d])
7088  (sat, [Implies(d, d), Implies(Not(c), Not(c)), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))])
7089  """
7090  if isinstance(assumptions, list):
7091  _asms = AstVector(None, self.ctx)
7092  for a in assumptions:
7093  _asms.push(a)
7094  assumptions = _asms
7095  if isinstance(variables, list):
7096  _vars = AstVector(None, self.ctx)
7097  for a in variables:
7098  _vars.push(a)
7099  variables = _vars
7100  _z3_assert(isinstance(assumptions, AstVector), "ast vector expected")
7101  _z3_assert(isinstance(variables, AstVector), "ast vector expected")
7102  consequences = AstVector(None, self.ctx)
7103  r = Z3_solver_get_consequences(self.ctx.ref(), self.solver, assumptions.vector,
7104  variables.vector, consequences.vector)
7105  sz = len(consequences)
7106  consequences = [consequences[i] for i in range(sz)]
7107  return CheckSatResult(r), consequences
7108 
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 7117 of file z3py.py.

7117  def cube(self, vars=None):
7118  """Get set of cubes
7119  The method takes an optional set of variables that restrict which
7120  variables may be used as a starting point for cubing.
7121  If vars is not None, then the first case split is based on a variable in
7122  this set.
7123  """
7124  self.cube_vs = AstVector(None, self.ctx)
7125  if vars is not None:
7126  for v in vars:
7127  self.cube_vs.push(v)
7128  while True:
7129  lvl = self.backtrack_level
7130  self.backtrack_level = 4000000000
7131  r = AstVector(Z3_solver_cube(self.ctx.ref(), self.solver, self.cube_vs.vector, lvl), self.ctx)
7132  if (len(r) == 1 and is_false(r[0])):
7133  return
7134  yield r
7135  if (len(r) == 0):
7136  return
7137 
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...
def is_false(a)
Definition: z3py.py:1573

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

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

◆ dimacs()

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

Definition at line 7260 of file z3py.py.

7260  def dimacs(self, include_names=True):
7261  """Return a textual representation of the solver in DIMACS format."""
7262  return Z3_solver_to_dimacs_string(self.ctx.ref(), self.solver, include_names)
7263 
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 7109 of file z3py.py.

7109  def from_file(self, filename):
7110  """Parse assertions from a file"""
7111  Z3_solver_from_file(self.ctx.ref(), self.solver, filename)
7112 
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 7113 of file z3py.py.

7113  def from_string(self, s):
7114  """Parse assertions from a string"""
7115  Z3_solver_from_string(self.ctx.ref(), self.solver, s)
7116 
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 7217 of file z3py.py.

7217  def help(self):
7218  """Display a string describing all available options."""
7219  print(Z3_solver_get_help(self.ctx.ref(), self.solver))
7220 
Z3_string Z3_API Z3_solver_get_help(Z3_context c, Z3_solver s)
Return a string describing all solver available parameters.

◆ import_model_converter()

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

Definition at line 7044 of file z3py.py.

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

6955  def insert(self, *args):
6956  """Assert constraints into the solver.
6957 
6958  >>> x = Int('x')
6959  >>> s = Solver()
6960  >>> s.insert(x > 0, x < 2)
6961  >>> s
6962  [x > 0, x < 2]
6963  """
6964  self.assert_exprs(*args)
6965 

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

7025  def model(self):
7026  """Return a model for the last `check()`.
7027 
7028  This function raises an exception if
7029  a model is not available (e.g., last `check()` returned unsat).
7030 
7031  >>> s = Solver()
7032  >>> a = Int('a')
7033  >>> s.add(a + 2 == 0)
7034  >>> s.check()
7035  sat
7036  >>> s.model()
7037  [a = -2]
7038  """
7039  try:
7040  return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx)
7041  except Z3Exception:
7042  raise Z3Exception("model is not available")
7043 
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 7168 of file z3py.py.

7168  def non_units(self):
7169  """Return an AST vector containing all atomic formulas in solver state that are not units.
7170  """
7171  return AstVector(Z3_solver_get_non_units(self.ctx.ref(), self.solver), self.ctx)
7172 
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 6878 of file z3py.py.

6878  def num_scopes(self):
6879  """Return the current number of backtracking points.
6880 
6881  >>> s = Solver()
6882  >>> s.num_scopes()
6883  0
6884  >>> s.push()
6885  >>> s.num_scopes()
6886  1
6887  >>> s.push()
6888  >>> s.num_scopes()
6889  2
6890  >>> s.pop()
6891  >>> s.num_scopes()
6892  1
6893  """
6894  return Z3_solver_get_num_scopes(self.ctx.ref(), self.solver)
6895 
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 7221 of file z3py.py.

7221  def param_descrs(self):
7222  """Return the parameter description set."""
7223  return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx)
7224 
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 6856 of file z3py.py.

6856  def pop(self, num=1):
6857  """Backtrack \\c num backtracking points.
6858 
6859  >>> x = Int('x')
6860  >>> s = Solver()
6861  >>> s.add(x > 0)
6862  >>> s
6863  [x > 0]
6864  >>> s.push()
6865  >>> s.add(x < 1)
6866  >>> s
6867  [x > 0, x < 1]
6868  >>> s.check()
6869  unsat
6870  >>> s.pop()
6871  >>> s.check()
6872  sat
6873  >>> s
6874  [x > 0]
6875  """
6876  Z3_solver_pop(self.ctx.ref(), self.solver, num)
6877 
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 7145 of file z3py.py.

7145  def proof(self):
7146  """Return a proof for the last `check()`. Proof construction must be enabled."""
7147  return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
7148 
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 6834 of file z3py.py.

6834  def push(self):
6835  """Create a backtracking point.
6836 
6837  >>> x = Int('x')
6838  >>> s = Solver()
6839  >>> s.add(x > 0)
6840  >>> s
6841  [x > 0]
6842  >>> s.push()
6843  >>> s.add(x < 1)
6844  >>> s
6845  [x > 0, x < 1]
6846  >>> s.check()
6847  unsat
6848  >>> s.pop()
6849  >>> s.check()
6850  sat
6851  >>> s
6852  [x > 0]
6853  """
6854  Z3_solver_push(self.ctx.ref(), self.solver)
6855 
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 7204 of file z3py.py.

7204  def reason_unknown(self):
7205  """Return a string describing why the last `check()` returned `unknown`.
7206 
7207  >>> x = Int('x')
7208  >>> s = SimpleSolver()
7209  >>> s.add(2**x == 4)
7210  >>> s.check()
7211  unknown
7212  >>> s.reason_unknown()
7213  '(incomplete (theory arithmetic))'
7214  """
7215  return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver)
7216 
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 6896 of file z3py.py.

6896  def reset(self):
6897  """Remove all asserted constraints and backtracking points created using `push()`.
6898 
6899  >>> x = Int('x')
6900  >>> s = Solver()
6901  >>> s.add(x > 0)
6902  >>> s
6903  [x > 0]
6904  >>> s.reset()
6905  >>> s
6906  []
6907  """
6908  Z3_solver_reset(self.ctx.ref(), self.solver)
6909 
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 6821 of file z3py.py.

6821  def set(self, *args, **keys):
6822  """Set a configuration option.
6823  The method `help()` return a string containing all available options.
6824 
6825  >>> s = Solver()
6826  >>> # The option MBQI can be set using three different approaches.
6827  >>> s.set(mbqi=True)
6828  >>> s.set('MBQI', True)
6829  >>> s.set(':mbqi', True)
6830  """
6831  p = args2params(args, keys, self.ctx)
6832  Z3_solver_set_params(self.ctx.ref(), self.solver, p.params)
6833 
void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p)
Set the given solver using the given parameters.
def args2params(arguments, keywords, ctx=None)
Definition: z3py.py:5398

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

7248  def sexpr(self):
7249  """Return a formatted string (in Lisp-like format) with all added constraints.
7250  We say the string is in s-expression format.
7251 
7252  >>> x = Int('x')
7253  >>> s = Solver()
7254  >>> s.add(x > 0)
7255  >>> s.add(x < 2)
7256  >>> r = s.sexpr()
7257  """
7258  return Z3_solver_to_string(self.ctx.ref(), self.solver)
7259 
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 7186 of file z3py.py.

7186  def statistics(self):
7187  """Return statistics for the last `check()`.
7188 
7189  >>> s = SimpleSolver()
7190  >>> x = Int('x')
7191  >>> s.add(x > 0)
7192  >>> s.check()
7193  sat
7194  >>> st = s.statistics()
7195  >>> st.get_key_value('final checks')
7196  1
7197  >>> len(st) > 0
7198  True
7199  >>> st[0] != 0
7200  True
7201  """
7202  return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx)
7203 
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 7264 of file z3py.py.

7264  def to_smt2(self):
7265  """return SMTLIB2 formatted benchmark for solver's assertions"""
7266  es = self.assertions()
7267  sz = len(es)
7268  sz1 = sz
7269  if sz1 > 0:
7270  sz1 -= 1
7271  v = (Ast * sz1)()
7272  for i in range(sz1):
7273  v[i] = es[i].as_ast()
7274  if sz > 0:
7275  e = es[sz1].as_ast()
7276  else:
7277  e = BoolVal(True, self.ctx).as_ast()
7279  self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e,
7280  )
7281 
7282 
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.
def BoolVal(val, ctx=None)
Definition: z3py.py:1675

◆ trail()

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

Definition at line 7181 of file z3py.py.

7181  def trail(self):
7182  """Return trail of the solver state after a check() call.
7183  """
7184  return AstVector(Z3_solver_get_trail(self.ctx.ref(), self.solver), self.ctx)
7185 
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 7173 of file z3py.py.

7173  def trail_levels(self):
7174  """Return trail and decision levels of the solver state after a check() call.
7175  """
7176  trail = self.trail()
7177  levels = (ctypes.c_uint * len(trail))()
7178  Z3_solver_get_levels(self.ctx.ref(), self.solver, trail.vector, len(trail), levels)
7179  return trail, levels
7180 
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 7229 of file z3py.py.

7229  def translate(self, target):
7230  """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
7231 
7232  >>> c1 = Context()
7233  >>> c2 = Context()
7234  >>> s1 = Solver(ctx=c1)
7235  >>> s2 = s1.translate(c2)
7236  """
7237  if z3_debug():
7238  _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
7239  solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref())
7240  return Solver(solver, target)
7241 
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.
def z3_debug()
Definition: z3py.py:64

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

7163  def units(self):
7164  """Return an AST vector containing all currently inferred units.
7165  """
7166  return AstVector(Z3_solver_get_units(self.ctx.ref(), self.solver), self.ctx)
7167 
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 7048 of file z3py.py.

7048  def unsat_core(self):
7049  """Return a subset (as an AST vector) of the assumptions provided to the last check().
7050 
7051  These are the assumptions Z3 used in the unsatisfiability proof.
7052  Assumptions are available in Z3. They are used to extract unsatisfiable cores.
7053  They may be also used to "retract" assumptions. Note that, assumptions are not really
7054  "soft constraints", but they can be used to implement them.
7055 
7056  >>> p1, p2, p3 = Bools('p1 p2 p3')
7057  >>> x, y = Ints('x y')
7058  >>> s = Solver()
7059  >>> s.add(Implies(p1, x > 0))
7060  >>> s.add(Implies(p2, y > x))
7061  >>> s.add(Implies(p2, y < 1))
7062  >>> s.add(Implies(p3, y > -3))
7063  >>> s.check(p1, p2, p3)
7064  unsat
7065  >>> core = s.unsat_core()
7066  >>> len(core)
7067  2
7068  >>> p1 in core
7069  True
7070  >>> p2 in core
7071  True
7072  >>> p3 in core
7073  False
7074  >>> # "Retracting" p2
7075  >>> s.check(p1, p3)
7076  sat
7077  """
7078  return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx)
7079 
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 6807 of file z3py.py.

◆ ctx

ctx

Definition at line 6806 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__(), ArithRef.__div__(), BitVecRef.__div__(), FPRef.__div__(), ExprRef.__eq__(), Probe.__eq__(), ArithRef.__ge__(), BitVecRef.__ge__(), Probe.__ge__(), FPRef.__ge__(), SeqRef.__ge__(), QuantifierRef.__getitem__(), ArrayRef.__getitem__(), 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__(), 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(), Fixedpoint.add_rule(), Optimize.add_soft(), 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(), 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(), 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(), 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(), 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 7124 of file z3py.py.

Referenced by Solver.cube_vars().

◆ solver

solver