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

Constructor & Destructor Documentation

◆ __init__()

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

Definition at line 6462 of file z3py.py.

6462  def __init__(self, solver=None, ctx=None, logFile=None):
6463  assert solver is None or ctx is not None
6464  self.ctx = _get_ctx(ctx)
6465  self.backtrack_level = 4000000000
6466  self.solver = None
6467  if solver is None:
6468  self.solver = Z3_mk_solver(self.ctx.ref())
6469  else:
6470  self.solver = solver
6471  Z3_solver_inc_ref(self.ctx.ref(), self.solver)
6472  if logFile is not None:
6473  self.set("solver.smtlib2_log", logFile)
6474 

◆ __del__()

def __del__ (   self)

Definition at line 6475 of file z3py.py.

6475  def __del__(self):
6476  if self.solver is not None and self.ctx.ref() is not None:
6477  Z3_solver_dec_ref(self.ctx.ref(), self.solver)
6478 

Member Function Documentation

◆ __copy__()

def __copy__ (   self)

Definition at line 6897 of file z3py.py.

6897  def __copy__(self):
6898  return self.translate(self.ctx)
6899 

◆ __deepcopy__()

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 6900 of file z3py.py.

6900  def __deepcopy__(self, memo={}):
6901  return self.translate(self.ctx)
6902 

◆ __iadd__()

def __iadd__ (   self,
  fml 
)

Definition at line 6597 of file z3py.py.

6597  def __iadd__(self, fml):
6598  self.add(fml)
6599  return self
6600 

◆ __repr__()

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

Definition at line 6880 of file z3py.py.

6880  def __repr__(self):
6881  """Return a formatted string with all added constraints."""
6882  return obj_to_string(self)
6883 

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

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

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

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

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

6623  def assert_and_track(self, a, p):
6624  """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
6625 
6626  If `p` is a string, it will be automatically converted into a Boolean constant.
6627 
6628  >>> x = Int('x')
6629  >>> p3 = Bool('p3')
6630  >>> s = Solver()
6631  >>> s.set(unsat_core=True)
6632  >>> s.assert_and_track(x > 0, 'p1')
6633  >>> s.assert_and_track(x != 1, 'p2')
6634  >>> s.assert_and_track(x < 0, p3)
6635  >>> print(s.check())
6636  unsat
6637  >>> c = s.unsat_core()
6638  >>> len(c)
6639  2
6640  >>> Bool('p1') in c
6641  True
6642  >>> Bool('p2') in c
6643  False
6644  >>> p3 in c
6645  True
6646  """
6647  if isinstance(p, str):
6648  p = Bool(p, self.ctx)
6649  _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
6650  _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
6651  Z3_solver_assert_and_track(self.ctx.ref(), self.solver, a.as_ast(), p.as_ast())
6652 

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

6567  def assert_exprs(self, *args):
6568  """Assert constraints into the solver.
6569 
6570  >>> x = Int('x')
6571  >>> s = Solver()
6572  >>> s.assert_exprs(x > 0, x < 2)
6573  >>> s
6574  [x > 0, x < 2]
6575  """
6576  args = _get_args(args)
6577  s = BoolSort(self.ctx)
6578  for arg in args:
6579  if isinstance(arg, Goal) or isinstance(arg, AstVector):
6580  for f in arg:
6581  Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast())
6582  else:
6583  arg = s.cast(arg)
6584  Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast())
6585 

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

6804  def assertions(self):
6805  """Return an AST vector containing all added constraints.
6806 
6807  >>> s = Solver()
6808  >>> s.assertions()
6809  []
6810  >>> a = Int('a')
6811  >>> s.add(a > 0)
6812  >>> s.add(a < 10)
6813  >>> s.assertions()
6814  [a > 0, a < 10]
6815  """
6816  return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
6817 

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

6653  def check(self, *assumptions):
6654  """Check whether the assertions in the given solver plus the optional assumptions are consistent or not.
6655 
6656  >>> x = Int('x')
6657  >>> s = Solver()
6658  >>> s.check()
6659  sat
6660  >>> s.add(x > 0, x < 2)
6661  >>> s.check()
6662  sat
6663  >>> s.model().eval(x)
6664  1
6665  >>> s.add(x < 1)
6666  >>> s.check()
6667  unsat
6668  >>> s.reset()
6669  >>> s.add(2**x == 4)
6670  >>> s.check()
6671  unknown
6672  """
6673  assumptions = _get_args(assumptions)
6674  num = len(assumptions)
6675  _assumptions = (Ast * num)()
6676  for i in range(num):
6677  _assumptions[i] = assumptions[i].as_ast()
6678  r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions)
6679  return CheckSatResult(r)
6680 

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

