Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
Public Member Functions | Data Fields
Solver Class Reference
+ Inheritance diagram for Solver:

Public Member Functions

def __init__
 
def __del__
 
def set
 
def push
 
def pop
 
def num_scopes
 
def reset
 
def assert_exprs
 
def add
 
def __iadd__
 
def append
 
def insert
 
def assert_and_track
 
def check
 
def model
 
def unsat_core
 
def consequences
 
def from_file
 
def from_string
 
def cube
 
def cube_vars
 
def proof
 
def assertions
 
def units
 
def non_units
 
def trail_levels
 
def trail
 
def statistics
 
def reason_unknown
 
def help
 
def param_descrs
 
def __repr__
 
def translate
 
def __copy__
 
def __deepcopy__
 
def sexpr
 
def dimacs
 
def to_smt2
 
- Public Member Functions inherited from Z3PPObject
def use_pp
 

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

Constructor & Destructor Documentation

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

Definition at line 6412 of file z3py.py.

6413  def __init__(self, solver=None, ctx=None):
6414  assert solver is None or ctx is not None
6415  self.ctx = _get_ctx(ctx)
6416  self.backtrack_level = 4000000000
6417  self.solver = None
6418  if solver is None:
6419  self.solver = Z3_mk_solver(self.ctx.ref())
6420  else:
6421  self.solver = solver
6422  Z3_solver_inc_ref(self.ctx.ref(), self.solver)
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:6412
backtrack_level
Definition: z3py.py:6415
def __del__ (   self)

Definition at line 6423 of file z3py.py.

6424  def __del__(self):
6425  if self.solver is not None and self.ctx.ref() is not None:
6426  Z3_solver_dec_ref(self.ctx.ref(), self.solver)
def __del__
Definition: z3py.py:6423
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 6841 of file z3py.py.

6842  def __copy__(self):
6843  return self.translate(self.ctx)
def __copy__
Definition: z3py.py:6841
def translate
Definition: z3py.py:6828
def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 6844 of file z3py.py.

6845  def __deepcopy__(self, memo={}):
6846  return self.translate(self.ctx)
def __deepcopy__
Definition: z3py.py:6844
def translate
Definition: z3py.py:6828
def __iadd__ (   self,
  fml 
)

Definition at line 6545 of file z3py.py.

6546  def __iadd__(self, fml):
6547  self.add(fml)
6548  return self
def __iadd__
Definition: z3py.py:6545
def add
Definition: z3py.py:6534
def __repr__ (   self)
Return a formatted string with all added constraints.

Definition at line 6824 of file z3py.py.

6825  def __repr__(self):
6826  """Return a formatted string with all added constraints."""
6827  return obj_to_string(self)
def __repr__
Definition: z3py.py:6824
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 6534 of file z3py.py.

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

6535  def add(self, *args):
6536  """Assert constraints into the solver.
6537 
6538  >>> x = Int('x')
6539  >>> s = Solver()
6540  >>> s.add(x > 0, x < 2)
6541  >>> s
6542  [x > 0, x < 2]
6543  """
6544  self.assert_exprs(*args)
def assert_exprs
Definition: z3py.py:6515
def add
Definition: z3py.py:6534
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 6549 of file z3py.py.

6550  def append(self, *args):
6551  """Assert constraints into the solver.
6552 
6553  >>> x = Int('x')
6554  >>> s = Solver()
6555  >>> s.append(x > 0, x < 2)
6556  >>> s
6557  [x > 0, x < 2]
6558  """
6559  self.assert_exprs(*args)
def assert_exprs
Definition: z3py.py:6515
def append
Definition: z3py.py:6549
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 6571 of file z3py.py.

