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

Constructor & Destructor Documentation

◆ __init__()

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

Definition at line 6828 of file z3py.py.

6828  def __init__(self, solver=None, ctx=None, logFile=None):
6829  assert solver is None or ctx is not None
6830  self.ctx = _get_ctx(ctx)
6831  self.backtrack_level = 4000000000
6832  self.solver = None
6833  if solver is None:
6834  self.solver = Z3_mk_solver(self.ctx.ref())
6835  else:
6836  self.solver = solver
6837  Z3_solver_inc_ref(self.ctx.ref(), self.solver)
6838  if logFile is not None:
6839  self.set("smtlib2_log", logFile)
6840 
Z3_solver Z3_API Z3_mk_solver(Z3_context c)
Create a new solver. This solver is a "combined solver" (see combined_solver module) that internally ...
void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s)
Increment the reference counter of the given solver.

◆ __del__()

def __del__ (   self)

Definition at line 6841 of file z3py.py.

6841  def __del__(self):
6842  if self.solver is not None and self.ctx.ref() is not None:
6843  Z3_solver_dec_ref(self.ctx.ref(), self.solver)
6844 
void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s)
Decrement the reference counter of the given solver.

Member Function Documentation

◆ __copy__()

def __copy__ (   self)

Definition at line 7266 of file z3py.py.

7266  def __copy__(self):
7267  return self.translate(self.ctx)
7268 

◆ __deepcopy__()

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 7269 of file z3py.py.

7269  def __deepcopy__(self, memo={}):
7270  return self.translate(self.ctx)
7271 

◆ __iadd__()

def __iadd__ (   self,
  fml 
)

Definition at line 6964 of file z3py.py.

6964  def __iadd__(self, fml):
6965  self.add(fml)
6966  return self
6967 

◆ __repr__()

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

Definition at line 7249 of file z3py.py.

7249  def __repr__(self):
7250  """Return a formatted string with all added constraints."""
7251  return obj_to_string(self)
7252 

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

6953  def add(self, *args):
6954  """Assert constraints into the solver.
6955 
6956  >>> x = Int('x')
6957  >>> s = Solver()
6958  >>> s.add(x > 0, x < 2)
6959  >>> s
6960  [x > 0, x < 2]
6961  """
6962  self.assert_exprs(*args)
6963 

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

6968  def append(self, *args):
6969  """Assert constraints into the solver.
6970 
6971  >>> x = Int('x')
6972  >>> s = Solver()
6973  >>> s.append(x > 0, x < 2)
6974  >>> s
6975  [x > 0, x < 2]
6976  """
6977  self.assert_exprs(*args)
6978 

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

6990  def assert_and_track(self, a, p):
6991  """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
6992 
6993  If `p` is a string, it will be automatically converted into a Boolean constant.
6994 
6995  >>> x = Int('x')
6996  >>> p3 = Bool('p3')
6997  >>> s = Solver()
6998  >>> s.set(unsat_core=True)
6999  >>> s.assert_and_track(x > 0, 'p1')
7000  >>> s.assert_and_track(x != 1, 'p2')
7001  >>> s.assert_and_track(x < 0, p3)
7002  >>> print(s.check())
7003  unsat
7004  >>> c = s.unsat_core()
7005  >>> len(c)
7006  2
7007  >>> Bool('p1') in c
7008  True
7009  >>> Bool('p2') in c
7010  False
7011  >>> p3 in c
7012  True
7013  """
7014  if isinstance(p, str):
7015  p = Bool(p, self.ctx)
7016  _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
7017  _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
7018  Z3_solver_assert_and_track(self.ctx.ref(), self.solver, a.as_ast(), p.as_ast())
7019 
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.
def is_const(a)
Definition: z3py.py:1258
def Bool(name, ctx=None)
Definition: z3py.py:1691

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

6934  def assert_exprs(self, *args):
6935  """Assert constraints into the solver.
6936 
6937  >>> x = Int('x')
6938  >>> s = Solver()
6939  >>> s.assert_exprs(x > 0, x < 2)
6940  >>> s
6941  [x > 0, x < 2]
6942  """
6943  args = _get_args(args)
6944  s = BoolSort(self.ctx)
6945  for arg in args:
6946  if isinstance(arg, Goal) or isinstance(arg, AstVector):
6947  for f in arg:
6948  Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast())
6949  else:
6950  arg = s.cast(arg)
6951  Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast())
6952 
void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a)
Assert a constraint into the solver.
def BoolSort(ctx=None)
Definition: z3py.py:1654