6736  def consequences(self, assumptions, variables):
6737  """Determine fixed values for the variables based on the solver state and assumptions.
6738  >>> s = Solver()
6739  >>> a, b, c, d = Bools('a b c d')
6740  >>> s.add(Implies(a,b), Implies(b, c))
6741  >>> s.consequences([a],[b,c,d])
6742  (sat, [Implies(a, b), Implies(a, c)])
6743  >>> s.consequences([Not(c),d],[a,b,c,d])
6744  (sat, [Implies(d, d), Implies(Not(c), Not(c)), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))])
6745  """
6746  if isinstance(assumptions, list):
6747  _asms = AstVector(None, self.ctx)
6748  for a in assumptions:
6749  _asms.push(a)
6750  assumptions = _asms
6751  if isinstance(variables, list):
6752  _vars = AstVector(None, self.ctx)
6753  for a in variables:
6754  _vars.push(a)
6755  variables = _vars
6756  _z3_assert(isinstance(assumptions, AstVector), "ast vector expected")
6757  _z3_assert(isinstance(variables, AstVector), "ast vector expected")
6758  consequences = AstVector(None, self.ctx)
6759  r = Z3_solver_get_consequences(self.ctx.ref(), self.solver, assumptions.vector, variables.vector, consequences.vector)
6760  sz = len(consequences)
6761  consequences = [ consequences[i] for i in range(sz) ]
6762  return CheckSatResult(r), consequences
6763 

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

6772  def cube(self, vars = None):
6773  """Get set of cubes
6774  The method takes an optional set of variables that restrict which
6775  variables may be used as a starting point for cubing.
6776  If vars is not None, then the first case split is based on a variable in
6777  this set.
6778  """
6779  self.cube_vs = AstVector(None, self.ctx)
6780  if vars is not None:
6781  for v in vars:
6782  self.cube_vs.push(v)
6783  while True:
6784  lvl = self.backtrack_level
6785  self.backtrack_level = 4000000000
6786  r = AstVector(Z3_solver_cube(self.ctx.ref(), self.solver, self.cube_vs.vector, lvl), self.ctx)
6787  if (len(r) == 1 and is_false(r[0])):
6788  return
6789  yield r
6790  if (len(r) == 0):
6791  return
6792 

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

6793  def cube_vars(self):
6794  """Access the set of variables that were touched by the most recently generated cube.
6795  This set of variables can be used as a starting point for additional cubes.
6796  The idea is that variables that appear in clauses that are reduced by the most recent
6797  cube are likely more useful to cube on."""
6798  return self.cube_vs
6799 

◆ dimacs()

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

Definition at line 6914 of file z3py.py.

6914  def dimacs(self, include_names=True):
6915  """Return a textual representation of the solver in DIMACS format."""
6916  return Z3_solver_to_dimacs_string(self.ctx.ref(), self.solver, include_names)
6917 

◆ from_file()

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

Definition at line 6764 of file z3py.py.

6764  def from_file(self, filename):
6765  """Parse assertions from a file"""
6766  Z3_solver_from_file(self.ctx.ref(), self.solver, filename)
6767 

◆ from_string()

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

Definition at line 6768 of file z3py.py.

6768  def from_string(self, s):
6769  """Parse assertions from a string"""
6770  Z3_solver_from_string(self.ctx.ref(), self.solver, s)
6771 

◆ help()

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

Definition at line 6872 of file z3py.py.

6872  def help(self):
6873  """Display a string describing all available options."""
6874  print(Z3_solver_get_help(self.ctx.ref(), self.solver))
6875 

◆ import_model_converter()

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

Definition at line 6700 of file z3py.py.

6700  def import_model_converter(self, other):
6701  """Import model converter from other into the current solver"""
6702  Z3_solver_import_model_converter(self.ctx.ref(), other.solver, self.solver)
6703 

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

6612  def insert(self, *args):
6613  """Assert constraints into the solver.
6614 
6615  >>> x = Int('x')
6616  >>> s = Solver()
6617  >>> s.insert(x > 0, x < 2)
6618  >>> s
6619  [x > 0, x < 2]
6620  """
6621  self.assert_exprs(*args)
6622 

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

6681  def model(self):
6682  """Return a model for the last `check()`.
6683 
6684  This function raises an exception if
6685  a model is not available (e.g., last `check()` returned unsat).
6686 
6687  >>> s = Solver()
6688  >>> a = Int('a')
6689  >>> s.add(a + 2 == 0)
6690  >>> s.check()
6691  sat
6692  >>> s.model()
6693  [a = -2]
6694  """
6695  try:
6696  return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx)
6697  except Z3Exception:
6698  raise Z3Exception("model is not available")
6699 

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

