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

Public Member Functions

def __init__
 
def __del__ (self)
 
def __enter__ (self)
 
def __exit__ (self, exc_info)
 
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 interrupt (self)
 
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 6943 of file z3py.py.

Constructor & Destructor Documentation

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

Definition at line 6949 of file z3py.py.

6949  def __init__(self, solver=None, ctx=None, logFile=None):
6950  assert solver is None or ctx is not None
6951  self.ctx = _get_ctx(ctx)
6952  self.backtrack_level = 4000000000
6953  self.solver = None
6954  if solver is None:
6955  self.solver = Z3_mk_solver(self.ctx.ref())
6956  else:
6957  self.solver = solver
6958  Z3_solver_inc_ref(self.ctx.ref(), self.solver)
6959  if logFile is not None:
6960  self.set("smtlib2_log", logFile)
6961 
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:6949
backtrack_level
Definition: z3py.py:6952
def set(self, args, keys)
Definition: z3py.py:6973
def __del__ (   self)

Definition at line 6962 of file z3py.py.

6962  def __del__(self):
6963  if self.solver is not None and self.ctx.ref() is not None and Z3_solver_dec_ref is not None:
6964  Z3_solver_dec_ref(self.ctx.ref(), self.solver)
6965 
def __del__(self)
Definition: z3py.py:6962
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 7417 of file z3py.py.

7417  def __copy__(self):
7418  return self.translate(self.ctx)
7419 
def translate(self, target)
Definition: z3py.py:7404
def __copy__(self)
Definition: z3py.py:7417
def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 7420 of file z3py.py.

7420  def __deepcopy__(self, memo={}):
7421  return self.translate(self.ctx)
7422 
def translate(self, target)
Definition: z3py.py:7404
def __deepcopy__
Definition: z3py.py:7420
def __enter__ (   self)

Definition at line 6966 of file z3py.py.

6966  def __enter__(self):
6967  self.push()
6968  return self
6969 
def push(self)
Definition: z3py.py:6986
def __enter__(self)
Definition: z3py.py:6966
def __exit__ (   self,
  exc_info 
)

Definition at line 6970 of file z3py.py.

6970  def __exit__(self, *exc_info):
6971  self.pop()
6972 
def __exit__(self, exc_info)
Definition: z3py.py:6970
def pop
Definition: z3py.py:7008
def __iadd__ (   self,
  fml 
)

Definition at line 7092 of file z3py.py.

7092  def __iadd__(self, fml):
7093  self.add(fml)
7094  return self
7095 
def __iadd__(self, fml)
Definition: z3py.py:7092
def add(self, args)
Definition: z3py.py:7081
def __repr__ (   self)
Return a formatted string with all added constraints.

Definition at line 7400 of file z3py.py.

7400  def __repr__(self):
7401  """Return a formatted string with all added constraints."""
7402  return obj_to_string(self)
7403 
def __repr__(self)
Definition: z3py.py:7400
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 7081 of file z3py.py.

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

7081  def add(self, *args):
7082  """Assert constraints into the solver.
7083 
7084  >>> x = Int('x')
7085  >>> s = Solver()
7086  >>> s.add(x > 0, x < 2)
7087  >>> s
7088  [x > 0, x < 2]
7089  """
7090  self.assert_exprs(*args)
7091 
def assert_exprs(self, args)
Definition: z3py.py:7062
def add(self, args)
Definition: z3py.py:7081
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 7096 of file z3py.py.

7096  def append(self, *args):
7097  """Assert constraints into the solver.
7098 
7099  >>> x = Int('x')
7100  >>> s = Solver()
7101  >>> s.append(x > 0, x < 2)
7102  >>> s
7103  [x > 0, x < 2]
7104  """
7105  self.assert_exprs(*args)
7106 
def assert_exprs(self, args)
Definition: z3py.py:7062
def append(self, args)
Definition: z3py.py:7096
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 7118 of file z3py.py.