Referenced by Goal.add(), Solver.add(), Fixedpoint.add(), Optimize.add(), Goal.append(), Solver.append(), Fixedpoint.append(), Goal.insert(), 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 7173 of file z3py.py.

7173  def assertions(self):
7174  """Return an AST vector containing all added constraints.
7175 
7176  >>> s = Solver()
7177  >>> s.assertions()
7178  []
7179  >>> a = Int('a')
7180  >>> s.add(a > 0)
7181  >>> s.add(a < 10)
7182  >>> s.assertions()
7183  [a > 0, a < 10]
7184  """
7185  return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
7186 
Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s)
Return the set of asserted formulas on the solver.

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

7020  def check(self, *assumptions):
7021  """Check whether the assertions in the given solver plus the optional assumptions are consistent or not.
7022 
7023  >>> x = Int('x')
7024  >>> s = Solver()
7025  >>> s.check()
7026  sat
7027  >>> s.add(x > 0, x < 2)
7028  >>> s.check()
7029  sat
7030  >>> s.model().eval(x)
7031  1
7032  >>> s.add(x < 1)
7033  >>> s.check()
7034  unsat
7035  >>> s.reset()
7036  >>> s.add(2**x == 4)
7037  >>> s.check()
7038  unknown
7039  """
7040  s = BoolSort(self.ctx)
7041  assumptions = _get_args(assumptions)
7042  num = len(assumptions)
7043  _assumptions = (Ast * num)()
7044  for i in range(num):
7045  _assumptions[i] = s.cast(assumptions[i]).as_ast()
7046  r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions)
7047  return CheckSatResult(r)
7048 
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.
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3823

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

7104  def consequences(self, assumptions, variables):
7105  """Determine fixed values for the variables based on the solver state and assumptions.
7106  >>> s = Solver()
7107  >>> a, b, c, d = Bools('a b c d')
7108  >>> s.add(Implies(a,b), Implies(b, c))
7109  >>> s.consequences([a],[b,c,d])
7110  (sat, [Implies(a, b), Implies(a, c)])
7111  >>> s.consequences([Not(c),d],[a,b,c,d])
7112  (sat, [Implies(d, d), Implies(Not(c), Not(c)), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))])
7113  """
7114  if isinstance(assumptions, list):
7115  _asms = AstVector(None, self.ctx)
7116  for a in assumptions:
7117  _asms.push(a)
7118  assumptions = _asms
7119  if isinstance(variables, list):
7120  _vars = AstVector(None, self.ctx)
7121  for a in variables:
7122  _vars.push(a)
7123  variables = _vars
7124  _z3_assert(isinstance(assumptions, AstVector), "ast vector expected")
7125  _z3_assert(isinstance(variables, AstVector), "ast vector expected")
7126  consequences = AstVector(None, self.ctx)
7127  r = Z3_solver_get_consequences(self.ctx.ref(), self.solver, assumptions.vector,
7128  variables.vector, consequences.vector)
7129  sz = len(consequences)
7130  consequences = [consequences[i] for i in range(sz)]
7131  return CheckSatResult(r), consequences
7132 
Z3_lbool Z3_API Z3_solver_get_consequences(Z3_context c, Z3_solver s, Z3_ast_vector assumptions, Z3_ast_vector variables, Z3_ast_vector consequences)
retrieve consequences from solver that determine values of the supplied function symbols.

◆ cube()

def cube (   self,
  vars = None 
)
Get set of cubes
The method takes an optional set of variables that restrict which
variables may be used as a starting point for cubing.
If vars is not None, then the first case split is based on a variable in
this set.

Definition at line 7141 of file z3py.py.

