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

Constructor & Destructor Documentation

◆ __init__()

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

Definition at line 6363 of file z3py.py.

6363  def __init__(self, solver=None, ctx=None):
6364  assert solver is None or ctx is not None
6365  self.ctx = _get_ctx(ctx)
6366  self.backtrack_level = 4000000000
6367  self.solver = None
6368  if solver is None:
6369  self.solver = Z3_mk_solver(self.ctx.ref())
6370  else:
6371  self.solver = solver
6372  Z3_solver_inc_ref(self.ctx.ref(), self.solver)
6373 
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 6374 of file z3py.py.

6374  def __del__(self):
6375  if self.solver is not None and self.ctx.ref() is not None:
6376  Z3_solver_dec_ref(self.ctx.ref(), self.solver)
6377 
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 6785 of file z3py.py.

6785  def __copy__(self):
6786  return self.translate(self.ctx)
6787 

◆ __deepcopy__()

def __deepcopy__ (   self)

Definition at line 6788 of file z3py.py.

6788  def __deepcopy__(self):
6789  return self.translate(self.ctx)
6790 

◆ __iadd__()

def __iadd__ (   self,
  fml 
)

Definition at line 6496 of file z3py.py.

6496  def __iadd__(self, fml):
6497  self.add(fml)
6498  return self
6499 

◆ __repr__()

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

Definition at line 6768 of file z3py.py.

6768  def __repr__(self):
6769  """Return a formatted string with all added constraints."""
6770  return obj_to_string(self)
6771 

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

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

6485  def add(self, *args):
6486  """Assert constraints into the solver.
6487 
6488  >>> x = Int('x')
6489  >>> s = Solver()
6490  >>> s.add(x > 0, x < 2)
6491  >>> s
6492  [x > 0, x < 2]
6493  """
6494  self.assert_exprs(*args)
6495 

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

6500  def append(self, *args):
6501  """Assert constraints into the solver.
6502 
6503  >>> x = Int('x')
6504  >>> s = Solver()
6505  >>> s.append(x > 0, x < 2)
6506  >>> s
6507  [x > 0, x < 2]
6508  """
6509  self.assert_exprs(*args)
6510 

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

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

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

6466  def assert_exprs(self, *args):
6467  """Assert constraints into the solver.
6468 
6469  >>> x = Int('x')
6470  >>> s = Solver()
6471  >>> s.assert_exprs(x > 0, x < 2)
6472  >>> s
6473  [x > 0, x < 2]
6474  """
6475  args = _get_args(args)
6476  s = BoolSort(self.ctx)
6477  for arg in args:
6478  if isinstance(arg, Goal) or isinstance(arg, AstVector):
6479  for f in arg:
6480  Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast())
6481  else:
6482  arg = s.cast(arg)
6483  Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast())
6484 
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 6705 of file z3py.py.

Referenced by Solver.to_smt2().

6705  def assertions(self):
6706  """Return an AST vector containing all added constraints.
6707 
6708  >>> s = Solver()
6709  >>> s.assertions()
6710  []
6711  >>> a = Int('a')
6712  >>> s.add(a > 0)
6713  >>> s.add(a < 10)
6714  >>> s.assertions()
6715  [a > 0, a < 10]
6716  """
6717  return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
6718 
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 6552 of file z3py.py.

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

6552  def check(self, *assumptions):
6553  """Check whether the assertions in the given solver plus the optional assumptions are consistent or not.
6554 
6555  >>> x = Int('x')
6556  >>> s = Solver()
6557  >>> s.check()
6558  sat
6559  >>> s.add(x > 0, x < 2)
6560  >>> s.check()
6561  sat
6562  >>> s.model().eval(x)
6563  1
6564  >>> s.add(x < 1)
6565  >>> s.check()
6566  unsat
6567  >>> s.reset()
6568  >>> s.add(2**x == 4)
6569  >>> s.check()
6570  unknown
6571  """
6572  assumptions = _get_args(assumptions)
6573  num = len(assumptions)
6574  _assumptions = (Ast * num)()
6575  for i in range(num):
6576  _assumptions[i] = assumptions[i].as_ast()
6577  r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions)
6578  return CheckSatResult(r)
6579 
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 6631 of file z3py.py.