7118  def assert_and_track(self, a, p):
7119  """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
7120 
7121  If `p` is a string, it will be automatically converted into a Boolean constant.
7122 
7123  >>> x = Int('x')
7124  >>> p3 = Bool('p3')
7125  >>> s = Solver()
7126  >>> s.set(unsat_core=True)
7127  >>> s.assert_and_track(x > 0, 'p1')
7128  >>> s.assert_and_track(x != 1, 'p2')
7129  >>> s.assert_and_track(x < 0, p3)
7130  >>> print(s.check())
7131  unsat
7132  >>> c = s.unsat_core()
7133  >>> len(c)
7134  2
7135  >>> Bool('p1') in c
7136  True
7137  >>> Bool('p2') in c
7138  False
7139  >>> p3 in c
7140  True
7141  """
7142  if isinstance(p, str):
7143  p = Bool(p, self.ctx)
7144  _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
7145  _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
7146  Z3_solver_assert_and_track(self.ctx.ref(), self.solver, a.as_ast(), p.as_ast())
7147 
def is_const(a)
Definition: z3py.py:1309
def assert_and_track(self, a, p)
Definition: z3py.py:7118
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:1768
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 7062 of file z3py.py.

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

7062  def assert_exprs(self, *args):
7063  """Assert constraints into the solver.
7064 
7065  >>> x = Int('x')
7066  >>> s = Solver()
7067  >>> s.assert_exprs(x > 0, x < 2)
7068  >>> s
7069  [x > 0, x < 2]
7070  """
7071  args = _get_args(args)
7072  s = BoolSort(self.ctx)
7073  for arg in args:
7074  if isinstance(arg, Goal) or isinstance(arg, AstVector):
7075  for f in arg:
7076  Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast())
7077  else:
7078  arg = s.cast(arg)
7079  Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast())
7080 
def BoolSort
Definition: z3py.py:1731
def assert_exprs(self, args)
Definition: z3py.py:7062
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 7324 of file z3py.py.

Referenced by Solver.to_smt2().

7324  def assertions(self):
7325  """Return an AST vector containing all added constraints.
7326 
7327  >>> s = Solver()
7328  >>> s.assertions()
7329  []
7330  >>> a = Int('a')
7331  >>> s.add(a > 0)
7332  >>> s.add(a < 10)
7333  >>> s.assertions()
7334  [a > 0, a < 10]
7335  """
7336  return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
7337 
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:7324
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 7148 of file z3py.py.

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

7148  def check(self, *assumptions):
7149  """Check whether the assertions in the given solver plus the optional assumptions are consistent or not.
7150 
7151  >>> x = Int('x')
7152  >>> s = Solver()
7153  >>> s.check()
7154  sat
7155  >>> s.add(x > 0, x < 2)
7156  >>> s.check()
7157  sat
7158  >>> s.model().eval(x)
7159  1
7160  >>> s.add(x < 1)
7161  >>> s.check()
7162  unsat
7163  >>> s.reset()
7164  >>> s.add(2**x == 4)
7165  >>> s.check()
7166  unknown
7167  """
7168  s = BoolSort(self.ctx)
7169  assumptions = _get_args(assumptions)
7170  num = len(assumptions)
7171  _assumptions = (Ast * num)()
7172  for i in range(num):
7173  _assumptions[i] = s.cast(assumptions[i]).as_ast()
7174  r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions)
7175  return CheckSatResult(r)
7176 
def BoolSort
Definition: z3py.py:1731
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:7148
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 7239 of file z3py.py.