6572  def assert_and_track(self, a, p):
6573  """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
6574 
6575  If `p` is a string, it will be automatically converted into a Boolean constant.
6576 
6577  >>> x = Int('x')
6578  >>> p3 = Bool('p3')
6579  >>> s = Solver()
6580  >>> s.set(unsat_core=True)
6581  >>> s.assert_and_track(x > 0, 'p1')
6582  >>> s.assert_and_track(x != 1, 'p2')
6583  >>> s.assert_and_track(x < 0, p3)
6584  >>> print(s.check())
6585  unsat
6586  >>> c = s.unsat_core()
6587  >>> len(c)
6588  2
6589  >>> Bool('p1') in c
6590  True
6591  >>> Bool('p2') in c
6592  False
6593  >>> p3 in c
6594  True
6595  """
6596  if isinstance(p, str):
6597  p = Bool(p, self.ctx)
6598  _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
6599  _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
6600  Z3_solver_assert_and_track(self.ctx.ref(), self.solver, a.as_ast(), p.as_ast())
def is_const
Definition: z3py.py:1152
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:1558
def assert_and_track
Definition: z3py.py:6571
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 6515 of file z3py.py.

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

6516  def assert_exprs(self, *args):
6517  """Assert constraints into the solver.
6518 
6519  >>> x = Int('x')
6520  >>> s = Solver()
6521  >>> s.assert_exprs(x > 0, x < 2)
6522  >>> s
6523  [x > 0, x < 2]
6524  """
6525  args = _get_args(args)
6526  s = BoolSort(self.ctx)
6527  for arg in args:
6528  if isinstance(arg, Goal) or isinstance(arg, AstVector):
6529  for f in arg:
6530  Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast())
6531  else:
6532  arg = s.cast(arg)
6533  Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast())
def BoolSort
Definition: z3py.py:1523
void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a)
Assert a constraint into the solver.
def assert_exprs
Definition: z3py.py:6515
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 6748 of file z3py.py.

Referenced by Solver.to_smt2().

6749  def assertions(self):
6750  """Return an AST vector containing all added constraints.
6751 
6752  >>> s = Solver()
6753  >>> s.assertions()
6754  []
6755  >>> a = Int('a')
6756  >>> s.add(a > 0)
6757  >>> s.add(a < 10)
6758  >>> s.assertions()
6759  [a > 0, a < 10]
6760  """
6761  return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
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
Definition: z3py.py:6748
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 6601 of file z3py.py.

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

6602  def check(self, *assumptions):
6603  """Check whether the assertions in the given solver plus the optional assumptions are consistent or not.
6604 
6605  >>> x = Int('x')
6606  >>> s = Solver()
6607  >>> s.check()
6608  sat
6609  >>> s.add(x > 0, x < 2)
6610  >>> s.check()
6611  sat
6612  >>> s.model().eval(x)
6613  1
6614  >>> s.add(x < 1)
6615  >>> s.check()
6616  unsat
6617  >>> s.reset()
6618  >>> s.add(2**x == 4)
6619  >>> s.check()
6620  unknown
6621  """
6622  assumptions = _get_args(assumptions)
6623  num = len(assumptions)
6624  _assumptions = (Ast * num)()
6625  for i in range(num):
6626  _assumptions[i] = assumptions[i].as_ast()
6627  r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions)
6628  return CheckSatResult(r)
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3358
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
Definition: z3py.py:6601
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 6680 of file z3py.py.

6681  def consequences(self, assumptions, variables):
6682  """Determine fixed values for the variables based on the solver state and assumptions.
6683  >>> s = Solver()
6684  >>> a, b, c, d = Bools('a b c d')
6685  >>> s.add(Implies(a,b), Implies(b, c))
6686  >>> s.consequences([a],[b,c,d])
6687  (sat, [Implies(a, b), Implies(a, c)])
6688  >>> s.consequences([Not(c),d],[a,b,c,d])
6689  (sat, [Implies(d, d), Implies(Not(c), Not(c)), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))])
6690  """
6691  if isinstance(assumptions, list):
6692  _asms = AstVector(None, self.ctx)
6693  for a in assumptions:
6694  _asms.push(a)
6695  assumptions = _asms
6696  if isinstance(variables, list):
6697  _vars = AstVector(None, self.ctx)
6698  for a in variables:
6699  _vars.push(a)
6700  variables = _vars
6701  _z3_assert(isinstance(assumptions, AstVector), "ast vector expected")
6702  _z3_assert(isinstance(variables, AstVector), "ast vector expected")
6703  consequences = AstVector(None, self.ctx)
6704  r = Z3_solver_get_consequences(self.ctx.ref(), self.solver, assumptions.vector, variables.vector, consequences.vector)
6705  sz = len(consequences)
6706  consequences = [ consequences[i] for i in range(sz) ]
6707  return CheckSatResult(r), consequences
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3358
def consequences
Definition: z3py.py:6680
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 6716 of file z3py.py.

