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

Public Member Functions

def __init__ (self, solver=None, ctx=None)
 
def __del__ (self)
 
def set (self, args, keys)
 
def push (self)
 
def pop (self, num=1)
 
def num_scopes (self)
 
def reset (self)
 
def assert_exprs (self, args)
 
def add (self, args)
 
def __iadd__ (self, fml)
 
def append (self, args)
 
def insert (self, args)
 
def assert_and_track (self, a, p)
 
def check (self, assumptions)
 
def model (self)
 
def unsat_core (self)
 
def consequences (self, assumptions, variables)
 
def from_file (self, filename)
 
def from_string (self, s)
 
def cube (self, vars=None)
 
def cube_vars (self)
 
def proof (self)
 
def assertions (self)
 
def units (self)
 
def non_units (self)
 
def trail_levels (self)
 
def trail (self)
 
def statistics (self)
 
def reason_unknown (self)
 
def help (self)
 
def param_descrs (self)
 
def __repr__ (self)
 
def translate (self, target)
 
def __copy__ (self)
 
def __deepcopy__ (self, memo={})
 
def sexpr (self)
 
def dimacs (self)
 
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 6409 of file z3py.py.

Constructor & Destructor Documentation

◆ __init__()

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

Definition at line 6412 of file z3py.py.

6412  def __init__(self, solver=None, ctx=None):
6413  assert solver is None or ctx is not None
6414  self.ctx = _get_ctx(ctx)
6415  self.backtrack_level = 4000000000
6416  self.solver = None
6417  if solver is None:
6418  self.solver = Z3_mk_solver(self.ctx.ref())
6419  else:
6420  self.solver = solver
6421  Z3_solver_inc_ref(self.ctx.ref(), self.solver)
6422 
Z3_solver Z3_API Z3_mk_solver(Z3_context c)
Create a new solver. This solver is a "combined solver" (see combined_solver module) that internally ...
void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s)
Increment the reference counter of the given solver.

◆ __del__()

def __del__ (   self)

Definition at line 6423 of file z3py.py.

6423  def __del__(self):
6424  if self.solver is not None and self.ctx.ref() is not None:
6425  Z3_solver_dec_ref(self.ctx.ref(), self.solver)
6426 
void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s)
Decrement the reference counter of the given solver.

Member Function Documentation

◆ __copy__()

def __copy__ (   self)

Definition at line 6841 of file z3py.py.

6841  def __copy__(self):
6842  return self.translate(self.ctx)
6843 

◆ __deepcopy__()

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 6844 of file z3py.py.

6844  def __deepcopy__(self, memo={}):
6845  return self.translate(self.ctx)
6846 

◆ __iadd__()

def __iadd__ (   self,
  fml 
)

Definition at line 6545 of file z3py.py.

6545  def __iadd__(self, fml):
6546  self.add(fml)
6547  return self
6548 

◆ __repr__()

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

Definition at line 6824 of file z3py.py.

6824  def __repr__(self):
6825  """Return a formatted string with all added constraints."""
6826  return obj_to_string(self)
6827 

◆ add()

def add (   self,
  args 
)
Assert constraints into the solver.

>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0, x < 2)
>>> s
[x > 0, x < 2]

Definition at line 6534 of file z3py.py.

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

6534  def add(self, *args):
6535  """Assert constraints into the solver.
6536 
6537  >>> x = Int('x')
6538  >>> s = Solver()
6539  >>> s.add(x > 0, x < 2)
6540  >>> s
6541  [x > 0, x < 2]
6542  """
6543  self.assert_exprs(*args)
6544 

◆ append()

def append (   self,
  args 
)
Assert constraints into the solver.

>>> x = Int('x')
>>> s = Solver()
>>> s.append(x > 0, x < 2)
>>> s
[x > 0, x < 2]

Definition at line 6549 of file z3py.py.

6549  def append(self, *args):
6550  """Assert constraints into the solver.
6551 
6552  >>> x = Int('x')
6553  >>> s = Solver()
6554  >>> s.append(x > 0, x < 2)
6555  >>> s
6556  [x > 0, x < 2]
6557  """
6558  self.assert_exprs(*args)
6559 

◆ assert_and_track()