6823  def non_units(self):
6824  """Return an AST vector containing all atomic formulas in solver state that are not units.
6825  """
6826  return AstVector(Z3_solver_get_non_units(self.ctx.ref(), self.solver), self.ctx)
6827 

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

6535  def num_scopes(self):
6536  """Return the current number of backtracking points.
6537 
6538  >>> s = Solver()
6539  >>> s.num_scopes()
6540  0L
6541  >>> s.push()
6542  >>> s.num_scopes()
6543  1L
6544  >>> s.push()
6545  >>> s.num_scopes()
6546  2L
6547  >>> s.pop()
6548  >>> s.num_scopes()
6549  1L
6550  """
6551  return Z3_solver_get_num_scopes(self.ctx.ref(), self.solver)
6552 

◆ param_descrs()

def param_descrs (   self)
Return the parameter description set.

Definition at line 6876 of file z3py.py.

6876  def param_descrs(self):
6877  """Return the parameter description set."""
6878  return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx)
6879 

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

6513  def pop(self, num=1):
6514  """Backtrack \c num backtracking points.
6515 
6516  >>> x = Int('x')
6517  >>> s = Solver()
6518  >>> s.add(x > 0)
6519  >>> s
6520  [x > 0]
6521  >>> s.push()
6522  >>> s.add(x < 1)
6523  >>> s
6524  [x > 0, x < 1]
6525  >>> s.check()
6526  unsat
6527  >>> s.pop()
6528  >>> s.check()
6529  sat
6530  >>> s
6531  [x > 0]
6532  """
6533  Z3_solver_pop(self.ctx.ref(), self.solver, num)
6534 

◆ proof()

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

Definition at line 6800 of file z3py.py.

6800  def proof(self):
6801  """Return a proof for the last `check()`. Proof construction must be enabled."""
6802  return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
6803 

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

6491  def push(self):
6492  """Create a backtracking point.
6493 
6494  >>> x = Int('x')
6495  >>> s = Solver()
6496  >>> s.add(x > 0)
6497  >>> s
6498  [x > 0]
6499  >>> s.push()
6500  >>> s.add(x < 1)
6501  >>> s
6502  [x > 0, x < 1]
6503  >>> s.check()
6504  unsat
6505  >>> s.pop()
6506  >>> s.check()
6507  sat
6508  >>> s
6509  [x > 0]
6510  """
6511  Z3_solver_push(self.ctx.ref(), self.solver)
6512 

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

6859  def reason_unknown(self):
6860  """Return a string describing why the last `check()` returned `unknown`.
6861 
6862  >>> x = Int('x')
6863  >>> s = SimpleSolver()
6864  >>> s.add(2**x == 4)
6865  >>> s.check()
6866  unknown
6867  >>> s.reason_unknown()
6868  '(incomplete (theory arithmetic))'
6869  """
6870  return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver)
6871 

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

6553  def reset(self):
6554  """Remove all asserted constraints and backtracking points created using `push()`.
6555 
6556  >>> x = Int('x')
6557  >>> s = Solver()
6558  >>> s.add(x > 0)
6559  >>> s
6560  [x > 0]
6561  >>> s.reset()
6562  >>> s
6563  []
6564  """
6565  Z3_solver_reset(self.ctx.ref(), self.solver)
6566 

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

6479  def set(self, *args, **keys):
6480  """Set a configuration option. The method `help()` return a string containing all available options.
6481 
6482  >>> s = Solver()
6483  >>> # The option MBQI can be set using three different approaches.
6484  >>> s.set(mbqi=True)
6485  >>> s.set('MBQI', True)
6486  >>> s.set(':mbqi', True)
6487  """
6488  p = args2params(args, keys, self.ctx)
6489  Z3_solver_set_params(self.ctx.ref(), self.solver, p.params)
6490 

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

6903  def sexpr(self):
6904  """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
6905 
6906  >>> x = Int('x')
6907  >>> s = Solver()
6908  >>> s.add(x > 0)
6909  >>> s.add(x < 2)
6910  >>> r = s.sexpr()
6911  """
6912  return Z3_solver_to_string(self.ctx.ref(), self.solver)
6913 

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

6841  def statistics(self):
6842  """Return statistics for the last `check()`.
6843 
6844  >>> s = SimpleSolver()
6845  >>> x = Int('x')
6846  >>> s.add(x > 0)
6847  >>> s.check()
6848  sat
6849  >>> st = s.statistics()
6850  >>> st.get_key_value('final checks')
6851  1
6852  >>> len(st) > 0
6853  True
6854  >>> st[0] != 0
6855  True
6856  """
6857  return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx)
6858 

◆ to_smt2()

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

Definition at line 6918 of file z3py.py.

