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

Public Member Functions

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

Constructor & Destructor Documentation

◆ __init__()

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

Definition at line 6480 of file z3py.py.

6480  def __init__(self, solver=None, ctx=None, logFile=None):
6481  assert solver is None or ctx is not None
6482  self.ctx = _get_ctx(ctx)
6483  self.backtrack_level = 4000000000
6484  self.solver = None
6485  if solver is None:
6486  self.solver = Z3_mk_solver(self.ctx.ref())
6487  else:
6488  self.solver = solver
6489  Z3_solver_inc_ref(self.ctx.ref(), self.solver)
6490  if logFile is not None:
6491  self.set("smtlib2_log", logFile)
6492 

◆ __del__()

def __del__ (   self)

Definition at line 6493 of file z3py.py.

6493  def __del__(self):
6494  if self.solver is not None and self.ctx.ref() is not None:
6495  Z3_solver_dec_ref(self.ctx.ref(), self.solver)
6496 

Member Function Documentation

◆ __copy__()

def __copy__ (   self)

Definition at line 6916 of file z3py.py.

6916  def __copy__(self):
6917  return self.translate(self.ctx)
6918 

◆ __deepcopy__()

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 6919 of file z3py.py.

6919  def __deepcopy__(self, memo={}):
6920  return self.translate(self.ctx)
6921 

◆ __iadd__()

def __iadd__ (   self,
  fml 
)

Definition at line 6615 of file z3py.py.

6615  def __iadd__(self, fml):
6616  self.add(fml)
6617  return self
6618 

◆ __repr__()

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

Definition at line 6899 of file z3py.py.

6899  def __repr__(self):
6900  """Return a formatted string with all added constraints."""
6901  return obj_to_string(self)
6902 

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

6604  def add(self, *args):
6605  """Assert constraints into the solver.
6606 
6607  >>> x = Int('x')
6608  >>> s = Solver()
6609  >>> s.add(x > 0, x < 2)
6610  >>> s
6611  [x > 0, x < 2]
6612  """
6613  self.assert_exprs(*args)
6614 

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

6619  def append(self, *args):
6620  """Assert constraints into the solver.
6621 
6622  >>> x = Int('x')
6623  >>> s = Solver()
6624  >>> s.append(x > 0, x < 2)
6625  >>> s
6626  [x > 0, x < 2]
6627  """
6628  self.assert_exprs(*args)
6629 

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

6641  def assert_and_track(self, a, p):
6642  """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
6643 
6644  If `p` is a string, it will be automatically converted into a Boolean constant.
6645 
6646  >>> x = Int('x')
6647  >>> p3 = Bool('p3')
6648  >>> s = Solver()
6649  >>> s.set(unsat_core=True)
6650  >>> s.assert_and_track(x > 0, 'p1')
6651  >>> s.assert_and_track(x != 1, 'p2')
6652  >>> s.assert_and_track(x < 0, p3)
6653  >>> print(s.check())
6654  unsat
6655  >>> c = s.unsat_core()
6656  >>> len(c)
6657  2
6658  >>> Bool('p1') in c
6659  True
6660  >>> Bool('p2') in c
6661  False
6662  >>> p3 in c
6663  True
6664  """
6665  if isinstance(p, str):
6666  p = Bool(p, self.ctx)
6667  _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
6668  _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
6669  Z3_solver_assert_and_track(self.ctx.ref(), self.solver, a.as_ast(), p.as_ast())
6670 

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

6585  def assert_exprs(self, *args):
6586  """Assert constraints into the solver.
6587 
6588  >>> x = Int('x')
6589  >>> s = Solver()
6590  >>> s.assert_exprs(x > 0, x < 2)
6591  >>> s
6592  [x > 0, x < 2]
6593  """
6594  args = _get_args(args)
6595  s = BoolSort(self.ctx)
6596  for arg in args:
6597  if isinstance(arg, Goal) or isinstance(arg, AstVector):
6598  for f in arg:
6599  Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast())
6600  else:
6601  arg = s.cast(arg)
6602  Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast())
6603 

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

6823  def assertions(self):
6824  """Return an AST vector containing all added constraints.
6825 
6826  >>> s = Solver()
6827  >>> s.assertions()
6828  []
6829  >>> a = Int('a')
6830  >>> s.add(a > 0)
6831  >>> s.add(a < 10)
6832  >>> s.assertions()
6833  [a > 0, a < 10]
6834  """
6835  return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
6836 

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