7141  def cube(self, vars=None):
7142  """Get set of cubes
7143  The method takes an optional set of variables that restrict which
7144  variables may be used as a starting point for cubing.
7145  If vars is not None, then the first case split is based on a variable in
7146  this set.
7147  """
7148  self.cube_vs = AstVector(None, self.ctx)
7149  if vars is not None:
7150  for v in vars:
7151  self.cube_vs.push(v)
7152  while True:
7153  lvl = self.backtrack_level
7154  self.backtrack_level = 4000000000
7155  r = AstVector(Z3_solver_cube(self.ctx.ref(), self.solver, self.cube_vs.vector, lvl), self.ctx)
7156  if (len(r) == 1 and is_false(r[0])):
7157  return
7158  yield r
7159  if (len(r) == 0):
7160  return
7161 
Z3_ast_vector Z3_API Z3_solver_cube(Z3_context c, Z3_solver s, Z3_ast_vector vars, unsigned backtrack_level)
extract a next cube for a solver. The last cube is the constant true or false. The number of (non-con...
def is_false(a)
Definition: z3py.py:1570

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

7162  def cube_vars(self):
7163  """Access the set of variables that were touched by the most recently generated cube.
7164  This set of variables can be used as a starting point for additional cubes.
7165  The idea is that variables that appear in clauses that are reduced by the most recent
7166  cube are likely more useful to cube on."""
7167  return self.cube_vs
7168 

◆ dimacs()

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

Definition at line 7284 of file z3py.py.

7284  def dimacs(self, include_names=True):
7285  """Return a textual representation of the solver in DIMACS format."""
7286  return Z3_solver_to_dimacs_string(self.ctx.ref(), self.solver, include_names)
7287 
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.

◆ from_file()

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

Definition at line 7133 of file z3py.py.

7133  def from_file(self, filename):
7134  """Parse assertions from a file"""
7135  Z3_solver_from_file(self.ctx.ref(), self.solver, filename)
7136 
void Z3_API Z3_solver_from_file(Z3_context c, Z3_solver s, Z3_string file_name)
load solver assertions from a file.

◆ from_string()

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

Definition at line 7137 of file z3py.py.

7137  def from_string(self, s):
7138  """Parse assertions from a string"""
7139  Z3_solver_from_string(self.ctx.ref(), self.solver, s)
7140 
void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string file_name)
load solver assertions from a string.

◆ help()

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

Definition at line 7241 of file z3py.py.

7241  def help(self):
7242  """Display a string describing all available options."""
7243  print(Z3_solver_get_help(self.ctx.ref(), self.solver))
7244 
Z3_string Z3_API Z3_solver_get_help(Z3_context c, Z3_solver s)
Return a string describing all solver available parameters.

◆ import_model_converter()

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

Definition at line 7068 of file z3py.py.

7068  def import_model_converter(self, other):
7069  """Import model converter from other into the current solver"""
7070  Z3_solver_import_model_converter(self.ctx.ref(), other.solver, self.solver)
7071 
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.

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

6979  def insert(self, *args):
6980  """Assert constraints into the solver.
6981 
6982  >>> x = Int('x')
6983  >>> s = Solver()
6984  >>> s.insert(x > 0, x < 2)
6985  >>> s
6986  [x > 0, x < 2]
6987  """
6988  self.assert_exprs(*args)
6989 

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

7049  def model(self):
7050  """Return a model for the last `check()`.
7051 
7052  This function raises an exception if
7053  a model is not available (e.g., last `check()` returned unsat).
7054 
7055  >>> s = Solver()
7056  >>> a = Int('a')
7057  >>> s.add(a + 2 == 0)
7058  >>> s.check()
7059  sat
7060  >>> s.model()
7061  [a = -2]
7062  """
7063  try:
7064  return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx)
7065  except Z3Exception:
7066  raise Z3Exception("model is not available")
7067 
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.

Referenced by ModelRef.__del__(), ModelRef.__getitem__(), ModelRef.__len__(), ModelRef.decls(), ModelRef.eval(), ModelRef.get_interp(), ModelRef.get_sort(), ModelRef.get_universe(), ModelRef.num_sorts(), ModelRef.sexpr(), FuncInterp.translate(), ModelRef.translate(), and ModelRef.update_value().

◆ non_units()

def non_units (   self)
Return an AST vector containing all atomic formulas in solver state that are not units.

Definition at line 7192 of file z3py.py.