def assert_and_track (   self,
  a,
  p 
)
Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.

If `p` is a string, it will be automatically converted into a Boolean constant.

>>> x = Int('x')
>>> p3 = Bool('p3')
>>> s = Solver()
>>> s.set(unsat_core=True)
>>> s.assert_and_track(x > 0,  'p1')
>>> s.assert_and_track(x != 1, 'p2')
>>> s.assert_and_track(x < 0,  p3)
>>> print(s.check())
unsat
>>> c = s.unsat_core()
>>> len(c)
2
>>> Bool('p1') in c
True
>>> Bool('p2') in c
False
>>> p3 in c
True

Definition at line 6571 of file z3py.py.

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

◆ assert_exprs()

def assert_exprs (   self,
  args 
)
Assert constraints into the solver.

>>> x = Int('x')
>>> s = Solver()
>>> s.assert_exprs(x > 0, x < 2)
>>> s
[x > 0, x < 2]

Definition at line 6515 of file z3py.py.

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

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

◆ assertions()

def assertions (   self)
Return an AST vector containing all added constraints.

>>> s = Solver()
>>> s.assertions()
[]
>>> a = Int('a')
>>> s.add(a > 0)
>>> s.add(a < 10)
>>> s.assertions()
[a > 0, a < 10]

Definition at line 6748 of file z3py.py.

Referenced by Solver.to_smt2().

6748  def assertions(self):
6749  """Return an AST vector containing all added constraints.
6750 
6751  >>> s = Solver()
6752  >>> s.assertions()
6753  []
6754  >>> a = Int('a')
6755  >>> s.add(a > 0)
6756  >>> s.add(a < 10)
6757  >>> s.assertions()
6758  [a > 0, a < 10]
6759  """
6760  return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
6761 
Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s)
Return the set of asserted formulas on the solver.

◆ check()

def check (   self,
  assumptions 
)
Check whether the assertions in the given solver plus the optional assumptions are consistent or not.

>>> x = Int('x')
>>> s = Solver()
>>> s.check()
sat
>>> s.add(x > 0, x < 2)
>>> s.check()
sat
>>> s.model().eval(x)
1
>>> s.add(x < 1)
>>> s.check()
unsat
>>> s.reset()
>>> s.add(2**x == 4)
>>> s.check()
unknown

Definition at line 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().

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

◆ consequences()

def consequences (   self,
  assumptions,
  variables 
)
Determine fixed values for the variables based on the solver state and assumptions.        
>>> s = Solver()
>>> a, b, c, d = Bools('a b c d')
>>> s.add(Implies(a,b), Implies(b, c))
>>> s.consequences([a],[b,c,d])
(sat, [Implies(a, b), Implies(a, c)])
>>> s.consequences([Not(c),d],[a,b,c,d])
(sat, [Implies(d, d), Implies(Not(c), Not(c)), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))])

Definition at line 6680 of file z3py.py.

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

◆ cube()

def cube (   self,
  vars = None 
)
Get set of cubes
The method takes an optional set of variables that restrict which
variables may be used as a starting point for cubing.
If vars is not None, then the first case split is based on a variable in
this set.

Definition at line 6716 of file z3py.py.

