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

Public Member Functions

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

Constructor & Destructor Documentation

◆ __init__()

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

Definition at line 6439 of file z3py.py.

6439  def __init__(self, solver=None, ctx=None, logFile=None):
6440  assert solver is None or ctx is not None
6441  self.ctx = _get_ctx(ctx)
6442  self.backtrack_level = 4000000000
6443  self.solver = None
6444  if solver is None:
6445  self.solver = Z3_mk_solver(self.ctx.ref())
6446  else:
6447  self.solver = solver
6448  Z3_solver_inc_ref(self.ctx.ref(), self.solver)
6449  if logFile is not None:
6450  self.set("solver.smtlib2_log", logFile)
6451 
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 6452 of file z3py.py.

6452  def __del__(self):
6453  if self.solver is not None and self.ctx.ref() is not None:
6454  Z3_solver_dec_ref(self.ctx.ref(), self.solver)
6455 
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 6874 of file z3py.py.

6874  def __copy__(self):
6875  return self.translate(self.ctx)
6876 

◆ __deepcopy__()

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 6877 of file z3py.py.

6877  def __deepcopy__(self, memo={}):
6878  return self.translate(self.ctx)
6879 

◆ __iadd__()

def __iadd__ (   self,
  fml 
)

Definition at line 6574 of file z3py.py.

6574  def __iadd__(self, fml):
6575  self.add(fml)
6576  return self
6577 

◆ __repr__()

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

Definition at line 6857 of file z3py.py.

6857  def __repr__(self):
6858  """Return a formatted string with all added constraints."""
6859  return obj_to_string(self)
6860 

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

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

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

◆ append()

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

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

Definition at line 6578 of file z3py.py.

6578  def append(self, *args):
6579  """Assert constraints into the solver.
6580 
6581  >>> x = Int('x')
6582  >>> s = Solver()
6583  >>> s.append(x > 0, x < 2)
6584  >>> s
6585  [x > 0, x < 2]
6586  """
6587  self.assert_exprs(*args)
6588 

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

6600  def assert_and_track(self, a, p):
6601  """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
6602 
6603  If `p` is a string, it will be automatically converted into a Boolean constant.
6604 
6605  >>> x = Int('x')
6606  >>> p3 = Bool('p3')
6607  >>> s = Solver()
6608  >>> s.set(unsat_core=True)
6609  >>> s.assert_and_track(x > 0, 'p1')
6610  >>> s.assert_and_track(x != 1, 'p2')
6611  >>> s.assert_and_track(x < 0, p3)
6612  >>> print(s.check())
6613  unsat
6614  >>> c = s.unsat_core()
6615  >>> len(c)
6616  2
6617  >>> Bool('p1') in c
6618  True
6619  >>> Bool('p2') in c
6620  False
6621  >>> p3 in c
6622  True
6623  """
6624  if isinstance(p, str):
6625  p = Bool(p, self.ctx)
6626  _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
6627  _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
6628  Z3_solver_assert_and_track(self.ctx.ref(), self.solver, a.as_ast(), p.as_ast())
6629 
def is_const(a)
Definition: z3py.py:1162
def Bool(name, ctx=None)
Definition: z3py.py:1568
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 6544 of file z3py.py.

6544  def assert_exprs(self, *args):
6545  """Assert constraints into the solver.
6546 
6547  >>> x = Int('x')
6548  >>> s = Solver()
6549  >>> s.assert_exprs(x > 0, x < 2)
6550  >>> s
6551  [x > 0, x < 2]
6552  """
6553  args = _get_args(args)
6554  s = BoolSort(self.ctx)
6555  for arg in args:
6556  if isinstance(arg, Goal) or isinstance(arg, AstVector):
6557  for f in arg:
6558  Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast())
6559  else:
6560  arg = s.cast(arg)
6561  Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast())
6562 
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:1533

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

◆ assertions()

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

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

Definition at line 6781 of file z3py.py.