7192  def non_units(self):
7193  """Return an AST vector containing all atomic formulas in solver state that are not units.
7194  """
7195  return AstVector(Z3_solver_get_non_units(self.ctx.ref(), self.solver), self.ctx)
7196 
Z3_ast_vector Z3_API Z3_solver_get_non_units(Z3_context c, Z3_solver s)
Return the set of non units in the solver state.

◆ num_scopes()

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

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

Definition at line 6902 of file z3py.py.

6902  def num_scopes(self):
6903  """Return the current number of backtracking points.
6904 
6905  >>> s = Solver()
6906  >>> s.num_scopes()
6907  0
6908  >>> s.push()
6909  >>> s.num_scopes()
6910  1
6911  >>> s.push()
6912  >>> s.num_scopes()
6913  2
6914  >>> s.pop()
6915  >>> s.num_scopes()
6916  1
6917  """
6918  return Z3_solver_get_num_scopes(self.ctx.ref(), self.solver)
6919 
unsigned Z3_API Z3_solver_get_num_scopes(Z3_context c, Z3_solver s)
Return the number of backtracking points.

◆ param_descrs()

def param_descrs (   self)
Return the parameter description set.

Definition at line 7245 of file z3py.py.

7245  def param_descrs(self):
7246  """Return the parameter description set."""
7247  return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx)
7248 
Z3_param_descrs Z3_API Z3_solver_get_param_descrs(Z3_context c, Z3_solver s)
Return the parameter description set for the given solver object.

◆ pop()

def pop (   self,
  num = 1 
)
Backtrack \\c num backtracking points.

>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0)
>>> s
[x > 0]
>>> s.push()
>>> s.add(x < 1)
>>> s
[x > 0, x < 1]
>>> s.check()
unsat
>>> s.pop()
>>> s.check()
sat
>>> s
[x > 0]

Definition at line 6880 of file z3py.py.

6880  def pop(self, num=1):
6881  """Backtrack \\c num backtracking points.
6882 
6883  >>> x = Int('x')
6884  >>> s = Solver()
6885  >>> s.add(x > 0)
6886  >>> s
6887  [x > 0]
6888  >>> s.push()
6889  >>> s.add(x < 1)
6890  >>> s
6891  [x > 0, x < 1]
6892  >>> s.check()
6893  unsat
6894  >>> s.pop()
6895  >>> s.check()
6896  sat
6897  >>> s
6898  [x > 0]
6899  """
6900  Z3_solver_pop(self.ctx.ref(), self.solver, num)
6901 
void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n)
Backtrack n backtracking points.

◆ proof()

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

Definition at line 7169 of file z3py.py.

7169  def proof(self):
7170  """Return a proof for the last `check()`. Proof construction must be enabled."""
7171  return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
7172 
Z3_ast Z3_API Z3_solver_get_proof(Z3_context c, Z3_solver s)
Retrieve the proof for the last Z3_solver_check or Z3_solver_check_assumptions.

◆ push()

def push (   self)
Create a backtracking point.

>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0)
>>> s
[x > 0]
>>> s.push()
>>> s.add(x < 1)
>>> s
[x > 0, x < 1]
>>> s.check()
unsat
>>> s.pop()
>>> s.check()
sat
>>> s
[x > 0]

Definition at line 6858 of file z3py.py.

6858  def push(self):
6859  """Create a backtracking point.
6860 
6861  >>> x = Int('x')
6862  >>> s = Solver()
6863  >>> s.add(x > 0)
6864  >>> s
6865  [x > 0]
6866  >>> s.push()
6867  >>> s.add(x < 1)
6868  >>> s
6869  [x > 0, x < 1]
6870  >>> s.check()
6871  unsat
6872  >>> s.pop()
6873  >>> s.check()
6874  sat
6875  >>> s
6876  [x > 0]
6877  """
6878  Z3_solver_push(self.ctx.ref(), self.solver)
6879 
void Z3_API Z3_solver_push(Z3_context c, Z3_solver s)
Create a backtracking point.

◆ reason_unknown()

def reason_unknown (   self)
Return a string describing why the last `check()` returned `unknown`.

>>> x = Int('x')
>>> s = SimpleSolver()
>>> s.add(2**x == 4)
>>> s.check()
unknown
>>> s.reason_unknown()
'(incomplete (theory arithmetic))'