6717  def cube(self, vars = None):
6718  """Get set of cubes
6719  The method takes an optional set of variables that restrict which
6720  variables may be used as a starting point for cubing.
6721  If vars is not None, then the first case split is based on a variable in
6722  this set.
6723  """
6724  self.cube_vs = AstVector(None, self.ctx)
6725  if vars is not None:
6726  for v in vars:
6727  self.cube_vs.push(v)
6728  while True:
6729  lvl = self.backtrack_level
6730  self.backtrack_level = 4000000000
6731  r = AstVector(Z3_solver_cube(self.ctx.ref(), self.solver, self.cube_vs.vector, lvl), self.ctx)
6732  if (len(r) == 1 and is_false(r[0])):
6733  return
6734  yield r
6735  if (len(r) == 0):
6736  return
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
Definition: z3py.py:1446
def cube
Definition: z3py.py:6716
backtrack_level
Definition: z3py.py:6415
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 6737 of file z3py.py.

6738  def cube_vars(self):
6739  """Access the set of variables that were touched by the most recently generated cube.
6740  This set of variables can be used as a starting point for additional cubes.
6741  The idea is that variables that appear in clauses that are reduced by the most recent
6742  cube are likely more useful to cube on."""
6743  return self.cube_vs
def cube_vars
Definition: z3py.py:6737
def dimacs (   self)
Return a textual representation of the solver in DIMACS format.

Definition at line 6858 of file z3py.py.

6859  def dimacs(self):
6860  """Return a textual representation of the solver in DIMACS format."""
6861  return Z3_solver_to_dimacs_string(self.ctx.ref(), self.solver)
Z3_string Z3_API Z3_solver_to_dimacs_string(Z3_context c, Z3_solver s)
Convert a solver into a DIMACS formatted string.
def dimacs
Definition: z3py.py:6858
def from_file (   self,
  filename 
)
Parse assertions from a file

Definition at line 6708 of file z3py.py.

6709  def from_file(self, filename):
6710  """Parse assertions from a file"""
6711  Z3_solver_from_file(self.ctx.ref(), self.solver, filename)
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
Definition: z3py.py:6708
def from_string (   self,
  s 
)
Parse assertions from a string

Definition at line 6712 of file z3py.py.

6713  def from_string(self, s):
6714  """Parse assertions from a string"""
6715  Z3_solver_from_string(self.ctx.ref(), self.solver, s)
void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string file_name)
load solver assertions from a string.
def from_string
Definition: z3py.py:6712
def help (   self)
Display a string describing all available options.

Definition at line 6816 of file z3py.py.

Referenced by Solver.set().

6817  def help(self):
6818  """Display a string describing all available options."""
6819  print(Z3_solver_get_help(self.ctx.ref(), self.solver))
def help
Definition: z3py.py:6816
Z3_string Z3_API Z3_solver_get_help(Z3_context c, Z3_solver s)
Return a string describing all solver available parameters.
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 6560 of file z3py.py.

6561  def insert(self, *args):
6562  """Assert constraints into the solver.
6563 
6564  >>> x = Int('x')
6565  >>> s = Solver()
6566  >>> s.insert(x > 0, x < 2)
6567  >>> s
6568  [x > 0, x < 2]
6569  """
6570  self.assert_exprs(*args)
def insert
Definition: z3py.py:6560
def assert_exprs
Definition: z3py.py:6515
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 6629 of file z3py.py.