6716  def cube(self, vars = None):
6717  """Get set of cubes
6718  The method takes an optional set of variables that restrict which
6719  variables may be used as a starting point for cubing.
6720  If vars is not None, then the first case split is based on a variable in
6721  this set.
6722  """
6723  self.cube_vs = AstVector(None, self.ctx)
6724  if vars is not None:
6725  for v in vars:
6726  self.cube_vs.push(v)
6727  while True:
6728  lvl = self.backtrack_level
6729  self.backtrack_level = 4000000000
6730  r = AstVector(Z3_solver_cube(self.ctx.ref(), self.solver, self.cube_vs.vector, lvl), self.ctx)
6731  if (len(r) == 1 and is_false(r[0])):
6732  return
6733  yield r
6734  if (len(r) == 0):
6735  return
6736 
Z3_ast_vector Z3_API Z3_solver_cube(Z3_context c, Z3_solver s, Z3_ast_vector vars, unsigned backtrack_level)
extract a next cube for a solver. The last cube is the constant true or false. The number of (non-con...
def is_false(a)
Definition: z3py.py:1446

◆ cube_vars()

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

Definition at line 6737 of file z3py.py.

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

◆ dimacs()

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

Definition at line 6858 of file z3py.py.

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

◆ from_file()

def from_file (   self,
  filename 
)
Parse assertions from a file

Definition at line 6708 of file z3py.py.

6708  def from_file(self, filename):
6709  """Parse assertions from a file"""
6710  Z3_solver_from_file(self.ctx.ref(), self.solver, filename)
6711 
void Z3_API Z3_solver_from_file(Z3_context c, Z3_solver s, Z3_string file_name)
load solver assertions from a file.

◆ from_string()

def from_string (   self,
  s 
)
Parse assertions from a string

Definition at line 6712 of file z3py.py.

6712  def from_string(self, s):
6713  """Parse assertions from a string"""
6714  Z3_solver_from_string(self.ctx.ref(), self.solver, s)
6715 
void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string file_name)
load solver assertions from a string.

◆ help()

def help (   self)
Display a string describing all available options.

Definition at line 6816 of file z3py.py.

Referenced by Solver.set().

6816  def help(self):
6817  """Display a string describing all available options."""
6818  print(Z3_solver_get_help(self.ctx.ref(), self.solver))
6819 
Z3_string Z3_API Z3_solver_get_help(Z3_context c, Z3_solver s)
Return a string describing all solver available parameters.

◆ insert()

def insert (   self,
  args 
)
Assert constraints into the solver.

>>> x = Int('x')
>>> s = Solver()
>>> s.insert(x > 0, x < 2)
>>> s
[x > 0, x < 2]

Definition at line 6560 of file z3py.py.

6560  def insert(self, *args):
6561  """Assert constraints into the solver.
6562 
6563  >>> x = Int('x')
6564  >>> s = Solver()
6565  >>> s.insert(x > 0, x < 2)
6566  >>> s
6567  [x > 0, x < 2]
6568  """
6569  self.assert_exprs(*args)
6570 

◆ model()

def model (   self)
Return a model for the last `check()`.

This function raises an exception if
a model is not available (e.g., last `check()` returned unsat).

>>> s = Solver()
>>> a = Int('a')
>>> s.add(a + 2 == 0)
>>> s.check()
sat
>>> s.model()
[a = -2]

Definition at line 6629 of file z3py.py.

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

◆ non_units()

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.

6767  def non_units(self):
6768  """Return an AST vector containing all atomic formulas in solver state that are not units.
6769  """
6770  return AstVector(Z3_solver_get_non_units(self.ctx.ref(), self.solver), self.ctx)
6771 
Z3_ast_vector Z3_API Z3_solver_get_non_units(Z3_context c, Z3_solver s)
Return the set of non units in the solver state.

◆ num_scopes()

def num_scopes (   self)
Return the current number of backtracking points.

>>> s = Solver()
>>> s.num_scopes()
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.

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

◆ param_descrs()

def param_descrs (   self)
Return the parameter description set.

Definition at line 6820 of file z3py.py.

6820  def param_descrs(self):
6821  """Return the parameter description set."""
6822  return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx)
6823 
Z3_param_descrs Z3_API Z3_solver_get_param_descrs(Z3_context c, Z3_solver s)
Return the parameter description set for the given solver object.

◆ pop()

def pop (   self,
  num = 1 
)
Backtrack \c num backtracking points.

>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0)
>>> s
[x > 0]
>>> s.push()
>>> s.add(x < 1)
>>> s
[x > 0, x < 1]
>>> s.check()
unsat
>>> s.pop()
>>> s.check()
sat
>>> s
[x > 0]

Definition at line 6461 of file z3py.py.

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

◆ proof()

def proof (   self)
Return a proof for the last `check()`. Proof construction must be enabled.

Definition at line 6744 of file z3py.py.

6744  def proof(self):
6745  """Return a proof for the last `check()`. Proof construction must be enabled."""
6746  return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
6747 
Z3_ast Z3_API Z3_solver_get_proof(Z3_context c, Z3_solver s)
Retrieve the proof for the last Z3_solver_check or Z3_solver_check_assumptions.