6671  def check(self, *assumptions):
6672  """Check whether the assertions in the given solver plus the optional assumptions are consistent or not.
6673 
6674  >>> x = Int('x')
6675  >>> s = Solver()
6676  >>> s.check()
6677  sat
6678  >>> s.add(x > 0, x < 2)
6679  >>> s.check()
6680  sat
6681  >>> s.model().eval(x)
6682  1
6683  >>> s.add(x < 1)
6684  >>> s.check()
6685  unsat
6686  >>> s.reset()
6687  >>> s.add(2**x == 4)
6688  >>> s.check()
6689  unknown
6690  """
6691  s = BoolSort(self.ctx)
6692  assumptions = _get_args(assumptions)
6693  num = len(assumptions)
6694  _assumptions = (Ast * num)()
6695  for i in range(num):
6696  _assumptions[i] = s.cast(assumptions[i]).as_ast()
6697  r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions)
6698  return CheckSatResult(r)
6699 

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

6755  def consequences(self, assumptions, variables):
6756  """Determine fixed values for the variables based on the solver state and assumptions.
6757  >>> s = Solver()
6758  >>> a, b, c, d = Bools('a b c d')
6759  >>> s.add(Implies(a,b), Implies(b, c))
6760  >>> s.consequences([a],[b,c,d])
6761  (sat, [Implies(a, b), Implies(a, c)])
6762  >>> s.consequences([Not(c),d],[a,b,c,d])
6763  (sat, [Implies(d, d), Implies(Not(c), Not(c)), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))])
6764  """
6765  if isinstance(assumptions, list):
6766  _asms = AstVector(None, self.ctx)
6767  for a in assumptions:
6768  _asms.push(a)
6769  assumptions = _asms
6770  if isinstance(variables, list):
6771  _vars = AstVector(None, self.ctx)
6772  for a in variables:
6773  _vars.push(a)
6774  variables = _vars
6775  _z3_assert(isinstance(assumptions, AstVector), "ast vector expected")
6776  _z3_assert(isinstance(variables, AstVector), "ast vector expected")
6777  consequences = AstVector(None, self.ctx)
6778  r = Z3_solver_get_consequences(self.ctx.ref(), self.solver, assumptions.vector, variables.vector, consequences.vector)
6779  sz = len(consequences)
6780  consequences = [ consequences[i] for i in range(sz) ]
6781  return CheckSatResult(r), consequences
6782 

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

6791  def cube(self, vars = None):
6792  """Get set of cubes
6793  The method takes an optional set of variables that restrict which
6794  variables may be used as a starting point for cubing.
6795  If vars is not None, then the first case split is based on a variable in
6796  this set.
6797  """
6798  self.cube_vs = AstVector(None, self.ctx)
6799  if vars is not None:
6800  for v in vars:
6801  self.cube_vs.push(v)
6802  while True:
6803  lvl = self.backtrack_level
6804  self.backtrack_level = 4000000000
6805  r = AstVector(Z3_solver_cube(self.ctx.ref(), self.solver, self.cube_vs.vector, lvl), self.ctx)
6806  if (len(r) == 1 and is_false(r[0])):
6807  return
6808  yield r
6809  if (len(r) == 0):
6810  return
6811 

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

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

◆ dimacs()

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

Definition at line 6933 of file z3py.py.

6933  def dimacs(self, include_names=True):
6934  """Return a textual representation of the solver in DIMACS format."""
6935  return Z3_solver_to_dimacs_string(self.ctx.ref(), self.solver, include_names)
6936 

◆ from_file()

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

Definition at line 6783 of file z3py.py.

6783  def from_file(self, filename):
6784  """Parse assertions from a file"""
6785  Z3_solver_from_file(self.ctx.ref(), self.solver, filename)
6786 

◆ from_string()

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

Definition at line 6787 of file z3py.py.

6787  def from_string(self, s):
6788  """Parse assertions from a string"""
6789  Z3_solver_from_string(self.ctx.ref(), self.solver, s)
6790 

◆ help()

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

Definition at line 6891 of file z3py.py.