6781  def assertions(self):
6782  """Return an AST vector containing all added constraints.
6783 
6784  >>> s = Solver()
6785  >>> s.assertions()
6786  []
6787  >>> a = Int('a')
6788  >>> s.add(a > 0)
6789  >>> s.add(a < 10)
6790  >>> s.assertions()
6791  [a > 0, a < 10]
6792  """
6793  return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
6794 
Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s)
Return the set of asserted formulas on the solver.

Referenced by Solver.to_smt2().

◆ check()

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

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

Definition at line 6630 of file z3py.py.

6630  def check(self, *assumptions):
6631  """Check whether the assertions in the given solver plus the optional assumptions are consistent or not.
6632 
6633  >>> x = Int('x')
6634  >>> s = Solver()
6635  >>> s.check()
6636  sat
6637  >>> s.add(x > 0, x < 2)
6638  >>> s.check()
6639  sat
6640  >>> s.model().eval(x)
6641  1
6642  >>> s.add(x < 1)
6643  >>> s.check()
6644  unsat
6645  >>> s.reset()
6646  >>> s.add(2**x == 4)
6647  >>> s.check()
6648  unknown
6649  """
6650  assumptions = _get_args(assumptions)
6651  num = len(assumptions)
6652  _assumptions = (Ast * num)()
6653  for i in range(num):
6654  _assumptions[i] = assumptions[i].as_ast()
6655  r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions)
6656  return CheckSatResult(r)
6657 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3431
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 6713 of file z3py.py.

6713  def consequences(self, assumptions, variables):
6714  """Determine fixed values for the variables based on the solver state and assumptions.
6715  >>> s = Solver()
6716  >>> a, b, c, d = Bools('a b c d')
6717  >>> s.add(Implies(a,b), Implies(b, c))
6718  >>> s.consequences([a],[b,c,d])
6719  (sat, [Implies(a, b), Implies(a, c)])
6720  >>> s.consequences([Not(c),d],[a,b,c,d])
6721  (sat, [Implies(d, d), Implies(Not(c), Not(c)), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))])
6722  """
6723  if isinstance(assumptions, list):
6724  _asms = AstVector(None, self.ctx)
6725  for a in assumptions:
6726  _asms.push(a)
6727  assumptions = _asms
6728  if isinstance(variables, list):
6729  _vars = AstVector(None, self.ctx)
6730  for a in variables:
6731  _vars.push(a)
6732  variables = _vars
6733  _z3_assert(isinstance(assumptions, AstVector), "ast vector expected")
6734  _z3_assert(isinstance(variables, AstVector), "ast vector expected")
6735  consequences = AstVector(None, self.ctx)
6736  r = Z3_solver_get_consequences(self.ctx.ref(), self.solver, assumptions.vector, variables.vector, consequences.vector)
6737  sz = len(consequences)
6738  consequences = [ consequences[i] for i in range(sz) ]
6739  return CheckSatResult(r), consequences
6740 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3431
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 6749 of file z3py.py.

6749  def cube(self, vars = None):
6750  """Get set of cubes
6751  The method takes an optional set of variables that restrict which
6752  variables may be used as a starting point for cubing.
6753  If vars is not None, then the first case split is based on a variable in
6754  this set.
6755  """
6756  self.cube_vs = AstVector(None, self.ctx)
6757  if vars is not None:
6758  for v in vars:
6759  self.cube_vs.push(v)
6760  while True:
6761  lvl = self.backtrack_level
6762  self.backtrack_level = 4000000000
6763  r = AstVector(Z3_solver_cube(self.ctx.ref(), self.solver, self.cube_vs.vector, lvl), self.ctx)
6764  if (len(r) == 1 and is_false(r[0])):
6765  return
6766  yield r
6767  if (len(r) == 0):
6768  return
6769 
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:1456

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

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

◆ dimacs()

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

Definition at line 6891 of file z3py.py.

6891  def dimacs(self):
6892  """Return a textual representation of the solver in DIMACS format."""
6893  return Z3_solver_to_dimacs_string(self.ctx.ref(), self.solver)
6894 
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 6741 of file z3py.py.

6741  def from_file(self, filename):
6742  """Parse assertions from a file"""
6743  Z3_solver_from_file(self.ctx.ref(), self.solver, filename)
6744 
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 6745 of file z3py.py.