7239  def consequences(self, assumptions, variables):
7240  """Determine fixed values for the variables based on the solver state and assumptions.
7241  >>> s = Solver()
7242  >>> a, b, c, d = Bools('a b c d')
7243  >>> s.add(Implies(a,b), Implies(b, c))
7244  >>> s.consequences([a],[b,c,d])
7245  (sat, [Implies(a, b), Implies(a, c)])
7246  >>> s.consequences([Not(c),d],[a,b,c,d])
7247  (sat, [Implies(d, d), Implies(Not(c), Not(c)), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))])
7248  """
7249  if isinstance(assumptions, list):
7250  _asms = AstVector(None, self.ctx)
7251  for a in assumptions:
7252  _asms.push(a)
7253  assumptions = _asms
7254  if isinstance(variables, list):
7255  _vars = AstVector(None, self.ctx)
7256  for a in variables:
7257  _vars.push(a)
7258  variables = _vars
7259  _z3_assert(isinstance(assumptions, AstVector), "ast vector expected")
7260  _z3_assert(isinstance(variables, AstVector), "ast vector expected")
7261  consequences = AstVector(None, self.ctx)
7262  r = Z3_solver_get_consequences(self.ctx.ref(), self.solver, assumptions.vector,
7263  variables.vector, consequences.vector)
7264  sz = len(consequences)
7265  consequences = [consequences[i] for i in range(sz)]
7266  return CheckSatResult(r), consequences
7267 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:4085
def consequences(self, assumptions, variables)
Definition: z3py.py:7239
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 7276 of file z3py.py.

7276  def cube(self, vars=None):
7277  """Get set of cubes
7278  The method takes an optional set of variables that restrict which
7279  variables may be used as a starting point for cubing.
7280  If vars is not None, then the first case split is based on a variable in
7281  this set.
7282  """
7283  self.cube_vs = AstVector(None, self.ctx)
7284  if vars is not None:
7285  for v in vars:
7286  self.cube_vs.push(v)
7287  while True:
7288  lvl = self.backtrack_level
7289  self.backtrack_level = 4000000000
7290  r = AstVector(Z3_solver_cube(self.ctx.ref(), self.solver, self.cube_vs.vector, lvl), self.ctx)
7291  if (len(r) == 1 and is_false(r[0])):
7292  return
7293  yield r
7294  if (len(r) == 0):
7295  return
7296 
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:7276
def is_false(a)
Definition: z3py.py:1647
backtrack_level
Definition: z3py.py:6952
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 7297 of file z3py.py.

7297  def cube_vars(self):
7298  """Access the set of variables that were touched by the most recently generated cube.
7299  This set of variables can be used as a starting point for additional cubes.
7300  The idea is that variables that appear in clauses that are reduced by the most recent
7301  cube are likely more useful to cube on."""
7302  return self.cube_vs
7303 
def cube_vars(self)
Definition: z3py.py:7297
def dimacs (   self,
  include_names = True 
)
Return a textual representation of the solver in DIMACS format.

Definition at line 7435 of file z3py.py.

7435  def dimacs(self, include_names=True):
7436  """Return a textual representation of the solver in DIMACS format."""
7437  return Z3_solver_to_dimacs_string(self.ctx.ref(), self.solver, include_names)
7438 
def dimacs
Definition: z3py.py:7435
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 7268 of file z3py.py.

7268  def from_file(self, filename):
7269  """Parse assertions from a file"""
7270  Z3_solver_from_file(self.ctx.ref(), self.solver, filename)
7271 
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:7268
def from_string (   self,
  s 
)
Parse assertions from a string

Definition at line 7272 of file z3py.py.

7272  def from_string(self, s):
7273  """Parse assertions from a string"""
7274  Z3_solver_from_string(self.ctx.ref(), self.solver, s)
7275 
def from_string(self, s)
Definition: z3py.py:7272
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 7392 of file z3py.py.

Referenced by Solver.set().

7392  def help(self):
7393  """Display a string describing all available options."""
7394  print(Z3_solver_get_help(self.ctx.ref(), self.solver))
7395 
def help(self)
Definition: z3py.py:7392
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 7196 of file z3py.py.

7196  def import_model_converter(self, other):
7197  """Import model converter from other into the current solver"""
7198  Z3_solver_import_model_converter(self.ctx.ref(), other.solver, self.solver)
7199 
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:7196
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 7107 of file z3py.py.

7107  def insert(self, *args):
7108  """Assert constraints into the solver.
7109 
7110  >>> x = Int('x')
7111  >>> s = Solver()
7112  >>> s.insert(x > 0, x < 2)
7113  >>> s
7114  [x > 0, x < 2]
7115  """
7116  self.assert_exprs(*args)
7117 
def assert_exprs(self, args)
Definition: z3py.py:7062
def insert(self, args)
Definition: z3py.py:7107
def interrupt (   self)
Interrupt the execution of the solver object.
Remarks: This ensures that the interrupt applies only
to the given solver object and it applies only if it is running.