6891  def help(self):
6892  """Display a string describing all available options."""
6893  print(Z3_solver_get_help(self.ctx.ref(), self.solver))
6894 

◆ import_model_converter()

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

Definition at line 6719 of file z3py.py.

6719  def import_model_converter(self, other):
6720  """Import model converter from other into the current solver"""
6721  Z3_solver_import_model_converter(self.ctx.ref(), other.solver, self.solver)
6722 

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

6630  def insert(self, *args):
6631  """Assert constraints into the solver.
6632 
6633  >>> x = Int('x')
6634  >>> s = Solver()
6635  >>> s.insert(x > 0, x < 2)
6636  >>> s
6637  [x > 0, x < 2]
6638  """
6639  self.assert_exprs(*args)
6640 

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

6700  def model(self):
6701  """Return a model for the last `check()`.
6702 
6703  This function raises an exception if
6704  a model is not available (e.g., last `check()` returned unsat).
6705 
6706  >>> s = Solver()
6707  >>> a = Int('a')
6708  >>> s.add(a + 2 == 0)
6709  >>> s.check()
6710  sat
6711  >>> s.model()
6712  [a = -2]
6713  """
6714  try:
6715  return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx)
6716  except Z3Exception:
6717  raise Z3Exception("model is not available")
6718 

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

6842  def non_units(self):
6843  """Return an AST vector containing all atomic formulas in solver state that are not units.
6844  """
6845  return AstVector(Z3_solver_get_non_units(self.ctx.ref(), self.solver), self.ctx)
6846 

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

6553  def num_scopes(self):
6554  """Return the current number of backtracking points.
6555 
6556  >>> s = Solver()
6557  >>> s.num_scopes()
6558  0L
6559  >>> s.push()
6560  >>> s.num_scopes()
6561  1L
6562  >>> s.push()
6563  >>> s.num_scopes()
6564  2L
6565  >>> s.pop()
6566  >>> s.num_scopes()
6567  1L
6568  """
6569  return Z3_solver_get_num_scopes(self.ctx.ref(), self.solver)
6570 

◆ param_descrs()

def param_descrs (   self)
Return the parameter description set.

Definition at line 6895 of file z3py.py.

6895  def param_descrs(self):
6896  """Return the parameter description set."""
6897  return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx)
6898 

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

6531  def pop(self, num=1):
6532  """Backtrack \c num backtracking points.
6533 
6534  >>> x = Int('x')
6535  >>> s = Solver()
6536  >>> s.add(x > 0)
6537  >>> s
6538  [x > 0]
6539  >>> s.push()
6540  >>> s.add(x < 1)
6541  >>> s
6542  [x > 0, x < 1]
6543  >>> s.check()
6544  unsat
6545  >>> s.pop()
6546  >>> s.check()
6547  sat
6548  >>> s
6549  [x > 0]
6550  """
6551  Z3_solver_pop(self.ctx.ref(), self.solver, num)
6552 

◆ proof()

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

Definition at line 6819 of file z3py.py.

6819  def proof(self):
6820  """Return a proof for the last `check()`. Proof construction must be enabled."""
6821  return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
6822 

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

6509  def push(self):
6510  """Create a backtracking point.
6511 
6512  >>> x = Int('x')
6513  >>> s = Solver()
6514  >>> s.add(x > 0)
6515  >>> s
6516  [x > 0]
6517  >>> s.push()
6518  >>> s.add(x < 1)
6519  >>> s
6520  [x > 0, x < 1]
6521  >>> s.check()
6522  unsat
6523  >>> s.pop()
6524  >>> s.check()
6525  sat
6526  >>> s
6527  [x > 0]
6528  """
6529  Z3_solver_push(self.ctx.ref(), self.solver)
6530 

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

6878  def reason_unknown(self):
6879  """Return a string describing why the last `check()` returned `unknown`.
6880 
6881  >>> x = Int('x')
6882  >>> s = SimpleSolver()
6883  >>> s.add(2**x == 4)
6884  >>> s.check()
6885  unknown
6886  >>> s.reason_unknown()
6887  '(incomplete (theory arithmetic))'
6888  """
6889  return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver)
6890 

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