◆ push()

def push (   self)
Create a backtracking point.

>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0)
>>> s
[x > 0]
>>> s.push()
>>> s.add(x < 1)
>>> s
[x > 0, x < 1]
>>> s.check()
unsat
>>> s.pop()
>>> s.check()
sat
>>> s
[x > 0]

Definition at line 6439 of file z3py.py.

Referenced by Solver.reset().

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

◆ reason_unknown()

def reason_unknown (   self)
Return a string describing why the last `check()` returned `unknown`.

>>> x = Int('x')
>>> s = SimpleSolver()
>>> s.add(2**x == 4)
>>> s.check()
unknown
>>> s.reason_unknown()
'(incomplete (theory arithmetic))'

Definition at line 6803 of file z3py.py.

6803  def reason_unknown(self):
6804  """Return a string describing why the last `check()` returned `unknown`.
6805 
6806  >>> x = Int('x')
6807  >>> s = SimpleSolver()
6808  >>> s.add(2**x == 4)
6809  >>> s.check()
6810  unknown
6811  >>> s.reason_unknown()
6812  '(incomplete (theory arithmetic))'
6813  """
6814  return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver)
6815 
Z3_string Z3_API Z3_solver_get_reason_unknown(Z3_context c, Z3_solver s)
Return a brief justification for an "unknown" result (i.e., Z3_L_UNDEF) for the commands Z3_solver_ch...

◆ reset()

def reset (   self)
Remove all asserted constraints and backtracking points created using `push()`.

>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0)
>>> s
[x > 0]
>>> s.reset()
>>> s
[]

Definition at line 6501 of file z3py.py.

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

◆ set()

def set (   self,
  args,
  keys 
)
Set a configuration option. The method `help()` return a string containing all available options.

>>> s = Solver()
>>> # The option MBQI can be set using three different approaches.
>>> s.set(mbqi=True)
>>> s.set('MBQI', True)
>>> s.set(':mbqi', True)

Definition at line 6427 of file z3py.py.

6427  def set(self, *args, **keys):
6428  """Set a configuration option. The method `help()` return a string containing all available options.
6429 
6430  >>> s = Solver()
6431  >>> # The option MBQI can be set using three different approaches.
6432  >>> s.set(mbqi=True)
6433  >>> s.set('MBQI', True)
6434  >>> s.set(':mbqi', True)
6435  """
6436  p = args2params(args, keys, self.ctx)
6437  Z3_solver_set_params(self.ctx.ref(), self.solver, p.params)
6438 
void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p)
Set the given solver using the given parameters.
def args2params(arguments, keywords, ctx=None)
Definition: z3py.py:5050

◆ sexpr()

def sexpr (   self)
Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.

>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0)
>>> s.add(x < 2)
>>> r = s.sexpr()

Definition at line 6847 of file z3py.py.

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

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

◆ statistics()

def statistics (   self)
Return statistics for the last `check()`.

>>> s = SimpleSolver()
>>> x = Int('x')
>>> s.add(x > 0)
>>> s.check()
sat
>>> st = s.statistics()
>>> st.get_key_value('final checks')
1
>>> len(st) > 0
True
>>> st[0] != 0
True

Definition at line 6785 of file z3py.py.

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

◆ to_smt2()

def to_smt2 (   self)
return SMTLIB2 formatted benchmark for solver's assertions

Definition at line 6862 of file z3py.py.

6862  def to_smt2(self):
6863  """return SMTLIB2 formatted benchmark for solver's assertions"""
6864  es = self.assertions()
6865  sz = len(es)
6866  sz1 = sz
6867  if sz1 > 0:
6868  sz1 -= 1
6869  v = (Ast * sz1)()
6870  for i in range(sz1):
6871  v[i] = es[i].as_ast()
6872  if sz > 0:
6873  e = es[sz1].as_ast()
6874  else:
6875  e = BoolVal(True, self.ctx).as_ast()
6876  return Z3_benchmark_to_smtlib_string(self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e)
6877 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3358
def BoolVal(val, ctx=None)
Definition: z3py.py:1540
Z3_string Z3_API Z3_benchmark_to_smtlib_string(Z3_context c, Z3_string name, Z3_string logic, Z3_string status, Z3_string attributes, unsigned num_assumptions, Z3_ast const assumptions[], Z3_ast formula)
Convert the given benchmark into SMT-LIB formatted string.

