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

Constructor & Destructor Documentation

◆ __init__()

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

Definition at line 6443 of file z3py.py.

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

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

6876  def __copy__(self):
6877  return self.translate(self.ctx)
6878 

◆ __deepcopy__()

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 6879 of file z3py.py.

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

◆ __iadd__()

def __iadd__ (   self,
  fml 
)

Definition at line 6576 of file z3py.py.

6576  def __iadd__(self, fml):
6577  self.add(fml)
6578  return self
6579 

◆ __repr__()

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

Definition at line 6859 of file z3py.py.

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

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

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

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

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

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

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

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

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

6783  def assertions(self):
6784  """Return an AST vector containing all added constraints.
6785 
6786  >>> s = Solver()
6787  >>> s.assertions()
6788  []
6789  >>> a = Int('a')
6790  >>> s.add(a > 0)
6791  >>> s.add(a < 10)
6792  >>> s.assertions()
6793  [a > 0, a < 10]
6794  """
6795  return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
6796 
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 6632 of file z3py.py.

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

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

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

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

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

◆ dimacs()

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

Definition at line 6893 of file z3py.py.

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

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

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

6851  def help(self):
6852  """Display a string describing all available options."""
6853  print(Z3_solver_get_help(self.ctx.ref(), self.solver))
6854 
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 6679 of file z3py.py.

6679  def import_model_converter(self, other):
6680  """Import model converter from other into the current solver"""
6681  Z3_solver_import_model_converter(self.ctx.ref(), other.solver, self.solver)
6682 
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 6591 of file z3py.py.

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

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

6660  def model(self):
6661  """Return a model for the last `check()`.
6662 
6663  This function raises an exception if
6664  a model is not available (e.g., last `check()` returned unsat).
6665 
6666  >>> s = Solver()
6667  >>> a = Int('a')
6668  >>> s.add(a + 2 == 0)
6669  >>> s.check()
6670  sat
6671  >>> s.model()
6672  [a = -2]
6673  """
6674  try:
6675  return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx)
6676  except Z3Exception:
6677  raise Z3Exception("model is not available")
6678 
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 6802 of file z3py.py.

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

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

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

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

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

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

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

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

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

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

6882  def sexpr(self):
6883  """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
6884 
6885  >>> x = Int('x')
6886  >>> s = Solver()
6887  >>> s.add(x > 0)
6888  >>> s.add(x < 2)
6889  >>> r = s.sexpr()
6890  """
6891  return Z3_solver_to_string(self.ctx.ref(), self.solver)
6892 
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 6820 of file z3py.py.

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

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

6815  def trail(self):
6816  """Return trail of the solver state after a check() call.
6817  """
6818  return AstVector(Z3_solver_get_trail(self.ctx.ref(), self.solver), self.ctx)
6819 
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 6807 of file z3py.py.

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

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

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

◆ units()

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

Definition at line 6797 of file z3py.py.

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

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

◆ ctx

ctx

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

Referenced by Solver.cube_vars().

◆ solver

solver