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

Constructor & Destructor Documentation

◆ __init__()

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

Definition at line 6866 of file z3py.py.

6866  def __init__(self, solver=None, ctx=None, logFile=None):
6867  assert solver is None or ctx is not None
6868  self.ctx = _get_ctx(ctx)
6869  self.backtrack_level = 4000000000
6870  self.solver = None
6871  if solver is None:
6872  self.solver = Z3_mk_solver(self.ctx.ref())
6873  else:
6874  self.solver = solver
6875  Z3_solver_inc_ref(self.ctx.ref(), self.solver)
6876  if logFile is not None:
6877  self.set("smtlib2_log", logFile)
6878 

◆ __del__()

def __del__ (   self)

Definition at line 6879 of file z3py.py.

6879  def __del__(self):
6880  if self.solver is not None and self.ctx.ref() is not None:
6881  Z3_solver_dec_ref(self.ctx.ref(), self.solver)
6882 

Member Function Documentation

◆ __copy__()

def __copy__ (   self)

Definition at line 7304 of file z3py.py.

7304  def __copy__(self):
7305  return self.translate(self.ctx)
7306 

◆ __deepcopy__()

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 7307 of file z3py.py.

7307  def __deepcopy__(self, memo={}):
7308  return self.translate(self.ctx)
7309 

◆ __iadd__()

def __iadd__ (   self,
  fml 
)

Definition at line 7002 of file z3py.py.

7002  def __iadd__(self, fml):
7003  self.add(fml)
7004  return self
7005 

◆ __repr__()

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

Definition at line 7287 of file z3py.py.

7287  def __repr__(self):
7288  """Return a formatted string with all added constraints."""
7289  return obj_to_string(self)
7290 

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

6991  def add(self, *args):
6992  """Assert constraints into the solver.
6993 
6994  >>> x = Int('x')
6995  >>> s = Solver()
6996  >>> s.add(x > 0, x < 2)
6997  >>> s
6998  [x > 0, x < 2]
6999  """
7000  self.assert_exprs(*args)
7001 

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

7006  def append(self, *args):
7007  """Assert constraints into the solver.
7008 
7009  >>> x = Int('x')
7010  >>> s = Solver()
7011  >>> s.append(x > 0, x < 2)
7012  >>> s
7013  [x > 0, x < 2]
7014  """
7015  self.assert_exprs(*args)
7016 

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

7028  def assert_and_track(self, a, p):
7029  """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
7030 
7031  If `p` is a string, it will be automatically converted into a Boolean constant.
7032 
7033  >>> x = Int('x')
7034  >>> p3 = Bool('p3')
7035  >>> s = Solver()
7036  >>> s.set(unsat_core=True)
7037  >>> s.assert_and_track(x > 0, 'p1')
7038  >>> s.assert_and_track(x != 1, 'p2')
7039  >>> s.assert_and_track(x < 0, p3)
7040  >>> print(s.check())
7041  unsat
7042  >>> c = s.unsat_core()
7043  >>> len(c)
7044  2
7045  >>> Bool('p1') in c
7046  True
7047  >>> Bool('p2') in c
7048  False
7049  >>> p3 in c
7050  True
7051  """
7052  if isinstance(p, str):
7053  p = Bool(p, self.ctx)
7054  _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
7055  _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
7056  Z3_solver_assert_and_track(self.ctx.ref(), self.solver, a.as_ast(), p.as_ast())
7057 

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

6972  def assert_exprs(self, *args):
6973  """Assert constraints into the solver.
6974 
6975  >>> x = Int('x')
6976  >>> s = Solver()
6977  >>> s.assert_exprs(x > 0, x < 2)
6978  >>> s
6979  [x > 0, x < 2]
6980  """
6981  args = _get_args(args)
6982  s = BoolSort(self.ctx)
6983  for arg in args:
6984  if isinstance(arg, Goal) or isinstance(arg, AstVector):
6985  for f in arg:
6986  Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast())
6987  else:
6988  arg = s.cast(arg)
6989  Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast())
6990 

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