Definition at line 7200 of file z3py.py.

7200  def interrupt(self):
7201  """Interrupt the execution of the solver object.
7202  Remarks: This ensures that the interrupt applies only
7203  to the given solver object and it applies only if it is running.
7204  """
7205  Z3_solver_interrupt(self.ctx.ref(), self.solver)
7206 
def interrupt(self)
Definition: z3py.py:7200
void Z3_API Z3_solver_interrupt(Z3_context c, Z3_solver s)
Solver local interrupt. Normally you should use Z3_interrupt to cancel solvers because only one solve...
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 7177 of file z3py.py.

Referenced by FuncInterp.translate().

7177  def model(self):
7178  """Return a model for the last `check()`.
7179 
7180  This function raises an exception if
7181  a model is not available (e.g., last `check()` returned unsat).
7182 
7183  >>> s = Solver()
7184  >>> a = Int('a')
7185  >>> s.add(a + 2 == 0)
7186  >>> s.check()
7187  sat
7188  >>> s.model()
7189  [a = -2]
7190  """
7191  try:
7192  return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx)
7193  except Z3Exception:
7194  raise Z3Exception("model is not available")
7195 
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:7177
def next (   self,
  t 
)

Definition at line 7312 of file z3py.py.

7312  def next(self, t):
7313  t = _py2expr(t, self.ctx)
7314  """Retrieve congruence closure sibling of the term t relative to the current search state
7315  The function primarily works for SimpleSolver. Terms and variables that are
7316  eliminated during pre-processing are not visible to the congruence closure.
7317  """
7318  return _to_expr_ref(Z3_solver_congruence_next(self.ctx.ref(), self.solver, t.ast), self.ctx)
7319 
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:7312
def non_units (   self)
Return an AST vector containing all atomic formulas in solver state that are not units.

Definition at line 7343 of file z3py.py.

7343  def non_units(self):
7344  """Return an AST vector containing all atomic formulas in solver state that are not units.
7345  """
7346  return AstVector(Z3_solver_get_non_units(self.ctx.ref(), self.solver), self.ctx)
7347 
def non_units(self)
Definition: z3py.py:7343
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 7030 of file z3py.py.

7030  def num_scopes(self):
7031  """Return the current number of backtracking points.
7032 
7033  >>> s = Solver()
7034  >>> s.num_scopes()
7035  0
7036  >>> s.push()
7037  >>> s.num_scopes()
7038  1
7039  >>> s.push()
7040  >>> s.num_scopes()
7041  2
7042  >>> s.pop()
7043  >>> s.num_scopes()
7044  1
7045  """
7046  return Z3_solver_get_num_scopes(self.ctx.ref(), self.solver)
7047 
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:7030
def param_descrs (   self)
Return the parameter description set.

Definition at line 7396 of file z3py.py.

7396  def param_descrs(self):
7397  """Return the parameter description set."""
7398  return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx)
7399 
def param_descrs(self)
Definition: z3py.py:7396
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 7008 of file z3py.py.

Referenced by Solver.__exit__().

7008  def pop(self, num=1):
7009  """Backtrack \\c num backtracking points.
7010 
7011  >>> x = Int('x')
7012  >>> s = Solver()
7013  >>> s.add(x > 0)
7014  >>> s
7015  [x > 0]
7016  >>> s.push()
7017  >>> s.add(x < 1)
7018  >>> s
7019  [x > 0, x < 1]
7020  >>> s.check()
7021  unsat
7022  >>> s.pop()
7023  >>> s.check()
7024  sat
7025  >>> s
7026  [x > 0]
7027  """
7028  Z3_solver_pop(self.ctx.ref(), self.solver, num)
7029 
void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n)
Backtrack n backtracking points.
def pop
Definition: z3py.py:7008
def proof (   self)
Return a proof for the last `check()`. Proof construction must be enabled.

Definition at line 7320 of file z3py.py.

