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 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)
 
def sexpr (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 6366 of file z3py.py.

Constructor & Destructor Documentation

◆ __init__()

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

Definition at line 6369 of file z3py.py.

6369  def __init__(self, solver=None, ctx=None):
6370  assert solver is None or ctx is not None
6371  self.ctx = _get_ctx(ctx)
6372  self.backtrack_level = 4000000000
6373  self.solver = None
6374  if solver is None:
6375  self.solver = Z3_mk_solver(self.ctx.ref())
6376  else:
6377  self.solver = solver
6378  Z3_solver_inc_ref(self.ctx.ref(), self.solver)
6379 
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 6380 of file z3py.py.

6380  def __del__(self):
6381  if self.solver is not None and self.ctx.ref() is not None:
6382  Z3_solver_dec_ref(self.ctx.ref(), self.solver)
6383 
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 6791 of file z3py.py.

6791  def __copy__(self):
6792  return self.translate(self.ctx)
6793 

◆ __deepcopy__()

def __deepcopy__ (   self)

Definition at line 6794 of file z3py.py.

6794  def __deepcopy__(self):
6795  return self.translate(self.ctx)
6796 

◆ __iadd__()

def __iadd__ (   self,
  fml 
)

Definition at line 6502 of file z3py.py.

6502  def __iadd__(self, fml):
6503  self.add(fml)
6504  return self
6505 

◆ __repr__()

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

Definition at line 6774 of file z3py.py.

6774  def __repr__(self):
6775  """Return a formatted string with all added constraints."""
6776  return obj_to_string(self)
6777 

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

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

6491  def add(self, *args):
6492  """Assert constraints into the solver.
6493 
6494  >>> x = Int('x')
6495  >>> s = Solver()
6496  >>> s.add(x > 0, x < 2)
6497  >>> s
6498  [x > 0, x < 2]
6499  """
6500  self.assert_exprs(*args)
6501 

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

6506  def append(self, *args):
6507  """Assert constraints into the solver.
6508 
6509  >>> x = Int('x')
6510  >>> s = Solver()
6511  >>> s.append(x > 0, x < 2)
6512  >>> s
6513  [x > 0, x < 2]
6514  """
6515  self.assert_exprs(*args)
6516 

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

6528  def assert_and_track(self, a, p):
6529  """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
6530 
6531  If `p` is a string, it will be automatically converted into a Boolean constant.
6532 
6533  >>> x = Int('x')
6534  >>> p3 = Bool('p3')
6535  >>> s = Solver()
6536  >>> s.set(unsat_core=True)
6537  >>> s.assert_and_track(x > 0, 'p1')
6538  >>> s.assert_and_track(x != 1, 'p2')
6539  >>> s.assert_and_track(x < 0, p3)
6540  >>> print(s.check())
6541  unsat
6542  >>> c = s.unsat_core()
6543  >>> len(c)
6544  2
6545  >>> Bool('p1') in c
6546  True
6547  >>> Bool('p2') in c
6548  False
6549  >>> p3 in c
6550  True
6551  """
6552  if isinstance(p, str):
6553  p = Bool(p, self.ctx)
6554  _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
6555  _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
6556  Z3_solver_assert_and_track(self.ctx.ref(), self.solver, a.as_ast(), p.as_ast())
6557 
def is_const(a)
Definition: z3py.py:1141
def Bool(name, ctx=None)
Definition: z3py.py:1547
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 6472 of file z3py.py.

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

6472  def assert_exprs(self, *args):
6473  """Assert constraints into the solver.
6474 
6475  >>> x = Int('x')
6476  >>> s = Solver()
6477  >>> s.assert_exprs(x > 0, x < 2)
6478  >>> s
6479  [x > 0, x < 2]
6480  """
6481  args = _get_args(args)
6482  s = BoolSort(self.ctx)
6483  for arg in args:
6484  if isinstance(arg, Goal) or isinstance(arg, AstVector):
6485  for f in arg:
6486  Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast())
6487  else:
6488  arg = s.cast(arg)
6489  Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast())
6490 
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:1512

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

Referenced by Solver.to_smt2().