7211  def assertions(self):
7212  """Return an AST vector containing all added constraints.
7213 
7214  >>> s = Solver()
7215  >>> s.assertions()
7216  []
7217  >>> a = Int('a')
7218  >>> s.add(a > 0)
7219  >>> s.add(a < 10)
7220  >>> s.assertions()
7221  [a > 0, a < 10]
7222  """
7223  return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
7224 

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

7058  def check(self, *assumptions):
7059  """Check whether the assertions in the given solver plus the optional assumptions are consistent or not.
7060 
7061  >>> x = Int('x')
7062  >>> s = Solver()
7063  >>> s.check()
7064  sat
7065  >>> s.add(x > 0, x < 2)
7066  >>> s.check()
7067  sat
7068  >>> s.model().eval(x)
7069  1
7070  >>> s.add(x < 1)
7071  >>> s.check()
7072  unsat
7073  >>> s.reset()
7074  >>> s.add(2**x == 4)
7075  >>> s.check()
7076  unknown
7077  """
7078  s = BoolSort(self.ctx)
7079  assumptions = _get_args(assumptions)
7080  num = len(assumptions)
7081  _assumptions = (Ast * num)()
7082  for i in range(num):
7083  _assumptions[i] = s.cast(assumptions[i]).as_ast()
7084  r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions)
7085  return CheckSatResult(r)
7086 

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

7142  def consequences(self, assumptions, variables):
7143  """Determine fixed values for the variables based on the solver state and assumptions.
7144  >>> s = Solver()
7145  >>> a, b, c, d = Bools('a b c d')
7146  >>> s.add(Implies(a,b), Implies(b, c))
7147  >>> s.consequences([a],[b,c,d])
7148  (sat, [Implies(a, b), Implies(a, c)])
7149  >>> s.consequences([Not(c),d],[a,b,c,d])
7150  (sat, [Implies(d, d), Implies(Not(c), Not(c)), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))])
7151  """
7152  if isinstance(assumptions, list):
7153  _asms = AstVector(None, self.ctx)
7154  for a in assumptions:
7155  _asms.push(a)
7156  assumptions = _asms
7157  if isinstance(variables, list):
7158  _vars = AstVector(None, self.ctx)
7159  for a in variables:
7160  _vars.push(a)
7161  variables = _vars
7162  _z3_assert(isinstance(assumptions, AstVector), "ast vector expected")
7163  _z3_assert(isinstance(variables, AstVector), "ast vector expected")
7164  consequences = AstVector(None, self.ctx)
7165  r = Z3_solver_get_consequences(self.ctx.ref(), self.solver, assumptions.vector,
7166  variables.vector, consequences.vector)
7167  sz = len(consequences)
7168  consequences = [consequences[i] for i in range(sz)]
7169  return CheckSatResult(r), consequences
7170 

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

7179  def cube(self, vars=None):
7180  """Get set of cubes
7181  The method takes an optional set of variables that restrict which
7182  variables may be used as a starting point for cubing.
7183  If vars is not None, then the first case split is based on a variable in
7184  this set.
7185  """
7186  self.cube_vs = AstVector(None, self.ctx)
7187  if vars is not None:
7188  for v in vars:
7189  self.cube_vs.push(v)
7190  while True:
7191  lvl = self.backtrack_level
7192  self.backtrack_level = 4000000000
7193  r = AstVector(Z3_solver_cube(self.ctx.ref(), self.solver, self.cube_vs.vector, lvl), self.ctx)
7194  if (len(r) == 1 and is_false(r[0])):
7195  return
7196  yield r
7197  if (len(r) == 0):
7198  return
7199 

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

7200  def cube_vars(self):
7201  """Access the set of variables that were touched by the most recently generated cube.
7202  This set of variables can be used as a starting point for additional cubes.
7203  The idea is that variables that appear in clauses that are reduced by the most recent
7204  cube are likely more useful to cube on."""
7205  return self.cube_vs
7206 

◆ dimacs()

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

Definition at line 7322 of file z3py.py.