6571  def reset(self):
6572  """Remove all asserted constraints and backtracking points created using `push()`.
6573 
6574  >>> x = Int('x')
6575  >>> s = Solver()
6576  >>> s.add(x > 0)
6577  >>> s
6578  [x > 0]
6579  >>> s.reset()
6580  >>> s
6581  []
6582  """
6583  Z3_solver_reset(self.ctx.ref(), self.solver)
6584 

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

6497  def set(self, *args, **keys):
6498  """Set a configuration option. The method `help()` return a string containing all available options.
6499 
6500  >>> s = Solver()
6501  >>> # The option MBQI can be set using three different approaches.
6502  >>> s.set(mbqi=True)
6503  >>> s.set('MBQI', True)
6504  >>> s.set(':mbqi', True)
6505  """
6506  p = args2params(args, keys, self.ctx)
6507  Z3_solver_set_params(self.ctx.ref(), self.solver, p.params)
6508 

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

6922  def sexpr(self):
6923  """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
6924 
6925  >>> x = Int('x')
6926  >>> s = Solver()
6927  >>> s.add(x > 0)
6928  >>> s.add(x < 2)
6929  >>> r = s.sexpr()
6930  """
6931  return Z3_solver_to_string(self.ctx.ref(), self.solver)
6932 

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

6860  def statistics(self):
6861  """Return statistics for the last `check()`.
6862 
6863  >>> s = SimpleSolver()
6864  >>> x = Int('x')
6865  >>> s.add(x > 0)
6866  >>> s.check()
6867  sat
6868  >>> st = s.statistics()
6869  >>> st.get_key_value('final checks')
6870  1
6871  >>> len(st) > 0
6872  True
6873  >>> st[0] != 0
6874  True
6875  """
6876  return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx)
6877 

◆ to_smt2()

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

Definition at line 6937 of file z3py.py.

6937  def to_smt2(self):
6938  """return SMTLIB2 formatted benchmark for solver's assertions"""
6939  es = self.assertions()
6940  sz = len(es)
6941  sz1 = sz
6942  if sz1 > 0:
6943  sz1 -= 1
6944  v = (Ast * sz1)()
6945  for i in range(sz1):
6946  v[i] = es[i].as_ast()
6947  if sz > 0:
6948  e = es[sz1].as_ast()
6949  else:
6950  e = BoolVal(True, self.ctx).as_ast()
6951  return Z3_benchmark_to_smtlib_string(self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e)
6952 

◆ trail()

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

Definition at line 6855 of file z3py.py.

6855  def trail(self):
6856  """Return trail of the solver state after a check() call.
6857  """
6858  return AstVector(Z3_solver_get_trail(self.ctx.ref(), self.solver), self.ctx)
6859 

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

6847  def trail_levels(self):
6848  """Return trail and decision levels of the solver state after a check() call.
6849  """
6850  trail = self.trail()
6851  levels = (ctypes.c_uint * len(trail))()
6852  Z3_solver_get_levels(self.ctx.ref(), self.solver, trail.vector, len(trail), levels)
6853  return trail, levels
6854 

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

6903  def translate(self, target):
6904  """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
6905 
6906  >>> c1 = Context()
6907  >>> c2 = Context()
6908  >>> s1 = Solver(ctx=c1)
6909  >>> s2 = s1.translate(c2)
6910  """
6911  if z3_debug():
6912  _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
6913  solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref())
6914  return Solver(solver, target)
6915 

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

◆ units()

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

Definition at line 6837 of file z3py.py.

6837  def units(self):
6838  """Return an AST vector containing all currently inferred units.
6839  """
6840  return AstVector(Z3_solver_get_units(self.ctx.ref(), self.solver), self.ctx)
6841 

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

6723  def unsat_core(self):
6724  """Return a subset (as an AST vector) of the assumptions provided to the last check().
6725 
6726  These are the assumptions Z3 used in the unsatisfiability proof.
6727  Assumptions are available in Z3. They are used to extract unsatisfiable cores.
6728  They may be also used to "retract" assumptions. Note that, assumptions are not really
6729  "soft constraints", but they can be used to implement them.
6730 
6731  >>> p1, p2, p3 = Bools('p1 p2 p3')
6732  >>> x, y = Ints('x y')
6733  >>> s = Solver()
6734  >>> s.add(Implies(p1, x > 0))
6735  >>> s.add(Implies(p2, y > x))
6736  >>> s.add(Implies(p2, y < 1))
6737  >>> s.add(Implies(p3, y > -3))
6738  >>> s.check(p1, p2, p3)
6739  unsat
6740  >>> core = s.unsat_core()
6741  >>> len(core)
6742  2
6743  >>> p1 in core
6744  True
6745  >>> p2 in core
6746  True
6747  >>> p3 in core
6748  False
6749  >>> # "Retracting" p2
6750  >>> s.check(p1, p3)
6751  sat
6752  """
6753  return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx)
6754 