Referenced by FuncInterp.translate().

6630  def model(self):
6631  """Return a model for the last `check()`.
6632 
6633  This function raises an exception if
6634  a model is not available (e.g., last `check()` returned unsat).
6635 
6636  >>> s = Solver()
6637  >>> a = Int('a')
6638  >>> s.add(a + 2 == 0)
6639  >>> s.check()
6640  sat
6641  >>> s.model()
6642  [a = -2]
6643  """
6644  try:
6645  return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx)
6646  except Z3Exception:
6647  raise Z3Exception("model is not available")
def model
Definition: z3py.py:6629
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 non_units (   self)
Return an AST vector containing all atomic formulas in solver state that are not units.

Definition at line 6767 of file z3py.py.

6768  def non_units(self):
6769  """Return an AST vector containing all atomic formulas in solver state that are not units.
6770  """
6771  return AstVector(Z3_solver_get_non_units(self.ctx.ref(), self.solver), self.ctx)
def non_units
Definition: z3py.py:6767
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()
0L
>>> s.push()
>>> s.num_scopes()
1L
>>> s.push()
>>> s.num_scopes()
2L
>>> s.pop()
>>> s.num_scopes()
1L

Definition at line 6483 of file z3py.py.

6484  def num_scopes(self):
6485  """Return the current number of backtracking points.
6486 
6487  >>> s = Solver()
6488  >>> s.num_scopes()
6489  0L
6490  >>> s.push()
6491  >>> s.num_scopes()
6492  1L
6493  >>> s.push()
6494  >>> s.num_scopes()
6495  2L
6496  >>> s.pop()
6497  >>> s.num_scopes()
6498  1L
6499  """
6500  return Z3_solver_get_num_scopes(self.ctx.ref(), self.solver)
def num_scopes
Definition: z3py.py:6483
unsigned Z3_API Z3_solver_get_num_scopes(Z3_context c, Z3_solver s)
Return the number of backtracking points.
def param_descrs (   self)
Return the parameter description set.

Definition at line 6820 of file z3py.py.

6821  def param_descrs(self):
6822  """Return the parameter description set."""
6823  return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx)
def param_descrs
Definition: z3py.py:6820
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 6461 of file z3py.py.

6462  def pop(self, num=1):
6463  """Backtrack \c num backtracking points.
6464 
6465  >>> x = Int('x')
6466  >>> s = Solver()
6467  >>> s.add(x > 0)
6468  >>> s
6469  [x > 0]
6470  >>> s.push()
6471  >>> s.add(x < 1)
6472  >>> s
6473  [x > 0, x < 1]
6474  >>> s.check()
6475  unsat
6476  >>> s.pop()
6477  >>> s.check()
6478  sat
6479  >>> s
6480  [x > 0]
6481  """
6482  Z3_solver_pop(self.ctx.ref(), self.solver, num)
void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n)
Backtrack n backtracking points.
def pop
Definition: z3py.py:6461
def proof (   self)
Return a proof for the last `check()`. Proof construction must be enabled.

Definition at line 6744 of file z3py.py.

6745  def proof(self):
6746  """Return a proof for the last `check()`. Proof construction must be enabled."""
6747  return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
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
Definition: z3py.py:6744
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 6439 of file z3py.py.

Referenced by Solver.reset().

6440  def push(self):
6441  """Create a backtracking point.
6442 
6443  >>> x = Int('x')
6444  >>> s = Solver()
6445  >>> s.add(x > 0)
6446  >>> s
6447  [x > 0]
6448  >>> s.push()
6449  >>> s.add(x < 1)
6450  >>> s
6451  [x > 0, x < 1]
6452  >>> s.check()
6453  unsat
6454  >>> s.pop()
6455  >>> s.check()
6456  sat
6457  >>> s
6458  [x > 0]
6459  """
6460  Z3_solver_push(self.ctx.ref(), self.solver)
void Z3_API Z3_solver_push(Z3_context c, Z3_solver s)
Create a backtracking point.
def push
Definition: z3py.py:6439
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 6803 of file z3py.py.