6711  def assertions(self):
6712  """Return an AST vector containing all added constraints.
6713 
6714  >>> s = Solver()
6715  >>> s.assertions()
6716  []
6717  >>> a = Int('a')
6718  >>> s.add(a > 0)
6719  >>> s.add(a < 10)
6720  >>> s.assertions()
6721  [a > 0, a < 10]
6722  """
6723  return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
6724 
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 6558 of file z3py.py.

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

6558  def check(self, *assumptions):
6559  """Check whether the assertions in the given solver plus the optional assumptions are consistent or not.
6560 
6561  >>> x = Int('x')
6562  >>> s = Solver()
6563  >>> s.check()
6564  sat
6565  >>> s.add(x > 0, x < 2)
6566  >>> s.check()
6567  sat
6568  >>> s.model().eval(x)
6569  1
6570  >>> s.add(x < 1)
6571  >>> s.check()
6572  unsat
6573  >>> s.reset()
6574  >>> s.add(2**x == 4)
6575  >>> s.check()
6576  unknown
6577  """
6578  assumptions = _get_args(assumptions)
6579  num = len(assumptions)
6580  _assumptions = (Ast * num)()
6581  for i in range(num):
6582  _assumptions[i] = assumptions[i].as_ast()
6583  r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions)
6584  return CheckSatResult(r)
6585 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3244
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 6637 of file z3py.py.

6637  def consequences(self, assumptions, variables):
6638  """Determine fixed values for the variables based on the solver state and assumptions.
6639  >>> s = Solver()
6640  >>> a, b, c, d = Bools('a b c d')
6641  >>> s.add(Implies(a,b), Implies(b, c))
6642  >>> s.consequences([a],[b,c,d])
6643  (sat, [Implies(a, b), Implies(a, c)])
6644  >>> s.consequences([Not(c),d],[a,b,c,d])
6645  (sat, [Implies(d, d), Implies(Not(c), Not(c)), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))])
6646  """
6647  if isinstance(assumptions, list):
6648  _asms = AstVector(None, self.ctx)
6649  for a in assumptions:
6650  _asms.push(a)
6651  assumptions = _asms
6652  if isinstance(variables, list):
6653  _vars = AstVector(None, self.ctx)
6654  for a in variables:
6655  _vars.push(a)
6656  variables = _vars
6657  _z3_assert(isinstance(assumptions, AstVector), "ast vector expected")
6658  _z3_assert(isinstance(variables, AstVector), "ast vector expected")
6659  consequences = AstVector(None, self.ctx)
6660  r = Z3_solver_get_consequences(self.ctx.ref(), self.solver, assumptions.vector, variables.vector, consequences.vector)
6661  sz = len(consequences)
6662  consequences = [ consequences[i] for i in range(sz) ]
6663  return CheckSatResult(r), consequences
6664 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3244
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 6679 of file z3py.py.

6679  def cube(self, vars = None):
6680  """Get set of cubes
6681  The method takes an optional set of variables that restrict which
6682  variables may be used as a starting point for cubing.
6683  If vars is not None, then the first case split is based on a variable in
6684  this set.
6685  """
6686  self.cube_vs = AstVector(None, self.ctx)
6687  if vars is not None:
6688  for v in vars:
6689  self.cube_vs.push(v)
6690  while True:
6691  lvl = self.backtrack_level
6692  self.backtrack_level = 4000000000
6693  r = AstVector(Z3_solver_cube(self.ctx.ref(), self.solver, self.cube_vs.vector, lvl), self.ctx)
6694  if (len(r) == 1 and is_false(r[0])):
6695  return
6696  yield r
6697  if (len(r) == 0):
6698  return
6699 
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:1435

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

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

◆ from_file()

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

Definition at line 6665 of file z3py.py.

6665  def from_file(self, filename):
6666  """Parse assertions from a file"""
6667  try:
6668  Z3_solver_from_file(self.ctx.ref(), self.solver, filename)
6669  except Z3Exception as e:
6670  _handle_parse_error(e, self.ctx)
6671 
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 6672 of file z3py.py.

6672  def from_string(self, s):
6673  """Parse assertions from a string"""
6674  try:
6675  Z3_solver_from_string(self.ctx.ref(), self.solver, s)
6676  except Z3Exception as e:
6677  _handle_parse_error(e, self.ctx)
6678 
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 6766 of file z3py.py.

Referenced by Solver.set().

6766  def help(self):
6767  """Display a string describing all available options."""
6768  print(Z3_solver_get_help(self.ctx.ref(), self.solver))
6769 
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 6517 of file z3py.py.