Field Documentation

◆ backtrack_level

backtrack_level

Definition at line 6483 of file z3py.py.

◆ ctx

ctx

Definition at line 6482 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(), UserPropagateBase.conflict(), Solver.consequences(), UserPropagateBase.ctx_ref(), 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 6798 of file z3py.py.

Referenced by Solver.cube_vars().

◆ solver

solver
Z3_solver_import_model_converter
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.
z3py.UserPropagateBase.__init__
def __init__(self, s, ctx=None)
Definition: z3py.py:10582
Z3_solver_to_string
Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s)
Convert a solver into a string.
Z3_solver_get_levels
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...
Z3_solver_reset
void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)
Remove all assertions from the solver.
Z3_solver_get_proof
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.
z3::range
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3515
Z3_solver_get_reason_unknown
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...
Z3_solver_pop
void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n)
Backtrack n backtracking points.
Z3_solver_check_assumptions
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.
z3py.UserPropagateBase.pop
def pop(self, num_scopes)
Definition: z3py.py:10647
Z3_solver_push
void Z3_API Z3_solver_push(Z3_context c, Z3_solver s)
Create a backtracking point.
z3py.UserPropagateBase.push
def push(self)
Definition: z3py.py:10644
Z3_solver_get_assertions
Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s)
Return the set of asserted formulas on the solver.
z3py.UserPropagateBase.__del__
def __del__(self)
Definition: z3py.py:10607
Z3_solver_to_dimacs_string
Z3_string Z3_API Z3_solver_to_dimacs_string(Z3_context c, Z3_solver s, bool include_names)
Convert a solver into a DIMACS formatted string.
Z3_solver_get_param_descrs
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.
z3py.is_const
def is_const(a)
Definition: z3py.py:1182
Z3_solver_get_num_scopes
unsigned Z3_API Z3_solver_get_num_scopes(Z3_context c, Z3_solver s)
Return the number of backtracking points.
Z3_solver_get_trail
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...
Z3_solver_dec_ref
void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s)
Decrement the reference counter of the given solver.
z3py.z3_debug
def z3_debug()
Definition: z3py.py:56
Z3_solver_from_string
void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string file_name)
load solver assertions from a string.
Z3_solver_get_unsat_core
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...
Z3_solver_get_units
Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s)
Return the set of units modulo model conversion.
Z3_solver_assert_and_track
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.
Z3_solver_get_statistics
Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s)
Return statistics for the given solver.
Z3_solver_set_params
void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p)
Set the given solver using the given parameters.
Z3_solver_get_non_units
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.
Z3_solver_cube
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...
z3py.Bool
def Bool(name, ctx=None)
Definition: z3py.py:1588
Z3_solver_assert
void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a)
Assert a constraint into the solver.
Z3_solver_translate
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.
z3py.BoolVal
def BoolVal(val, ctx=None)
Definition: z3py.py:1570
Z3_mk_solver
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 ...
Z3_solver_from_file
void Z3_API Z3_solver_from_file(Z3_context c, Z3_solver s, Z3_string file_name)
load solver assertions from a file.
Z3_solver_get_help
Z3_string Z3_API Z3_solver_get_help(Z3_context c, Z3_solver s)
Return a string describing all solver available parameters.
z3py.UserPropagateBase.add
def add(self, e)
Definition: z3py.py:10653
Z3_solver_get_consequences
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.
z3py.args2params
def args2params(arguments, keywords, ctx=None)
Definition: z3py.py:5111
z3py.is_false
def is_false(a)
Definition: z3py.py:1476
Z3_benchmark_to_smtlib_string
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.
z3py.BoolSort
def BoolSort(ctx=None)
Definition: z3py.py:1553
Z3_solver_get_model
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.
Z3_solver_inc_ref
void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s)
Increment the reference counter of the given solver.