6804  def reason_unknown(self):
6805  """Return a string describing why the last `check()` returned `unknown`.
6806 
6807  >>> x = Int('x')
6808  >>> s = SimpleSolver()
6809  >>> s.add(2**x == 4)
6810  >>> s.check()
6811  unknown
6812  >>> s.reason_unknown()
6813  '(incomplete (theory arithmetic))'
6814  """
6815  return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver)
def reason_unknown
Definition: z3py.py:6803
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 6501 of file z3py.py.

6502  def reset(self):
6503  """Remove all asserted constraints and backtracking points created using `push()`.
6504 
6505  >>> x = Int('x')
6506  >>> s = Solver()
6507  >>> s.add(x > 0)
6508  >>> s
6509  [x > 0]
6510  >>> s.reset()
6511  >>> s
6512  []
6513  """
6514  Z3_solver_reset(self.ctx.ref(), self.solver)
void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)
Remove all assertions from the solver.
def reset
Definition: z3py.py:6501
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 6427 of file z3py.py.

6428  def set(self, *args, **keys):
6429  """Set a configuration option. The method `help()` return a string containing all available options.
6430 
6431  >>> s = Solver()
6432  >>> # The option MBQI can be set using three different approaches.
6433  >>> s.set(mbqi=True)
6434  >>> s.set('MBQI', True)
6435  >>> s.set(':mbqi', True)
6436  """
6437  p = args2params(args, keys, self.ctx)
6438  Z3_solver_set_params(self.ctx.ref(), self.solver, p.params)
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:5050
def set
Definition: z3py.py:6427
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 6847 of file z3py.py.

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

6848  def sexpr(self):
6849  """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
6850 
6851  >>> x = Int('x')
6852  >>> s = Solver()
6853  >>> s.add(x > 0)
6854  >>> s.add(x < 2)
6855  >>> r = s.sexpr()
6856  """
6857  return Z3_solver_to_string(self.ctx.ref(), self.solver)
Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s)
Convert a solver into a string.
def sexpr
Definition: z3py.py:6847
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 6785 of file z3py.py.

6786  def statistics(self):
6787  """Return statistics for the last `check()`.
6788 
6789  >>> s = SimpleSolver()
6790  >>> x = Int('x')
6791  >>> s.add(x > 0)
6792  >>> s.check()
6793  sat
6794  >>> st = s.statistics()
6795  >>> st.get_key_value('final checks')
6796  1
6797  >>> len(st) > 0
6798  True
6799  >>> st[0] != 0
6800  True
6801  """
6802  return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx)
Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s)
Return statistics for the given solver.
Statistics.
Definition: z3py.py:6235
def statistics
Definition: z3py.py:6785
def to_smt2 (   self)
return SMTLIB2 formatted benchmark for solver's assertions

Definition at line 6862 of file z3py.py.

6863  def to_smt2(self):
6864  """return SMTLIB2 formatted benchmark for solver's assertions"""
6865  es = self.assertions()
6866  sz = len(es)
6867  sz1 = sz
6868  if sz1 > 0:
6869  sz1 -= 1
6870  v = (Ast * sz1)()
6871  for i in range(sz1):
6872  v[i] = es[i].as_ast()
6873  if sz > 0:
6874  e = es[sz1].as_ast()
6875  else:
6876  e = BoolVal(True, self.ctx).as_ast()
6877  return Z3_benchmark_to_smtlib_string(self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e)
def BoolVal
Definition: z3py.py:1540
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3358
def to_smt2
Definition: z3py.py:6862
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 assertions
Definition: z3py.py:6748
def trail (   self)
Return trail of the solver state after a check() call. 

Definition at line 6780 of file z3py.py.

6781  def trail(self):
6782  """Return trail of the solver state after a check() call.
6783  """
6784  return AstVector(Z3_solver_get_trail(self.ctx.ref(), self.solver), self.ctx)
def trail
Definition: z3py.py:6780
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 6772 of file z3py.py.