6517  def insert(self, *args):
6518  """Assert constraints into the solver.
6519 
6520  >>> x = Int('x')
6521  >>> s = Solver()
6522  >>> s.insert(x > 0, x < 2)
6523  >>> s
6524  [x > 0, x < 2]
6525  """
6526  self.assert_exprs(*args)
6527 

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

6586  def model(self):
6587  """Return a model for the last `check()`.
6588 
6589  This function raises an exception if
6590  a model is not available (e.g., last `check()` returned unsat).
6591 
6592  >>> s = Solver()
6593  >>> a = Int('a')
6594  >>> s.add(a + 2 == 0)
6595  >>> s.check()
6596  sat
6597  >>> s.model()
6598  [a = -2]
6599  """
6600  try:
6601  return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx)
6602  except Z3Exception:
6603  raise Z3Exception("model is not available")
6604 
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 6730 of file z3py.py.

6730  def non_units(self):
6731  """Return an AST vector containing all atomic formulas in solver state that are not units.
6732  """
6733  return AstVector(Z3_solver_get_non_units(self.ctx.ref(), self.solver), self.ctx)
6734 
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 6440 of file z3py.py.

6440  def num_scopes(self):
6441  """Return the current number of backtracking points.
6442 
6443  >>> s = Solver()
6444  >>> s.num_scopes()
6445  0L
6446  >>> s.push()
6447  >>> s.num_scopes()
6448  1L
6449  >>> s.push()
6450  >>> s.num_scopes()
6451  2L
6452  >>> s.pop()
6453  >>> s.num_scopes()
6454  1L
6455  """
6456  return Z3_solver_get_num_scopes(self.ctx.ref(), self.solver)
6457 
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 6770 of file z3py.py.

6770  def param_descrs(self):
6771  """Return the parameter description set."""
6772  return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx)
6773 
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 6418 of file z3py.py.

6418  def pop(self, num=1):
6419  """Backtrack \c num backtracking points.
6420 
6421  >>> x = Int('x')
6422  >>> s = Solver()
6423  >>> s.add(x > 0)
6424  >>> s
6425  [x > 0]
6426  >>> s.push()
6427  >>> s.add(x < 1)
6428  >>> s
6429  [x > 0, x < 1]
6430  >>> s.check()
6431  unsat
6432  >>> s.pop()
6433  >>> s.check()
6434  sat
6435  >>> s
6436  [x > 0]
6437  """
6438  Z3_solver_pop(self.ctx.ref(), self.solver, num)
6439 
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 6707 of file z3py.py.

6707  def proof(self):
6708  """Return a proof for the last `check()`. Proof construction must be enabled."""
6709  return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
6710 
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 6396 of file z3py.py.

Referenced by Solver.reset().

6396  def push(self):
6397  """Create a backtracking point.
6398 
6399  >>> x = Int('x')
6400  >>> s = Solver()
6401  >>> s.add(x > 0)
6402  >>> s
6403  [x > 0]
6404  >>> s.push()
6405  >>> s.add(x < 1)
6406  >>> s
6407  [x > 0, x < 1]
6408  >>> s.check()
6409  unsat
6410  >>> s.pop()
6411  >>> s.check()
6412  sat
6413  >>> s
6414  [x > 0]
6415  """
6416  Z3_solver_push(self.ctx.ref(), self.solver)
6417 
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 6753 of file z3py.py.

6753  def reason_unknown(self):
6754  """Return a string describing why the last `check()` returned `unknown`.
6755 
6756  >>> x = Int('x')
6757  >>> s = SimpleSolver()
6758  >>> s.add(2**x == 4)
6759  >>> s.check()
6760  unknown
6761  >>> s.reason_unknown()
6762  '(incomplete (theory arithmetic))'
6763  """
6764  return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver)
6765 
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 6458 of file z3py.py.

6458  def reset(self):
6459  """Remove all asserted constraints and backtracking points created using `push()`.
6460 
6461  >>> x = Int('x')
6462  >>> s = Solver()
6463  >>> s.add(x > 0)
6464  >>> s
6465  [x > 0]
6466  >>> s.reset()
6467  >>> s
6468  []
6469  """
6470  Z3_solver_reset(self.ctx.ref(), self.solver)
6471 
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 6384 of file z3py.py.