7320  def proof(self):
7321  """Return a proof for the last `check()`. Proof construction must be enabled."""
7322  return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
7323 
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:7320
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 6986 of file z3py.py.

Referenced by Solver.__enter__(), and Solver.reset().

6986  def push(self):
6987  """Create a backtracking point.
6988 
6989  >>> x = Int('x')
6990  >>> s = Solver()
6991  >>> s.add(x > 0)
6992  >>> s
6993  [x > 0]
6994  >>> s.push()
6995  >>> s.add(x < 1)
6996  >>> s
6997  [x > 0, x < 1]
6998  >>> s.check()
6999  unsat
7000  >>> s.pop()
7001  >>> s.check()
7002  sat
7003  >>> s
7004  [x > 0]
7005  """
7006  Z3_solver_push(self.ctx.ref(), self.solver)
7007 
void Z3_API Z3_solver_push(Z3_context c, Z3_solver s)
Create a backtracking point.
def push(self)
Definition: z3py.py:6986
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 7379 of file z3py.py.

7379  def reason_unknown(self):
7380  """Return a string describing why the last `check()` returned `unknown`.
7381 
7382  >>> x = Int('x')
7383  >>> s = SimpleSolver()
7384  >>> s.add(2**x == 4)
7385  >>> s.check()
7386  unknown
7387  >>> s.reason_unknown()
7388  '(incomplete (theory arithmetic))'
7389  """
7390  return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver)
7391 
def reason_unknown(self)
Definition: z3py.py:7379
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 7048 of file z3py.py.

7048  def reset(self):
7049  """Remove all asserted constraints and backtracking points created using `push()`.
7050 
7051  >>> x = Int('x')
7052  >>> s = Solver()
7053  >>> s.add(x > 0)
7054  >>> s
7055  [x > 0]
7056  >>> s.reset()
7057  >>> s
7058  []
7059  """
7060  Z3_solver_reset(self.ctx.ref(), self.solver)
7061 
void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)
Remove all assertions from the solver.
def reset(self)
Definition: z3py.py:7048
def root (   self,
  t 
)

Definition at line 7304 of file z3py.py.

7304  def root(self, t):
7305  t = _py2expr(t, self.ctx)
7306  """Retrieve congruence closure root of the term t relative to the current search state
7307  The function primarily works for SimpleSolver. Terms and variables that are
7308  eliminated during pre-processing are not visible to the congruence closure.
7309  """
7310  return _to_expr_ref(Z3_solver_congruence_root(self.ctx.ref(), self.solver, t.ast), self.ctx)
7311 
def root(self, t)
Definition: z3py.py:7304
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 6973 of file z3py.py.

6973  def set(self, *args, **keys):
6974  """Set a configuration option.
6975  The method `help()` return a string containing all available options.
6976 
6977  >>> s = Solver()
6978  >>> # The option MBQI can be set using three different approaches.
6979  >>> s.set(mbqi=True)
6980  >>> s.set('MBQI', True)
6981  >>> s.set(':mbqi', True)
6982  """
6983  p = args2params(args, keys, self.ctx)
6984  Z3_solver_set_params(self.ctx.ref(), self.solver, p.params)
6985 
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:5512
def set(self, args, keys)
Definition: z3py.py:6973
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 7423 of file z3py.py.

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

7423  def sexpr(self):
7424  """Return a formatted string (in Lisp-like format) with all added constraints.
7425  We say the string is in s-expression format.
7426 
7427  >>> x = Int('x')
7428  >>> s = Solver()
7429  >>> s.add(x > 0)
7430  >>> s.add(x < 2)
7431  >>> r = s.sexpr()
7432  """
7433  return Z3_solver_to_string(self.ctx.ref(), self.solver)
7434 
def sexpr(self)
Definition: z3py.py:7423
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 7361 of file z3py.py.