6745  def from_string(self, s):
6746  """Parse assertions from a string"""
6747  Z3_solver_from_string(self.ctx.ref(), self.solver, s)
6748 
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 6849 of file z3py.py.

6849  def help(self):
6850  """Display a string describing all available options."""
6851  print(Z3_solver_get_help(self.ctx.ref(), self.solver))
6852 
Z3_string Z3_API Z3_solver_get_help(Z3_context c, Z3_solver s)
Return a string describing all solver available parameters.

◆ import_model_converter()

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

Definition at line 6677 of file z3py.py.

6677  def import_model_converter(self, other):
6678  """Import model converter from other into the current solver"""
6679  Z3_solver_import_model_converter(self.ctx.ref(), other.solver, self.solver)
6680 
void Z3_API Z3_solver_import_model_converter(Z3_context ctx, Z3_solver src, Z3_solver dst)
Ad-hoc method for importing model conversion from solver.

◆ insert()

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

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

Definition at line 6589 of file z3py.py.

6589  def insert(self, *args):
6590  """Assert constraints into the solver.
6591 
6592  >>> x = Int('x')
6593  >>> s = Solver()
6594  >>> s.insert(x > 0, x < 2)
6595  >>> s
6596  [x > 0, x < 2]
6597  """
6598  self.assert_exprs(*args)
6599 

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

6658  def model(self):
6659  """Return a model for the last `check()`.
6660 
6661  This function raises an exception if
6662  a model is not available (e.g., last `check()` returned unsat).
6663 
6664  >>> s = Solver()
6665  >>> a = Int('a')
6666  >>> s.add(a + 2 == 0)
6667  >>> s.check()
6668  sat
6669  >>> s.model()
6670  [a = -2]
6671  """
6672  try:
6673  return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx)
6674  except Z3Exception:
6675  raise Z3Exception("model is not available")
6676 
Z3_model Z3_API Z3_solver_get_model(Z3_context c, Z3_solver s)
Retrieve the model for the last Z3_solver_check or Z3_solver_check_assumptions.

Referenced by FuncInterp.translate().

◆ non_units()

def non_units (   self)
Return an AST vector containing all atomic formulas in solver state that are not units.

Definition at line 6800 of file z3py.py.

6800  def non_units(self):
6801  """Return an AST vector containing all atomic formulas in solver state that are not units.
6802  """
6803  return AstVector(Z3_solver_get_non_units(self.ctx.ref(), self.solver), self.ctx)
6804 
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 6512 of file z3py.py.

6512  def num_scopes(self):
6513  """Return the current number of backtracking points.
6514 
6515  >>> s = Solver()
6516  >>> s.num_scopes()
6517  0L
6518  >>> s.push()
6519  >>> s.num_scopes()
6520  1L
6521  >>> s.push()
6522  >>> s.num_scopes()
6523  2L
6524  >>> s.pop()
6525  >>> s.num_scopes()
6526  1L
6527  """
6528  return Z3_solver_get_num_scopes(self.ctx.ref(), self.solver)
6529 
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 6853 of file z3py.py.

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

6490  def pop(self, num=1):
6491  """Backtrack \c num backtracking points.
6492 
6493  >>> x = Int('x')
6494  >>> s = Solver()
6495  >>> s.add(x > 0)
6496  >>> s
6497  [x > 0]
6498  >>> s.push()
6499  >>> s.add(x < 1)
6500  >>> s
6501  [x > 0, x < 1]
6502  >>> s.check()
6503  unsat
6504  >>> s.pop()
6505  >>> s.check()
6506  sat
6507  >>> s
6508  [x > 0]
6509  """
6510  Z3_solver_pop(self.ctx.ref(), self.solver, num)
6511 
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 6777 of file z3py.py.

6777  def proof(self):
6778  """Return a proof for the last `check()`. Proof construction must be enabled."""
6779  return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
6780 
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 6468 of file z3py.py.