6384  def set(self, *args, **keys):
6385  """Set a configuration option. The method `help()` return a string containing all available options.
6386 
6387  >>> s = Solver()
6388  >>> # The option MBQI can be set using three different approaches.
6389  >>> s.set(mbqi=True)
6390  >>> s.set('MBQI', True)
6391  >>> s.set(':mbqi', True)
6392  """
6393  p = args2params(args, keys, self.ctx)
6394  Z3_solver_set_params(self.ctx.ref(), self.solver, p.params)
6395 
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:5007

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

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

6797  def sexpr(self):
6798  """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
6799 
6800  >>> x = Int('x')
6801  >>> s = Solver()
6802  >>> s.add(x > 0)
6803  >>> s.add(x < 2)
6804  >>> r = s.sexpr()
6805  """
6806  return Z3_solver_to_string(self.ctx.ref(), self.solver)
6807 
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 6735 of file z3py.py.

6735  def statistics(self):
6736  """Return statistics for the last `check()`.
6737 
6738  >>> s = SimpleSolver()
6739  >>> x = Int('x')
6740  >>> s.add(x > 0)
6741  >>> s.check()
6742  sat
6743  >>> st = s.statistics()
6744  >>> st.get_key_value('final checks')
6745  1
6746  >>> len(st) > 0
6747  True
6748  >>> st[0] != 0
6749  True
6750  """
6751  return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx)
6752 
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 6808 of file z3py.py.

6808  def to_smt2(self):
6809  """return SMTLIB2 formatted benchmark for solver's assertions"""
6810  es = self.assertions()
6811  sz = len(es)
6812  sz1 = sz
6813  if sz1 > 0:
6814  sz1 -= 1
6815  v = (Ast * sz1)()
6816  for i in range(sz1):
6817  v[i] = es[i].as_ast()
6818  if sz > 0:
6819  e = es[sz1].as_ast()
6820  else:
6821  e = BoolVal(True, self.ctx).as_ast()
6822  return Z3_benchmark_to_smtlib_string(self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e)
6823 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3244
def BoolVal(val, ctx=None)
Definition: z3py.py:1529
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.

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

6778  def translate(self, target):
6779  """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
6780 
6781  >>> c1 = Context()
6782  >>> c2 = Context()
6783  >>> s1 = Solver(ctx=c1)
6784  >>> s2 = s1.translate(c2)
6785  """
6786  if __debug__:
6787  _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
6788  solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref())
6789  return Solver(solver, target)
6790 
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.

◆ units()

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

Definition at line 6725 of file z3py.py.

6725  def units(self):
6726  """Return an AST vector containing all currently inferred units.
6727  """
6728  return AstVector(Z3_solver_get_units(self.ctx.ref(), self.solver), self.ctx)
6729 
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 6605 of file z3py.py.

6605  def unsat_core(self):
6606  """Return a subset (as an AST vector) of the assumptions provided to the last check().
6607 
6608  These are the assumptions Z3 used in the unsatisfiability proof.
6609  Assumptions are available in Z3. They are used to extract unsatisfiable cores.
6610  They may be also used to "retract" assumptions. Note that, assumptions are not really
6611  "soft constraints", but they can be used to implement them.
6612 
6613  >>> p1, p2, p3 = Bools('p1 p2 p3')
6614  >>> x, y = Ints('x y')
6615  >>> s = Solver()
6616  >>> s.add(Implies(p1, x > 0))
6617  >>> s.add(Implies(p2, y > x))
6618  >>> s.add(Implies(p2, y < 1))
6619  >>> s.add(Implies(p3, y > -3))
6620  >>> s.check(p1, p2, p3)
6621  unsat
6622  >>> core = s.unsat_core()
6623  >>> len(core)
6624  2
6625  >>> p1 in core
6626  True
6627  >>> p2 in core
6628  True
6629  >>> p3 in core
6630  False
6631  >>> # "Retracting" p2
6632  >>> s.check(p1, p3)
6633  sat
6634  """
6635  return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx)
6636 
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 6372 of file z3py.py.

◆ ctx

ctx

Definition at line 6371 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(), 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(), Fixedpoint.pop(), Optimize.pop(), Fixedpoint.push(), 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 6686 of file z3py.py.

◆ solver

solver

Definition at line 6373 of file z3py.py.