7322  def dimacs(self, include_names=True):
7323  """Return a textual representation of the solver in DIMACS format."""
7324  return Z3_solver_to_dimacs_string(self.ctx.ref(), self.solver, include_names)
7325 

◆ from_file()

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

Definition at line 7171 of file z3py.py.

7171  def from_file(self, filename):
7172  """Parse assertions from a file"""
7173  Z3_solver_from_file(self.ctx.ref(), self.solver, filename)
7174 

◆ from_string()

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

Definition at line 7175 of file z3py.py.

7175  def from_string(self, s):
7176  """Parse assertions from a string"""
7177  Z3_solver_from_string(self.ctx.ref(), self.solver, s)
7178 

◆ help()

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

Definition at line 7279 of file z3py.py.

7279  def help(self):
7280  """Display a string describing all available options."""
7281  print(Z3_solver_get_help(self.ctx.ref(), self.solver))
7282 

◆ import_model_converter()

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

Definition at line 7106 of file z3py.py.

7106  def import_model_converter(self, other):
7107  """Import model converter from other into the current solver"""
7108  Z3_solver_import_model_converter(self.ctx.ref(), other.solver, self.solver)
7109 

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

7017  def insert(self, *args):
7018  """Assert constraints into the solver.
7019 
7020  >>> x = Int('x')
7021  >>> s = Solver()
7022  >>> s.insert(x > 0, x < 2)
7023  >>> s
7024  [x > 0, x < 2]
7025  """
7026  self.assert_exprs(*args)
7027 

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

7087  def model(self):
7088  """Return a model for the last `check()`.
7089 
7090  This function raises an exception if
7091  a model is not available (e.g., last `check()` returned unsat).
7092 
7093  >>> s = Solver()
7094  >>> a = Int('a')
7095  >>> s.add(a + 2 == 0)
7096  >>> s.check()
7097  sat
7098  >>> s.model()
7099  [a = -2]
7100  """
7101  try:
7102  return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx)
7103  except Z3Exception:
7104  raise Z3Exception("model is not available")
7105 

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

7230  def non_units(self):
7231  """Return an AST vector containing all atomic formulas in solver state that are not units.
7232  """
7233  return AstVector(Z3_solver_get_non_units(self.ctx.ref(), self.solver), self.ctx)
7234 

◆ num_scopes()

def num_scopes (   self)
Return the current number of backtracking points.

>>> s = Solver()
>>> s.num_scopes()
0
>>> s.push()
>>> s.num_scopes()
1
>>> s.push()
>>> s.num_scopes()
2
>>> s.pop()
>>> s.num_scopes()
1

Definition at line 6940 of file z3py.py.

6940  def num_scopes(self):
6941  """Return the current number of backtracking points.
6942 
6943  >>> s = Solver()
6944  >>> s.num_scopes()
6945  0
6946  >>> s.push()
6947  >>> s.num_scopes()
6948  1
6949  >>> s.push()
6950  >>> s.num_scopes()
6951  2
6952  >>> s.pop()
6953  >>> s.num_scopes()
6954  1
6955  """
6956  return Z3_solver_get_num_scopes(self.ctx.ref(), self.solver)
6957 

◆ param_descrs()

def param_descrs (   self)
Return the parameter description set.

Definition at line 7283 of file z3py.py.

7283  def param_descrs(self):
7284  """Return the parameter description set."""
7285  return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx)
7286 

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

6918  def pop(self, num=1):
6919  """Backtrack \\c num backtracking points.
6920 
6921  >>> x = Int('x')
6922  >>> s = Solver()
6923  >>> s.add(x > 0)
6924  >>> s
6925  [x > 0]
6926  >>> s.push()
6927  >>> s.add(x < 1)
6928  >>> s
6929  [x > 0, x < 1]
6930  >>> s.check()
6931  unsat
6932  >>> s.pop()
6933  >>> s.check()
6934  sat
6935  >>> s
6936  [x > 0]
6937  """
6938  Z3_solver_pop(self.ctx.ref(), self.solver, num)
6939 

◆ proof()

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

Definition at line 7207 of file z3py.py.

7207  def proof(self):
7208  """Return a proof for the last `check()`. Proof construction must be enabled."""
7209  return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
7210 

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