Definition at line 7228 of file z3py.py.

7228  def reason_unknown(self):
7229  """Return a string describing why the last `check()` returned `unknown`.
7230 
7231  >>> x = Int('x')
7232  >>> s = SimpleSolver()
7233  >>> s.add(2**x == 4)
7234  >>> s.check()
7235  unknown
7236  >>> s.reason_unknown()
7237  '(incomplete (theory arithmetic))'
7238  """
7239  return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver)
7240 
Z3_string Z3_API Z3_solver_get_reason_unknown(Z3_context c, Z3_solver s)
Return a brief justification for an "unknown" result (i.e., Z3_L_UNDEF) for the commands Z3_solver_ch...

◆ reset()

def reset (   self)
Remove all asserted constraints and backtracking points created using `push()`.

>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0)
>>> s
[x > 0]
>>> s.reset()
>>> s
[]

Definition at line 6920 of file z3py.py.

6920  def reset(self):
6921  """Remove all asserted constraints and backtracking points created using `push()`.
6922 
6923  >>> x = Int('x')
6924  >>> s = Solver()
6925  >>> s.add(x > 0)
6926  >>> s
6927  [x > 0]
6928  >>> s.reset()
6929  >>> s
6930  []
6931  """
6932  Z3_solver_reset(self.ctx.ref(), self.solver)
6933 
void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)
Remove all assertions from the solver.

◆ set()

def set (   self,
args,
**  keys 
)
Set a configuration option.
The method `help()` return a string containing all available options.

>>> s = Solver()
>>> # The option MBQI can be set using three different approaches.
>>> s.set(mbqi=True)
>>> s.set('MBQI', True)
>>> s.set(':mbqi', True)

Definition at line 6845 of file z3py.py.

6845  def set(self, *args, **keys):
6846  """Set a configuration option.
6847  The method `help()` return a string containing all available options.
6848 
6849  >>> s = Solver()
6850  >>> # The option MBQI can be set using three different approaches.
6851  >>> s.set(mbqi=True)
6852  >>> s.set('MBQI', True)
6853  >>> s.set(':mbqi', True)
6854  """
6855  p = args2params(args, keys, self.ctx)
6856  Z3_solver_set_params(self.ctx.ref(), self.solver, p.params)
6857 
void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p)
Set the given solver using the given parameters.
def args2params(arguments, keywords, ctx=None)
Definition: z3py.py:5422

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

7272  def sexpr(self):
7273  """Return a formatted string (in Lisp-like format) with all added constraints.
7274  We say the string is in s-expression format.
7275 
7276  >>> x = Int('x')
7277  >>> s = Solver()
7278  >>> s.add(x > 0)
7279  >>> s.add(x < 2)
7280  >>> r = s.sexpr()
7281  """
7282  return Z3_solver_to_string(self.ctx.ref(), self.solver)
7283 
Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s)
Convert a solver into a string.

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

7210  def statistics(self):
7211  """Return statistics for the last `check()`.
7212 
7213  >>> s = SimpleSolver()
7214  >>> x = Int('x')
7215  >>> s.add(x > 0)
7216  >>> s.check()
7217  sat
7218  >>> st = s.statistics()
7219  >>> st.get_key_value('final checks')
7220  1
7221  >>> len(st) > 0
7222  True
7223  >>> st[0] != 0
7224  True
7225  """
7226  return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx)
7227 
Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s)
Return statistics for the given solver.

◆ to_smt2()

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

Definition at line 7288 of file z3py.py.

7288  def to_smt2(self):
7289  """return SMTLIB2 formatted benchmark for solver's assertions"""
7290  es = self.assertions()
7291  sz = len(es)
7292  sz1 = sz
7293  if sz1 > 0:
7294  sz1 -= 1
7295  v = (Ast * sz1)()
7296  for i in range(sz1):
7297  v[i] = es[i].as_ast()
7298  if sz > 0:
7299  e = es[sz1].as_ast()
7300  else:
7301  e = BoolVal(True, self.ctx).as_ast()
7303  self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e,
7304  )
7305 
7306 
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.
def BoolVal(val, ctx=None)
Definition: z3py.py:1672

