Z3
Public Member Functions | Data Fields
Solver Class Reference
+ Inheritance diagram for Solver:

Public Member Functions

def __init__
 
def __del__ (self)
 
def set (self, args, keys)
 
def push (self)
 
def pop
 
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
 
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__
 
def sexpr (self)
 
def dimacs
 
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 6889 of file z3py.py.

Constructor & Destructor Documentation

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.
def __init__
Definition: z3py.py:6895
backtrack_level
Definition: z3py.py:6898
def set(self, args, keys)
Definition: z3py.py:6912
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 
def __del__(self)
Definition: z3py.py:6908
void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s)
Decrement the reference counter of the given solver.

Member Function Documentation

def __copy__ (   self)

Definition at line 7349 of file z3py.py.

7349  def __copy__(self):
7350  return self.translate(self.ctx)
7351 
def translate(self, target)
Definition: z3py.py:7336
def __copy__(self)
Definition: z3py.py:7349
def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 7352 of file z3py.py.

7352  def __deepcopy__(self, memo={}):
7353  return self.translate(self.ctx)
7354 
def translate(self, target)
Definition: z3py.py:7336
def __deepcopy__
Definition: z3py.py:7352
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 
def __iadd__(self, fml)
Definition: z3py.py:7031
def add(self, args)
Definition: z3py.py:7020
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 
def __repr__(self)
Definition: z3py.py:7332
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.

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

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 
def assert_exprs(self, args)
Definition: z3py.py:7001
def add(self, args)
Definition: z3py.py:7020
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 
def assert_exprs(self, args)
Definition: z3py.py:7001
def append(self, args)
Definition: z3py.py:7035
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 
def is_const(a)
Definition: z3py.py:1287
def assert_and_track(self, a, p)
Definition: z3py.py:7057
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 Bool
Definition: z3py.py:1724
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.

Referenced by Solver.add(), Fixedpoint.add(), Optimize.add(), Solver.append(), Fixedpoint.append(), and Fixedpoint.insert().

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 
def BoolSort
Definition: z3py.py:1687
def assert_exprs(self, args)
Definition: z3py.py:7001
void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a)
Assert a constraint into the solver.
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.

Referenced by Solver.to_smt2().

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.
def assertions(self)
Definition: z3py.py:7256
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.

Referenced by Solver.model(), Solver.proof(), Solver.reason_unknown(), Solver.statistics(), Solver.trail(), Solver.trail_levels(), and Solver.unsat_core().

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 
def BoolSort
Definition: z3py.py:1687
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:4085
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...
def check(self, assumptions)
Definition: z3py.py:7087
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 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:4085
def consequences(self, assumptions, variables)
Definition: z3py.py:7171
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.
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...
def cube
Definition: z3py.py:7208
def is_false(a)
Definition: z3py.py:1603
backtrack_level
Definition: z3py.py:6898
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 
def cube_vars(self)
Definition: z3py.py:7229
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 
def dimacs
Definition: z3py.py:7367
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.
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.
def from_file(self, filename)
Definition: z3py.py:7200
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 
def from_string(self, s)
Definition: z3py.py:7204
void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string file_name)
load solver assertions from a string.
def help (   self)
Display a string describing all available options.

Definition at line 7324 of file z3py.py.

Referenced by Solver.set().

7324  def help(self):
7325  """Display a string describing all available options."""
7326  print(Z3_solver_get_help(self.ctx.ref(), self.solver))
7327 
def help(self)
Definition: z3py.py:7324
Z3_string Z3_API Z3_solver_get_help(Z3_context c, Z3_solver s)
Return a string describing all solver available parameters.
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.
def import_model_converter(self, other)
Definition: z3py.py:7135
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 
def assert_exprs(self, args)
Definition: z3py.py:7001
def insert(self, args)
Definition: z3py.py:7046
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.

Referenced by FuncInterp.translate().

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.
def model(self)
Definition: z3py.py:7116
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...
def next(self, t)
Definition: z3py.py:7244
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 
def non_units(self)
Definition: z3py.py:7275
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.
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.
def num_scopes(self)
Definition: z3py.py:6969
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 
def param_descrs(self)
Definition: z3py.py:7328
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.
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.
def pop
Definition: z3py.py:6947
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.
def proof(self)
Definition: z3py.py:7252
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.

Referenced by Solver.reset().

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.
def push(self)
Definition: z3py.py:6925
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 
def reason_unknown(self)
Definition: z3py.py:7311
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...
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.
def reset(self)
Definition: z3py.py:6987
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 
def root(self, t)
Definition: z3py.py:7236
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...
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.
def args2params
Definition: z3py.py:5458
def set(self, args, keys)
Definition: z3py.py:6912
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.

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

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 
def sexpr(self)
Definition: z3py.py:7355
Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s)
Convert a solver into a string.
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.
Statistics.
Definition: z3py.py:6704
def statistics(self)
Definition: z3py.py:7293
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 
def BoolVal
Definition: z3py.py:1705
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:4085
def to_smt2(self)
Definition: z3py.py:7371
def assertions(self)
Definition: z3py.py:7256
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 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 
def trail(self)
Definition: z3py.py:7288
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...
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 
def trail_levels(self)
Definition: z3py.py:7280
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...
def trail(self)
Definition: z3py.py:7288
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.

Referenced by Solver.__copy__(), and Solver.__deepcopy__().

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 
def translate(self, target)
Definition: z3py.py:7336
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:62
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 
def units(self)
Definition: z3py.py:7270
Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s)
Return the set of units modulo model conversion.
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...
def unsat_core(self)
Definition: z3py.py:7139

Field Documentation

backtrack_level

Definition at line 6898 of file z3py.py.

ctx

Definition at line 6897 of file z3py.py.

Referenced by Solver.__copy__(), Solver.__deepcopy__(), Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Simplifier.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), Probe.__ne__(), Simplifier.add(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), ApplyResult.as_expr(), Solver.assert_and_track(), Optimize.assert_and_track(), Solver.assert_exprs(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Solver.assertions(), Optimize.assertions(), Solver.check(), Solver.consequences(), ParserContext.from_string(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_ground_sat_answer(), Fixedpoint.get_rule_names_along_trace(), Fixedpoint.get_rules(), Fixedpoint.get_rules_along_trace(), Solver.model(), Optimize.model(), Solver.next(), Solver.non_units(), Optimize.objectives(), Solver.param_descrs(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Simplifier.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Solver.proof(), Fixedpoint.query(), Solver.root(), Solver.set(), Fixedpoint.set(), Optimize.set(), Optimize.set_on_model(), Tactic.solver(), Solver.statistics(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), Solver.trail(), Solver.units(), Solver.unsat_core(), Optimize.unsat_core(), Fixedpoint.update_rule(), and Simplifier.using_params().

cube_vs

Definition at line 7215 of file z3py.py.

Referenced by Solver.cube_vars().

solver