6896  def push(self):
6897  """Create a backtracking point.
6898 
6899  >>> x = Int('x')
6900  >>> s = Solver()
6901  >>> s.add(x > 0)
6902  >>> s
6903  [x > 0]
6904  >>> s.push()
6905  >>> s.add(x < 1)
6906  >>> s
6907  [x > 0, x < 1]
6908  >>> s.check()
6909  unsat
6910  >>> s.pop()
6911  >>> s.check()
6912  sat
6913  >>> s
6914  [x > 0]
6915  """
6916  Z3_solver_push(self.ctx.ref(), self.solver)
6917 

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

7266  def reason_unknown(self):
7267  """Return a string describing why the last `check()` returned `unknown`.
7268 
7269  >>> x = Int('x')
7270  >>> s = SimpleSolver()
7271  >>> s.add(2**x == 4)
7272  >>> s.check()
7273  unknown
7274  >>> s.reason_unknown()
7275  '(incomplete (theory arithmetic))'
7276  """
7277  return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver)
7278 

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

6958  def reset(self):
6959  """Remove all asserted constraints and backtracking points created using `push()`.
6960 
6961  >>> x = Int('x')
6962  >>> s = Solver()
6963  >>> s.add(x > 0)
6964  >>> s
6965  [x > 0]
6966  >>> s.reset()
6967  >>> s
6968  []
6969  """
6970  Z3_solver_reset(self.ctx.ref(), self.solver)
6971 

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

6883  def set(self, *args, **keys):
6884  """Set a configuration option.
6885  The method `help()` return a string containing all available options.
6886 
6887  >>> s = Solver()
6888  >>> # The option MBQI can be set using three different approaches.
6889  >>> s.set(mbqi=True)
6890  >>> s.set('MBQI', True)
6891  >>> s.set(':mbqi', True)
6892  """
6893  p = args2params(args, keys, self.ctx)
6894  Z3_solver_set_params(self.ctx.ref(), self.solver, p.params)
6895 

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

7310  def sexpr(self):
7311  """Return a formatted string (in Lisp-like format) with all added constraints.
7312  We say the string is in s-expression format.
7313 
7314  >>> x = Int('x')
7315  >>> s = Solver()
7316  >>> s.add(x > 0)
7317  >>> s.add(x < 2)
7318  >>> r = s.sexpr()
7319  """
7320  return Z3_solver_to_string(self.ctx.ref(), self.solver)
7321 

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

7248  def statistics(self):
7249  """Return statistics for the last `check()`.
7250 
7251  >>> s = SimpleSolver()
7252  >>> x = Int('x')
7253  >>> s.add(x > 0)
7254  >>> s.check()
7255  sat
7256  >>> st = s.statistics()
7257  >>> st.get_key_value('final checks')
7258  1
7259  >>> len(st) > 0
7260  True
7261  >>> st[0] != 0
7262  True
7263  """
7264  return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx)
7265 

◆ to_smt2()

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

Definition at line 7326 of file z3py.py.

7326  def to_smt2(self):
7327  """return SMTLIB2 formatted benchmark for solver's assertions"""
7328  es = self.assertions()
7329  sz = len(es)
7330  sz1 = sz
7331  if sz1 > 0:
7332  sz1 -= 1
7333  v = (Ast * sz1)()
7334  for i in range(sz1):
7335  v[i] = es[i].as_ast()
7336  if sz > 0:
7337  e = es[sz1].as_ast()
7338  else:
7339  e = BoolVal(True, self.ctx).as_ast()
7341  self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e,
7342  )
7343 
7344 

◆ trail()

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

Definition at line 7243 of file z3py.py.

7243  def trail(self):
7244  """Return trail of the solver state after a check() call.
7245  """
7246  return AstVector(Z3_solver_get_trail(self.ctx.ref(), self.solver), self.ctx)
7247 

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