◆ trail()

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

Definition at line 6780 of file z3py.py.

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

◆ trail_levels()

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.

6772  def trail_levels(self):
6773  """Return trail and decision levels of the solver state after a check() call.
6774  """
6775  trail = self.trail()
6776  levels = (ctypes.c_uint * len(trail))()
6777  Z3_solver_get_levels(self.ctx.ref(), self.solver, trail.vector, len(trail), levels)
6778  return trail, levels
6779 
void Z3_API Z3_solver_get_levels(Z3_context c, Z3_solver s, Z3_ast_vector literals, unsigned sz, unsigned levels[])
retrieve the decision depth of Boolean literals (variables or their negations). Assumes a check-sat c...

◆ translate()

def translate (   self,
  target 
)
Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.

>>> c1 = Context()
>>> c2 = Context()
>>> s1 = Solver(ctx=c1)
>>> s2 = s1.translate(c2)

Definition at line 6828 of file z3py.py.

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

◆ units()

def units (   self)
Return an AST vector containing all currently inferred units.

Definition at line 6762 of file z3py.py.

6762  def units(self):
6763  """Return an AST vector containing all currently inferred units.
6764  """
6765  return AstVector(Z3_solver_get_units(self.ctx.ref(), self.solver), self.ctx)
6766 
Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s)
Return the set of units modulo model conversion.

◆ unsat_core()

def unsat_core (   self)
Return a subset (as an AST vector) of the assumptions provided to the last check().

These are the assumptions Z3 used in the unsatisfiability proof.
Assumptions are available in Z3. They are used to extract unsatisfiable cores.
They may be also used to "retract" assumptions. Note that, assumptions are not really
"soft constraints", but they can be used to implement them.

>>> p1, p2, p3 = Bools('p1 p2 p3')
>>> x, y       = Ints('x y')
>>> s          = Solver()
>>> s.add(Implies(p1, x > 0))
>>> s.add(Implies(p2, y > x))
>>> s.add(Implies(p2, y < 1))
>>> s.add(Implies(p3, y > -3))
>>> s.check(p1, p2, p3)
unsat
>>> core = s.unsat_core()
>>> len(core)
2
>>> p1 in core
True
>>> p2 in core
True
>>> p3 in core
False
>>> # "Retracting" p2
>>> s.check(p1, p3)
sat

Definition at line 6648 of file z3py.py.

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

Field Documentation

◆ backtrack_level

backtrack_level

Definition at line 6415 of file z3py.py.

◆ ctx

ctx

Definition at line 6414 of file z3py.py.

Referenced by Probe.__call__(), Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), Fixedpoint.__del__(), Optimize.__del__(), ApplyResult.__del__(), Tactic.__del__(), Probe.__del__(), Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), ApplyResult.__len__(), Probe.__lt__(), Probe.__ne__(), Fixedpoint.add_cover(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), ApplyResult.as_expr(), Optimize.assert_and_track(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Optimize.assertions(), Optimize.check(), Optimize.from_file(), Optimize.from_string(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_ground_sat_answer(), Fixedpoint.get_num_levels(), Fixedpoint.get_rule_names_along_trace(), Fixedpoint.get_rules(), Fixedpoint.get_rules_along_trace(), Fixedpoint.help(), Optimize.help(), Tactic.help(), Optimize.maximize(), Optimize.minimize(), Optimize.model(), Optimize.objectives(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Optimize.pop(), Optimize.push(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), Fixedpoint.reason_unknown(), Optimize.reason_unknown(), Fixedpoint.register_relation(), Fixedpoint.set(), Optimize.set(), Fixedpoint.set_predicate_representation(), Fixedpoint.sexpr(), Optimize.sexpr(), ApplyResult.sexpr(), Tactic.solver(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), Fixedpoint.to_string(), Optimize.unsat_core(), and Fixedpoint.update_rule().

◆ cube_vs

cube_vs

Definition at line 6723 of file z3py.py.

◆ solver

solver

Definition at line 6416 of file z3py.py.