6631  def consequences(self, assumptions, variables):
6632  """Determine fixed values for the variables based on the solver state and assumptions.
6633  >>> s = Solver()
6634  >>> a, b, c, d = Bools('a b c d')
6635  >>> s.add(Implies(a,b), Implies(b, c))
6636  >>> s.consequences([a],[b,c,d])
6637  (sat, [Implies(a, b), Implies(a, c)])
6638  >>> s.consequences([Not(c),d],[a,b,c,d])
6639  (sat, [Implies(d, d), Implies(Not(c), Not(c)), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))])
6640  """
6641  if isinstance(assumptions, list):
6642  _asms = AstVector(None, self.ctx)
6643  for a in assumptions:
6644  _asms.push(a)
6645  assumptions = _asms
6646  if isinstance(variables, list):
6647  _vars = AstVector(None, self.ctx)
6648  for a in variables:
6649  _vars.push(a)
6650  variables = _vars
6651  _z3_assert(isinstance(assumptions, AstVector), "ast vector expected")
6652  _z3_assert(isinstance(variables, AstVector), "ast vector expected")
6653  consequences = AstVector(None, self.ctx)
6654  r = Z3_solver_get_consequences(self.ctx.ref(), self.solver, assumptions.vector, variables.vector, consequences.vector)
6655  sz = len(consequences)
6656  consequences = [ consequences[i] for i in range(sz) ]
6657  return CheckSatResult(r), consequences
6658 
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 6673 of file z3py.py.

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

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

◆ from_file()

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

Definition at line 6659 of file z3py.py.

6659  def from_file(self, filename):
6660  """Parse assertions from a file"""
6661  try:
6662  Z3_solver_from_file(self.ctx.ref(), self.solver, filename)
6663  except Z3Exception as e:
6664  _handle_parse_error(e, self.ctx)
6665 
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 6666 of file z3py.py.

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

Referenced by Solver.set().

6760  def help(self):
6761  """Display a string describing all available options."""
6762  print(Z3_solver_get_help(self.ctx.ref(), self.solver))
6763 
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 6511 of file z3py.py.

6511  def insert(self, *args):
6512  """Assert constraints into the solver.
6513 
6514  >>> x = Int('x')
6515  >>> s = Solver()
6516  >>> s.insert(x > 0, x < 2)
6517  >>> s
6518  [x > 0, x < 2]
6519  """
6520  self.assert_exprs(*args)
6521 

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

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

6724  def non_units(self):
6725  """Return an AST vector containing all atomic formulas in solver state that are not units.
6726  """
6727  return AstVector(Z3_solver_get_non_units(self.ctx.ref(), self.solver), self.ctx)
6728 
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 6434 of file z3py.py.

6434  def num_scopes(self):
6435  """Return the current number of backtracking points.
6436 
6437  >>> s = Solver()
6438  >>> s.num_scopes()
6439  0L
6440  >>> s.push()
6441  >>> s.num_scopes()
6442  1L
6443  >>> s.push()
6444  >>> s.num_scopes()
6445  2L
6446  >>> s.pop()
6447  >>> s.num_scopes()
6448  1L
6449  """
6450  return Z3_solver_get_num_scopes(self.ctx.ref(), self.solver)
6451 
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 6764 of file z3py.py.

6764  def param_descrs(self):
6765  """Return the parameter description set."""
6766  return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx)
6767 
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 6412 of file z3py.py.

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

6701  def proof(self):
6702  """Return a proof for the last `check()`. Proof construction must be enabled."""
6703  return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
6704 
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 6390 of file z3py.py.

Referenced by Solver.reset().

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

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

6452  def reset(self):
6453  """Remove all asserted constraints and backtracking points created using `push()`.
6454 
6455  >>> x = Int('x')
6456  >>> s = Solver()
6457  >>> s.add(x > 0)
6458  >>> s
6459  [x > 0]
6460  >>> s.reset()
6461  >>> s
6462  []
6463  """
6464  Z3_solver_reset(self.ctx.ref(), self.solver)
6465 
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 6378 of file z3py.py.

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

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

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

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

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

6802  def to_smt2(self):
6803  """return SMTLIB2 formatted benchmark for solver's assertions"""
6804  es = self.assertions()
6805  sz = len(es)
6806  sz1 = sz
6807  if sz1 > 0:
6808  sz1 -= 1
6809  v = (Ast * sz1)()
6810  for i in range(sz1):
6811  v[i] = es[i].as_ast()
6812  if sz > 0:
6813  e = es[sz1].as_ast()
6814  else:
6815  e = BoolVal(True, self.ctx).as_ast()
6816  return Z3_benchmark_to_smtlib_string(self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e)
6817 
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 6772 of file z3py.py.

6772  def translate(self, target):
6773  """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
6774 
6775  >>> c1 = Context()
6776  >>> c2 = Context()
6777  >>> s1 = Solver(ctx=c1)
6778  >>> s2 = s1.translate(c2)
6779  """
6780  if __debug__:
6781  _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
6782  solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref())
6783  return Solver(solver, target)
6784 
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 6719 of file z3py.py.

6719  def units(self):
6720  """Return an AST vector containing all currently inferred units.
6721  """
6722  return AstVector(Z3_solver_get_units(self.ctx.ref(), self.solver), self.ctx)
6723 
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 6599 of file z3py.py.

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

◆ ctx

ctx

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

◆ solver

solver

Definition at line 6367 of file z3py.py.