7235  def trail_levels(self):
7236  """Return trail and decision levels of the solver state after a check() call.
7237  """
7238  trail = self.trail()
7239  levels = (ctypes.c_uint * len(trail))()
7240  Z3_solver_get_levels(self.ctx.ref(), self.solver, trail.vector, len(trail), levels)
7241  return trail, levels
7242 

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

7291  def translate(self, target):
7292  """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
7293 
7294  >>> c1 = Context()
7295  >>> c2 = Context()
7296  >>> s1 = Solver(ctx=c1)
7297  >>> s2 = s1.translate(c2)
7298  """
7299  if z3_debug():
7300  _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
7301  solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref())
7302  return Solver(solver, target)
7303 

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

◆ units()

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

Definition at line 7225 of file z3py.py.

7225  def units(self):
7226  """Return an AST vector containing all currently inferred units.
7227  """
7228  return AstVector(Z3_solver_get_units(self.ctx.ref(), self.solver), self.ctx)
7229 

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

7110  def unsat_core(self):
7111  """Return a subset (as an AST vector) of the assumptions provided to the last check().
7112 
7113  These are the assumptions Z3 used in the unsatisfiability proof.
7114  Assumptions are available in Z3. They are used to extract unsatisfiable cores.
7115  They may be also used to "retract" assumptions. Note that, assumptions are not really
7116  "soft constraints", but they can be used to implement them.
7117 
7118  >>> p1, p2, p3 = Bools('p1 p2 p3')
7119  >>> x, y = Ints('x y')
7120  >>> s = Solver()
7121  >>> s.add(Implies(p1, x > 0))
7122  >>> s.add(Implies(p2, y > x))
7123  >>> s.add(Implies(p2, y < 1))
7124  >>> s.add(Implies(p3, y > -3))
7125  >>> s.check(p1, p2, p3)
7126  unsat
7127  >>> core = s.unsat_core()
7128  >>> len(core)
7129  2
7130  >>> p1 in core
7131  True
7132  >>> p2 in core
7133  True
7134  >>> p3 in core
7135  False
7136  >>> # "Retracting" p2
7137  >>> s.check(p1, p3)
7138  sat
7139  """
7140  return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx)
7141 

Field Documentation

◆ backtrack_level

backtrack_level

Definition at line 6869 of file z3py.py.

◆ ctx

ctx

Definition at line 6868 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(), Optimize.set_on_model(), 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 7186 of file z3py.py.

Referenced by Solver.cube_vars().

◆ solver

solver
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_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.UserPropagateBase.__init__
def __init__(self, s, ctx=None)
Definition: z3py.py:11351
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.
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_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_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_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::range
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3824
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_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.
z3py.UserPropagateBase.pop
def pop(self, num_scopes)
Definition: z3py.py:11417
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_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.push
def push(self)
Definition: z3py.py:11414
z3py.UserPropagateBase.__del__
def __del__(self)
Definition: z3py.py:11377
Z3_solver_reset
void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)
Remove all assertions from the solver.
z3py.is_const
def is_const(a)
Definition: z3py.py:1280
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.
Z3_solver_push
void Z3_API Z3_solver_push(Z3_context c, Z3_solver s)
Create a backtracking point.
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.
z3py.z3_debug
def z3_debug()
Definition: z3py.py:62
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_pop
void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n)
Backtrack n backtracking points.
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_inc_ref
void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s)
Increment the reference counter of the given solver.
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_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_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...
z3py.Bool
def Bool(name, ctx=None)
Definition: z3py.py:1713
z3py.BoolVal
def BoolVal(val, ctx=None)
Definition: z3py.py:1694
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.
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_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_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_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.
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_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.UserPropagateBase.add
def add(self, e)
Definition: z3py.py:11423
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_num_scopes
unsigned Z3_API Z3_solver_get_num_scopes(Z3_context c, Z3_solver s)
Return the number of backtracking points.
z3py.args2params
def args2params(arguments, keywords, ctx=None)
Definition: z3py.py:5447
z3py.is_false
def is_false(a)
Definition: z3py.py:1592
z3py.BoolSort
def BoolSort(ctx=None)
Definition: z3py.py:1676
Z3_solver_to_string
Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s)
Convert a solver into a string.