◆ trail()

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

Definition at line 7205 of file z3py.py.

7205  def trail(self):
7206  """Return trail of the solver state after a check() call.
7207  """
7208  return AstVector(Z3_solver_get_trail(self.ctx.ref(), self.solver), self.ctx)
7209 
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...

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

7197  def trail_levels(self):
7198  """Return trail and decision levels of the solver state after a check() call.
7199  """
7200  trail = self.trail()
7201  levels = (ctypes.c_uint * len(trail))()
7202  Z3_solver_get_levels(self.ctx.ref(), self.solver, trail.vector, len(trail), levels)
7203  return trail, levels
7204 
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...

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

7253  def translate(self, target):
7254  """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
7255 
7256  >>> c1 = Context()
7257  >>> c2 = Context()
7258  >>> s1 = Solver(ctx=c1)
7259  >>> s2 = s1.translate(c2)
7260  """
7261  if z3_debug():
7262  _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
7263  solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref())
7264  return Solver(solver, target)
7265 
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.
def z3_debug()
Definition: z3py.py:62

Referenced by AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), Solver.__copy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), and Solver.__deepcopy__().

◆ units()

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

Definition at line 7187 of file z3py.py.

7187  def units(self):
7188  """Return an AST vector containing all currently inferred units.
7189  """
7190  return AstVector(Z3_solver_get_units(self.ctx.ref(), self.solver), self.ctx)
7191 
Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s)
Return the set of units modulo model conversion.

◆ unsat_core()

def unsat_core (   self)
Return a subset (as an AST vector) of the assumptions provided to the last check().

These are the assumptions Z3 used in the unsatisfiability proof.
Assumptions are available in Z3. They are used to extract unsatisfiable cores.
They may be also used to "retract" assumptions. Note that, assumptions are not really
"soft constraints", but they can be used to implement them.

>>> p1, p2, p3 = Bools('p1 p2 p3')
>>> x, y       = Ints('x y')
>>> s          = Solver()
>>> s.add(Implies(p1, x > 0))
>>> s.add(Implies(p2, y > x))
>>> s.add(Implies(p2, y < 1))
>>> s.add(Implies(p3, y > -3))
>>> s.check(p1, p2, p3)
unsat
>>> core = s.unsat_core()
>>> len(core)
2
>>> p1 in core
True
>>> p2 in core
True
>>> p3 in core
False
>>> # "Retracting" p2
>>> s.check(p1, p3)
sat

Definition at line 7072 of file z3py.py.

7072  def unsat_core(self):
7073  """Return a subset (as an AST vector) of the assumptions provided to the last check().
7074 
7075  These are the assumptions Z3 used in the unsatisfiability proof.
7076  Assumptions are available in Z3. They are used to extract unsatisfiable cores.
7077  They may be also used to "retract" assumptions. Note that, assumptions are not really
7078  "soft constraints", but they can be used to implement them.
7079 
7080  >>> p1, p2, p3 = Bools('p1 p2 p3')
7081  >>> x, y = Ints('x y')
7082  >>> s = Solver()
7083  >>> s.add(Implies(p1, x > 0))
7084  >>> s.add(Implies(p2, y > x))
7085  >>> s.add(Implies(p2, y < 1))
7086  >>> s.add(Implies(p3, y > -3))
7087  >>> s.check(p1, p2, p3)
7088  unsat
7089  >>> core = s.unsat_core()
7090  >>> len(core)
7091  2
7092  >>> p1 in core
7093  True
7094  >>> p2 in core
7095  True
7096  >>> p3 in core
7097  False
7098  >>> # "Retracting" p2
7099  >>> s.check(p1, p3)
7100  sat
7101  """
7102  return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx)
7103 
Z3_ast_vector Z3_API Z3_solver_get_unsat_core(Z3_context c, Z3_solver s)
Retrieve the unsat core for the last Z3_solver_check_assumptions The unsat core is a subset of the as...

Field Documentation

◆ backtrack_level

backtrack_level

Definition at line 6831 of file z3py.py.

◆ ctx

ctx

Definition at line 6830 of file z3py.py.