6468  def push(self):
6469  """Create a backtracking point.
6470 
6471  >>> x = Int('x')
6472  >>> s = Solver()
6473  >>> s.add(x > 0)
6474  >>> s
6475  [x > 0]
6476  >>> s.push()
6477  >>> s.add(x < 1)
6478  >>> s
6479  [x > 0, x < 1]
6480  >>> s.check()
6481  unsat
6482  >>> s.pop()
6483  >>> s.check()
6484  sat
6485  >>> s
6486  [x > 0]
6487  """
6488  Z3_solver_push(self.ctx.ref(), self.solver)
6489 
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 6836 of file z3py.py.

6836  def reason_unknown(self):
6837  """Return a string describing why the last `check()` returned `unknown`.
6838 
6839  >>> x = Int('x')
6840  >>> s = SimpleSolver()
6841  >>> s.add(2**x == 4)
6842  >>> s.check()
6843  unknown
6844  >>> s.reason_unknown()
6845  '(incomplete (theory arithmetic))'
6846  """
6847  return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver)
6848 
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 6530 of file z3py.py.

6530  def reset(self):
6531  """Remove all asserted constraints and backtracking points created using `push()`.
6532 
6533  >>> x = Int('x')
6534  >>> s = Solver()
6535  >>> s.add(x > 0)
6536  >>> s
6537  [x > 0]
6538  >>> s.reset()
6539  >>> s
6540  []
6541  """
6542  Z3_solver_reset(self.ctx.ref(), self.solver)
6543 
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 6456 of file z3py.py.

6456  def set(self, *args, **keys):
6457  """Set a configuration option. The method `help()` return a string containing all available options.
6458 
6459  >>> s = Solver()
6460  >>> # The option MBQI can be set using three different approaches.
6461  >>> s.set(mbqi=True)
6462  >>> s.set('MBQI', True)
6463  >>> s.set(':mbqi', True)
6464  """
6465  p = args2params(args, keys, self.ctx)
6466  Z3_solver_set_params(self.ctx.ref(), self.solver, p.params)
6467 
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:5070

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

6880  def sexpr(self):
6881  """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
6882 
6883  >>> x = Int('x')
6884  >>> s = Solver()
6885  >>> s.add(x > 0)
6886  >>> s.add(x < 2)
6887  >>> r = s.sexpr()
6888  """
6889  return Z3_solver_to_string(self.ctx.ref(), self.solver)
6890 
Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s)
Convert a solver into a string.

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

◆ statistics()

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

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

Definition at line 6818 of file z3py.py.

6818  def statistics(self):
6819  """Return statistics for the last `check()`.
6820 
6821  >>> s = SimpleSolver()
6822  >>> x = Int('x')
6823  >>> s.add(x > 0)
6824  >>> s.check()
6825  sat
6826  >>> st = s.statistics()
6827  >>> st.get_key_value('final checks')
6828  1
6829  >>> len(st) > 0
6830  True
6831  >>> st[0] != 0
6832  True
6833  """
6834  return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx)
6835 
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 6895 of file z3py.py.

6895  def to_smt2(self):
6896  """return SMTLIB2 formatted benchmark for solver's assertions"""
6897  es = self.assertions()
6898  sz = len(es)
6899  sz1 = sz
6900  if sz1 > 0:
6901  sz1 -= 1
6902  v = (Ast * sz1)()
6903  for i in range(sz1):
6904  v[i] = es[i].as_ast()
6905  if sz > 0:
6906  e = es[sz1].as_ast()
6907  else:
6908  e = BoolVal(True, self.ctx).as_ast()
6909  return Z3_benchmark_to_smtlib_string(self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e)
6910 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3431
def BoolVal(val, ctx=None)
Definition: z3py.py:1550
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 6813 of file z3py.py.

6813  def trail(self):
6814  """Return trail of the solver state after a check() call.
6815  """
6816  return AstVector(Z3_solver_get_trail(self.ctx.ref(), self.solver), self.ctx)
6817 
Z3_ast_vector Z3_API Z3_solver_get_trail(Z3_context c, Z3_solver s)
Return the trail modulo model conversion, in order of decision level The decision level can be retrie...

Referenced by Solver.trail_levels().

◆ trail_levels()

def trail_levels (   self)
Return trail and decision levels of the solver state after a check() call.