6773  def trail_levels(self):
6774  """Return trail and decision levels of the solver state after a check() call.
6775  """
6776  trail = self.trail()
6777  levels = (ctypes.c_uint * len(trail))()
6778  Z3_solver_get_levels(self.ctx.ref(), self.solver, trail.vector, len(trail), levels)
6779  return trail, levels
def trail
Definition: z3py.py:6780
def trail_levels
Definition: z3py.py:6772
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 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 6828 of file z3py.py.

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

6829  def translate(self, target):
6830  """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
6831 
6832  >>> c1 = Context()
6833  >>> c2 = Context()
6834  >>> s1 = Solver(ctx=c1)
6835  >>> s2 = s1.translate(c2)
6836  """
6837  if z3_debug():
6838  _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
6839  solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref())
6840  return Solver(solver, target)
def translate
Definition: z3py.py:6828
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:58
def units (   self)
Return an AST vector containing all currently inferred units.

Definition at line 6762 of file z3py.py.

6763  def units(self):
6764  """Return an AST vector containing all currently inferred units.
6765  """
6766  return AstVector(Z3_solver_get_units(self.ctx.ref(), self.solver), self.ctx)
Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s)
Return the set of units modulo model conversion.
def units
Definition: z3py.py:6762
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 6648 of file z3py.py.

6649  def unsat_core(self):
6650  """Return a subset (as an AST vector) of the assumptions provided to the last check().
6651 
6652  These are the assumptions Z3 used in the unsatisfiability proof.
6653  Assumptions are available in Z3. They are used to extract unsatisfiable cores.
6654  They may be also used to "retract" assumptions. Note that, assumptions are not really
6655  "soft constraints", but they can be used to implement them.
6656 
6657  >>> p1, p2, p3 = Bools('p1 p2 p3')
6658  >>> x, y = Ints('x y')
6659  >>> s = Solver()
6660  >>> s.add(Implies(p1, x > 0))
6661  >>> s.add(Implies(p2, y > x))
6662  >>> s.add(Implies(p2, y < 1))
6663  >>> s.add(Implies(p3, y > -3))
6664  >>> s.check(p1, p2, p3)
6665  unsat
6666  >>> core = s.unsat_core()
6667  >>> len(core)
6668  2
6669  >>> p1 in core
6670  True
6671  >>> p2 in core
6672  True
6673  >>> p3 in core
6674  False
6675  >>> # "Retracting" p2
6676  >>> s.check(p1, p3)
6677  sat
6678  """
6679  return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx)
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
Definition: z3py.py:6648

Field Documentation

backtrack_level

Definition at line 6415 of file z3py.py.

ctx

Definition at line 6414 of file z3py.py.

Referenced by Solver.__copy__(), Solver.__deepcopy__(), Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), Probe.__ne__(), 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.consequences(), 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.non_units(), Optimize.objectives(), Solver.param_descrs(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Solver.proof(), Fixedpoint.query(), Solver.set(), Fixedpoint.set(), Optimize.set(), Tactic.solver(), Solver.statistics(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), Solver.trail(), Solver.units(), Solver.unsat_core(), Optimize.unsat_core(), and Fixedpoint.update_rule().

cube_vs

Definition at line 6723 of file z3py.py.

Referenced by Solver.cube_vars().

solver

Definition at line 6416 of file z3py.py.

Referenced by Solver.__del__(), Solver.assert_and_track(), Solver.assert_exprs(), Solver.assertions(), Solver.check(), Solver.consequences(), Solver.dimacs(), Solver.from_file(), Solver.from_string(), Solver.help(), Solver.model(), Solver.non_units(), Solver.num_scopes(), Solver.param_descrs(), Solver.pop(), Solver.proof(), Solver.push(), Solver.reason_unknown(), Solver.reset(), Solver.set(), Solver.sexpr(), Solver.statistics(), Solver.trail(), Solver.trail_levels(), Solver.translate(), Solver.units(), and Solver.unsat_core().