7361  def statistics(self):
7362  """Return statistics for the last `check()`.
7363 
7364  >>> s = SimpleSolver()
7365  >>> x = Int('x')
7366  >>> s.add(x > 0)
7367  >>> s.check()
7368  sat
7369  >>> st = s.statistics()
7370  >>> st.get_key_value('final checks')
7371  1
7372  >>> len(st) > 0
7373  True
7374  >>> st[0] != 0
7375  True
7376  """
7377  return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx)
7378 
Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s)
Return statistics for the given solver.
Statistics.
Definition: z3py.py:6758
def statistics(self)
Definition: z3py.py:7361
def to_smt2 (   self)
return SMTLIB2 formatted benchmark for solver's assertions

Definition at line 7439 of file z3py.py.

7439  def to_smt2(self):
7440  """return SMTLIB2 formatted benchmark for solver's assertions"""
7441  es = self.assertions()
7442  sz = len(es)
7443  sz1 = sz
7444  if sz1 > 0:
7445  sz1 -= 1
7446  v = (Ast * sz1)()
7447  for i in range(sz1):
7448  v[i] = es[i].as_ast()
7449  if sz > 0:
7450  e = es[sz1].as_ast()
7451  else:
7452  e = BoolVal(True, self.ctx).as_ast()
7454  self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e,
7455  )
7456 
7457 
def BoolVal
Definition: z3py.py:1749
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:4085
def to_smt2(self)
Definition: z3py.py:7439
def assertions(self)
Definition: z3py.py:7324
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 7356 of file z3py.py.

7356  def trail(self):
7357  """Return trail of the solver state after a check() call.
7358  """
7359  return AstVector(Z3_solver_get_trail(self.ctx.ref(), self.solver), self.ctx)
7360 
def trail(self)
Definition: z3py.py:7356
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 7348 of file z3py.py.

7348  def trail_levels(self):
7349  """Return trail and decision levels of the solver state after a check() call.
7350  """
7351  trail = self.trail()
7352  levels = (ctypes.c_uint * len(trail))()
7353  Z3_solver_get_levels(self.ctx.ref(), self.solver, trail.vector, len(trail), levels)
7354  return trail, levels
7355 
def trail_levels(self)
Definition: z3py.py:7348
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:7356
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 7404 of file z3py.py.

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

7404  def translate(self, target):
7405  """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
7406 
7407  >>> c1 = Context()
7408  >>> c2 = Context()
7409  >>> s1 = Solver(ctx=c1)
7410  >>> s2 = s1.translate(c2)
7411  """
7412  if z3_debug():
7413  _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
7414  solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref())
7415  return Solver(solver, target)
7416 
def translate(self, target)
Definition: z3py.py:7404
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 7338 of file z3py.py.

7338  def units(self):
7339  """Return an AST vector containing all currently inferred units.
7340  """
7341  return AstVector(Z3_solver_get_units(self.ctx.ref(), self.solver), self.ctx)
7342 
def units(self)
Definition: z3py.py:7338
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 7207 of file z3py.py.

7207  def unsat_core(self):
7208  """Return a subset (as an AST vector) of the assumptions provided to the last check().
7209 
7210  These are the assumptions Z3 used in the unsatisfiability proof.
7211  Assumptions are available in Z3. They are used to extract unsatisfiable cores.
7212  They may be also used to "retract" assumptions. Note that, assumptions are not really
7213  "soft constraints", but they can be used to implement them.
7214 
7215  >>> p1, p2, p3 = Bools('p1 p2 p3')
7216  >>> x, y = Ints('x y')
7217  >>> s = Solver()
7218  >>> s.add(Implies(p1, x > 0))
7219  >>> s.add(Implies(p2, y > x))
7220  >>> s.add(Implies(p2, y < 1))
7221  >>> s.add(Implies(p3, y > -3))
7222  >>> s.check(p1, p2, p3)
7223  unsat
7224  >>> core = s.unsat_core()
7225  >>> len(core)
7226  2
7227  >>> p1 in core
7228  True
7229  >>> p2 in core
7230  True
7231  >>> p3 in core
7232  False
7233  >>> # "Retracting" p2
7234  >>> s.check(p1, p3)
7235  sat
7236  """
7237  return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx)
7238 
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:7207

Field Documentation

backtrack_level

Definition at line 6952 of file z3py.py.

ctx

Definition at line 6951 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 7283 of file z3py.py.

Referenced by Solver.cube_vars().

solver