Definition at line 6805 of file z3py.py.

6805  def trail_levels(self):
6806  """Return trail and decision levels of the solver state after a check() call.
6807  """
6808  trail = self.trail()
6809  levels = (ctypes.c_uint * len(trail))()
6810  Z3_solver_get_levels(self.ctx.ref(), self.solver, trail.vector, len(trail), levels)
6811  return trail, levels
6812 
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 6861 of file z3py.py.

6861  def translate(self, target):
6862  """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
6863 
6864  >>> c1 = Context()
6865  >>> c2 = Context()
6866  >>> s1 = Solver(ctx=c1)
6867  >>> s2 = s1.translate(c2)
6868  """
6869  if z3_debug():
6870  _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
6871  solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref())
6872  return Solver(solver, target)
6873 
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:56

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

◆ units()

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

Definition at line 6795 of file z3py.py.

6795  def units(self):
6796  """Return an AST vector containing all currently inferred units.
6797  """
6798  return AstVector(Z3_solver_get_units(self.ctx.ref(), self.solver), self.ctx)
6799 
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 6681 of file z3py.py.

6681  def unsat_core(self):
6682  """Return a subset (as an AST vector) of the assumptions provided to the last check().
6683 
6684  These are the assumptions Z3 used in the unsatisfiability proof.
6685  Assumptions are available in Z3. They are used to extract unsatisfiable cores.
6686  They may be also used to "retract" assumptions. Note that, assumptions are not really
6687  "soft constraints", but they can be used to implement them.
6688 
6689  >>> p1, p2, p3 = Bools('p1 p2 p3')
6690  >>> x, y = Ints('x y')
6691  >>> s = Solver()
6692  >>> s.add(Implies(p1, x > 0))
6693  >>> s.add(Implies(p2, y > x))
6694  >>> s.add(Implies(p2, y < 1))
6695  >>> s.add(Implies(p3, y > -3))
6696  >>> s.check(p1, p2, p3)
6697  unsat
6698  >>> core = s.unsat_core()
6699  >>> len(core)
6700  2
6701  >>> p1 in core
6702  True
6703  >>> p2 in core
6704  True
6705  >>> p3 in core
6706  False
6707  >>> # "Retracting" p2
6708  >>> s.check(p1, p3)
6709  sat
6710  """
6711  return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx)
6712 
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 6442 of file z3py.py.

◆ ctx

ctx

Definition at line 6441 of file z3py.py.

Referenced by Probe.__call__(), Solver.__copy__(), Solver.__deepcopy__(), Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), Solver.__del__(), 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(), Solver.assert_and_track(), Optimize.assert_and_track(), Solver.assert_exprs(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Solver.assertions(), Optimize.assertions(), Solver.check(), Optimize.check(), Solver.consequences(), Solver.dimacs(), Solver.from_file(), Optimize.from_file(), Solver.from_string(), 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(), Solver.help(), Fixedpoint.help(), Optimize.help(), Tactic.help(), Solver.import_model_converter(), Optimize.maximize(), Optimize.minimize(), Solver.model(), Optimize.model(), Solver.non_units(), Solver.num_scopes(), Optimize.objectives(), Solver.param_descrs(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Solver.pop(), Optimize.pop(), Solver.proof(), Solver.push(), Optimize.push(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), Solver.reason_unknown(), Fixedpoint.reason_unknown(), Optimize.reason_unknown(), Fixedpoint.register_relation(), Solver.reset(), Solver.set(), Fixedpoint.set(), Optimize.set(), Fixedpoint.set_predicate_representation(), Solver.sexpr(), Fixedpoint.sexpr(), Optimize.sexpr(), ApplyResult.sexpr(), Tactic.solver(), Solver.statistics(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), Fixedpoint.to_string(), Solver.trail(), Solver.trail_levels(), Solver.translate(), Solver.units(), Solver.unsat_core(), Optimize.unsat_core(), and Fixedpoint.update_rule().

◆ cube_vs

cube_vs

Definition at line 6756 of file z3py.py.

Referenced by Solver.cube_vars().

◆ solver

solver