Referenced by ArithRef.__add__(), BitVecRef.__add__(), FPRef.__add__(), BitVecRef.__and__(), FuncDeclRef.__call__(), Probe.__call__(), AstMap.__contains__(), AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), Solver.__copy__(), AstRef.__deepcopy__(), Datatype.__deepcopy__(), ParamsRef.__deepcopy__(), ParamDescrsRef.__deepcopy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), AstMap.__deepcopy__(), FuncEntry.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), Statistics.__deepcopy__(), Solver.__deepcopy__(), Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), Context.__del__(), AstRef.__del__(), ScopedConstructor.__del__(), ScopedConstructorList.__del__(), ParamsRef.__del__(), ParamDescrsRef.__del__(), Goal.__del__(), AstVector.__del__(), AstMap.__del__(), FuncEntry.__del__(), FuncInterp.__del__(), ModelRef.__del__(), Statistics.__del__(), Solver.__del__(), Fixedpoint.__del__(), Optimize.__del__(), ApplyResult.__del__(), Tactic.__del__(), Probe.__del__(), ArithRef.__div__(), BitVecRef.__div__(), FPRef.__div__(), ExprRef.__eq__(), Probe.__eq__(), ArithRef.__ge__(), BitVecRef.__ge__(), Probe.__ge__(), FPRef.__ge__(), SeqRef.__ge__(), AstVector.__getitem__(), SeqRef.__getitem__(), ModelRef.__getitem__(), Statistics.__getitem__(), ApplyResult.__getitem__(), AstMap.__getitem__(), ArithRef.__gt__(), BitVecRef.__gt__(), Probe.__gt__(), FPRef.__gt__(), SeqRef.__gt__(), BitVecRef.__invert__(), ArithRef.__le__(), BitVecRef.__le__(), Probe.__le__(), FPRef.__le__(), SeqRef.__le__(), CharRef.__le__(), AstVector.__len__(), AstMap.__len__(), ModelRef.__len__(), Statistics.__len__(), ApplyResult.__len__(), BitVecRef.__lshift__(), ArithRef.__lt__(), BitVecRef.__lt__(), Probe.__lt__(), FPRef.__lt__(), SeqRef.__lt__(), ArithRef.__mod__(), BitVecRef.__mod__(), ArithRef.__mul__(), BitVecRef.__mul__(), FPRef.__mul__(), ExprRef.__ne__(), Probe.__ne__(), ArithRef.__neg__(), BitVecRef.__neg__(), BitVecRef.__or__(), ArithRef.__pow__(), ArithRef.__radd__(), BitVecRef.__radd__(), FPRef.__radd__(), BitVecRef.__rand__(), ArithRef.__rdiv__(), BitVecRef.__rdiv__(), FPRef.__rdiv__(), ParamsRef.__repr__(), ParamDescrsRef.__repr__(), AstMap.__repr__(), Statistics.__repr__(), BitVecRef.__rlshift__(), ArithRef.__rmod__(), BitVecRef.__rmod__(), ArithRef.__rmul__(), BitVecRef.__rmul__(), FPRef.__rmul__(), BitVecRef.__ror__(), ArithRef.__rpow__(), BitVecRef.__rrshift__(), BitVecRef.__rshift__(), ArithRef.__rsub__(), BitVecRef.__rsub__(), FPRef.__rsub__(), BitVecRef.__rxor__(), AstVector.__setitem__(), AstMap.__setitem__(), ArithRef.__sub__(), BitVecRef.__sub__(), FPRef.__sub__(), BitVecRef.__xor__(), DatatypeSortRef.accessor(), Fixedpoint.add_cover(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), AlgebraicNumRef.approx(), ExprRef.arg(), FuncEntry.arg_value(), FuncInterp.arity(), Goal.as_expr(), ApplyResult.as_expr(), FPNumRef.as_string(), Solver.assert_and_track(), Optimize.assert_and_track(), Goal.assert_exprs(), Solver.assert_exprs(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Solver.assertions(), Optimize.assertions(), SeqRef.at(), SeqSortRef.basis(), ReSortRef.basis(), QuantifierRef.body(), BoolSortRef.cast(), Solver.check(), Optimize.check(), UserPropagateBase.conflict(), Solver.consequences(), DatatypeSortRef.constructor(), Goal.convert_model(), AstRef.ctx_ref(), UserPropagateBase.ctx_ref(), ExprRef.decl(), ModelRef.decls(), ArrayRef.default(), RatNumRef.denominator(), Goal.depth(), Goal.dimacs(), Solver.dimacs(), ArraySortRef.domain(), FuncDeclRef.domain(), ArraySortRef.domain_n(), FuncInterp.else_value(), FuncInterp.entry(), AstMap.erase(), ModelRef.eval(), FPNumRef.exponent(), FPNumRef.exponent_as_bv(), FPNumRef.exponent_as_long(), Solver.from_file(), Optimize.from_file(), Solver.from_string(), Optimize.from_string(), Goal.get(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), ParamDescrsRef.get_documentation(), Fixedpoint.get_ground_sat_answer(), ModelRef.get_interp(), Statistics.get_key_value(), ParamDescrsRef.get_kind(), ParamDescrsRef.get_name(), Fixedpoint.get_num_levels(), Fixedpoint.get_rule_names_along_trace(), Fixedpoint.get_rules(), Fixedpoint.get_rules_along_trace(), ModelRef.get_sort(), ModelRef.get_universe(), Solver.help(), Fixedpoint.help(), Optimize.help(), Tactic.help(), Solver.import_model_converter(), Goal.inconsistent(), CharRef.is_digit(), FPNumRef.isInf(), FPNumRef.isNaN(), FPNumRef.isNegative(), FPNumRef.isNormal(), FPNumRef.isPositive(), FPNumRef.isSubnormal(), FPNumRef.isZero(), AstMap.keys(), Statistics.keys(), SortRef.kind(), Optimize.maximize(), Optimize.minimize(), Solver.model(), Optimize.model(), SortRef.name(), FuncDeclRef.name(), QuantifierRef.no_pattern(), Solver.non_units(), FuncEntry.num_args(), FuncInterp.num_entries(), Solver.num_scopes(), ModelRef.num_sorts(), RatNumRef.numerator(), Optimize.objectives(), Solver.param_descrs(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), FuncDeclRef.params(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), QuantifierRef.pattern(), AlgebraicNumRef.poly(), Optimize.pop(), Solver.pop(), Goal.prec(), Solver.proof(), Solver.push(), Optimize.push(), AstVector.push(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), FuncDeclRef.range(), ArraySortRef.range(), Solver.reason_unknown(), Fixedpoint.reason_unknown(), Optimize.reason_unknown(), DatatypeSortRef.recognizer(), Context.ref(), Fixedpoint.register_relation(), AstMap.reset(), Solver.reset(), AstVector.resize(), Solver.set(), Fixedpoint.set(), Optimize.set(), ParamsRef.set(), Optimize.set_on_model(), Fixedpoint.set_predicate_representation(), Goal.sexpr(), AstVector.sexpr(), ModelRef.sexpr(), Solver.sexpr(), Fixedpoint.sexpr(), Optimize.sexpr(), ApplyResult.sexpr(), FPNumRef.sign(), FPNumRef.sign_as_bv(), FPNumRef.significand(), FPNumRef.significand_as_bv(), FPNumRef.significand_as_long(), ParamDescrsRef.size(), Goal.size(), Tactic.solver(), ExprRef.sort(), BoolRef.sort(), QuantifierRef.sort(), ArithRef.sort(), BitVecRef.sort(), ArrayRef.sort(), DatatypeRef.sort(), FiniteDomainRef.sort(), FPRef.sort(), SeqRef.sort(), Solver.statistics(), Fixedpoint.statistics(), Optimize.statistics(), CharRef.to_bv(), CharRef.to_int(), Solver.to_smt2(), Fixedpoint.to_string(), Solver.trail(), Solver.trail_levels(), AstVector.translate(), FuncInterp.translate(), AstRef.translate(), Goal.translate(), ModelRef.translate(), Solver.translate(), Solver.units(), Solver.unsat_core(), Optimize.unsat_core(), Fixedpoint.update_rule(), ParamsRef.validate(), FuncEntry.value(), QuantifierRef.var_name(), and QuantifierRef.var_sort().

◆ cube_vs

cube_vs

Definition at line 7148 of file z3py.py.

Referenced by Solver.cube_vars().

◆ solver

solver