6918  def to_smt2(self):
6919  """return SMTLIB2 formatted benchmark for solver's assertions"""
6920  es = self.assertions()
6921  sz = len(es)
6922  sz1 = sz
6923  if sz1 > 0:
6924  sz1 -= 1
6925  v = (Ast * sz1)()
6926  for i in range(sz1):
6927  v[i] = es[i].as_ast()
6928  if sz > 0:
6929  e = es[sz1].as_ast()
6930  else:
6931  e = BoolVal(True, self.ctx).as_ast()
6932  return Z3_benchmark_to_smtlib_string(self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e)
6933 

◆ trail()

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

Definition at line 6836 of file z3py.py.

6836  def trail(self):
6837  """Return trail of the solver state after a check() call.
6838  """
6839  return AstVector(Z3_solver_get_trail(self.ctx.ref(), self.solver), self.ctx)
6840 

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

6828  def trail_levels(self):
6829  """Return trail and decision levels of the solver state after a check() call.
6830  """
6831  trail = self.trail()
6832  levels = (ctypes.c_uint * len(trail))()
6833  Z3_solver_get_levels(self.ctx.ref(), self.solver, trail.vector, len(trail), levels)
6834  return trail, levels
6835 

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

6884  def translate(self, target):
6885  """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
6886 
6887  >>> c1 = Context()
6888  >>> c2 = Context()
6889  >>> s1 = Solver(ctx=c1)
6890  >>> s2 = s1.translate(c2)
6891  """
6892  if z3_debug():
6893  _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
6894  solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref())
6895  return Solver(solver, target)
6896 

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

◆ units()

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

Definition at line 6818 of file z3py.py.

6818  def units(self):
6819  """Return an AST vector containing all currently inferred units.
6820  """
6821  return AstVector(Z3_solver_get_units(self.ctx.ref(), self.solver), self.ctx)
6822 

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

6704  def unsat_core(self):
6705  """Return a subset (as an AST vector) of the assumptions provided to the last check().
6706 
6707  These are the assumptions Z3 used in the unsatisfiability proof.
6708  Assumptions are available in Z3. They are used to extract unsatisfiable cores.
6709  They may be also used to "retract" assumptions. Note that, assumptions are not really
6710  "soft constraints", but they can be used to implement them.
6711 
6712  >>> p1, p2, p3 = Bools('p1 p2 p3')
6713  >>> x, y = Ints('x y')
6714  >>> s = Solver()
6715  >>> s.add(Implies(p1, x > 0))
6716  >>> s.add(Implies(p2, y > x))
6717  >>> s.add(Implies(p2, y < 1))
6718  >>> s.add(Implies(p3, y > -3))
6719  >>> s.check(p1, p2, p3)
6720  unsat
6721  >>> core = s.unsat_core()
6722  >>> len(core)
6723  2
6724  >>> p1 in core
6725  True
6726  >>> p2 in core
6727  True
6728  >>> p3 in core
6729  False
6730  >>> # "Retracting" p2
6731  >>> s.check(p1, p3)
6732  sat
6733  """
6734  return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx)
6735 

Field Documentation

◆ backtrack_level

backtrack_level

Definition at line 6465 of file z3py.py.

◆ ctx

ctx

Definition at line 6464 of file z3py.py.

Referenced by Probe.__call__(), Solver.__copy__(), Solver.__deepcopy__(), Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), Solver.__del__(), Fixedpoint.__del__(), Optimize.__del__(), ApplyResult.__del__(), Tactic.__del__(), Probe.__del__(), Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), ApplyResult.__len__(), Probe.__lt__(), Probe.__ne__(), Fixedpoint.add_cover(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), ApplyResult.as_expr(), Solver.assert_and_track(), Optimize.assert_and_track(), Solver.assert_exprs(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Solver.assertions(), Optimize.assertions(), Solver.check(), Optimize.check(), Solver.consequences(), Solver.dimacs(), Solver.from_file(), Optimize.from_file(), Solver.from_string(), Optimize.from_string(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_ground_sat_answer(), Fixedpoint.get_num_levels(), Fixedpoint.get_rule_names_along_trace(), Fixedpoint.get_rules(), Fixedpoint.get_rules_along_trace(), Solver.help(), Fixedpoint.help(), Optimize.help(), Tactic.help(), Solver.import_model_converter(), Optimize.maximize(), Optimize.minimize(), Solver.model(), Optimize.model(), Solver.non_units(), Solver.num_scopes(), Optimize.objectives(), Solver.param_descrs(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Optimize.pop(), Solver.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 6779 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.
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:3488
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.
Z3_solver_push
void Z3_API Z3_solver_push(Z3_context c, Z3_solver s)
Create a backtracking point.
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.
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.
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:5093
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.