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

Constructor & Destructor Documentation

◆ __init__()

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

Definition at line 6793 of file z3py.py.

6793  def __init__(self, solver=None, ctx=None, logFile=None):
6794  assert solver is None or ctx is not None
6795  self.ctx = _get_ctx(ctx)
6796  self.backtrack_level = 4000000000
6797  self.solver = None
6798  if solver is None:
6799  self.solver = Z3_mk_solver(self.ctx.ref())
6800  else:
6801  self.solver = solver
6802  Z3_solver_inc_ref(self.ctx.ref(), self.solver)
6803  if logFile is not None:
6804  self.set("smtlib2_log", logFile)
6805 
def __init__(self, s, ctx=None)
Definition: z3py.py:11177
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 6806 of file z3py.py.

6806  def __del__(self):
6807  if self.solver is not None and self.ctx.ref() is not None:
6808  Z3_solver_dec_ref(self.ctx.ref(), self.solver)
6809 
def __del__(self)
Definition: z3py.py:11202
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 7231 of file z3py.py.

7231  def __copy__(self):
7232  return self.translate(self.ctx)
7233 

◆ __deepcopy__()

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 7234 of file z3py.py.

7234  def __deepcopy__(self, memo={}):
7235  return self.translate(self.ctx)
7236 

◆ __iadd__()

def __iadd__ (   self,
  fml 
)

Definition at line 6929 of file z3py.py.

6929  def __iadd__(self, fml):
6930  self.add(fml)
6931  return self
6932 

◆ __repr__()

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

Definition at line 7214 of file z3py.py.

7214  def __repr__(self):
7215  """Return a formatted string with all added constraints."""
7216  return obj_to_string(self)
7217 

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

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

6918  def add(self, *args):
6919  """Assert constraints into the solver.
6920 
6921  >>> x = Int('x')
6922  >>> s = Solver()
6923  >>> s.add(x > 0, x < 2)
6924  >>> s
6925  [x > 0, x < 2]
6926  """
6927  self.assert_exprs(*args)
6928 
def add(self, e)
Definition: z3py.py:11248

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

6933  def append(self, *args):
6934  """Assert constraints into the solver.
6935 
6936  >>> x = Int('x')
6937  >>> s = Solver()
6938  >>> s.append(x > 0, x < 2)
6939  >>> s
6940  [x > 0, x < 2]
6941  """
6942  self.assert_exprs(*args)
6943 

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

6955  def assert_and_track(self, a, p):
6956  """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
6957 
6958  If `p` is a string, it will be automatically converted into a Boolean constant.
6959 
6960  >>> x = Int('x')
6961  >>> p3 = Bool('p3')
6962  >>> s = Solver()
6963  >>> s.set(unsat_core=True)
6964  >>> s.assert_and_track(x > 0, 'p1')
6965  >>> s.assert_and_track(x != 1, 'p2')
6966  >>> s.assert_and_track(x < 0, p3)
6967  >>> print(s.check())
6968  unsat
6969  >>> c = s.unsat_core()
6970  >>> len(c)
6971  2
6972  >>> Bool('p1') in c
6973  True
6974  >>> Bool('p2') in c
6975  False
6976  >>> p3 in c
6977  True
6978  """
6979  if isinstance(p, str):
6980  p = Bool(p, self.ctx)
6981  _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
6982  _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
6983  Z3_solver_assert_and_track(self.ctx.ref(), self.solver, a.as_ast(), p.as_ast())
6984 
def is_const(a)
Definition: z3py.py:1259
def Bool(name, ctx=None)
Definition: z3py.py:1692
void Z3_API Z3_solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p)
Assert a constraint a into the solver, and track it (in the unsat) core using the Boolean constant p...

◆ assert_exprs()

def assert_exprs (   self,
  args 
)
Assert constraints into the solver.

>>> x = Int('x')
>>> s = Solver()
>>> s.assert_exprs(x > 0, x < 2)
>>> s
[x > 0, x < 2]

Definition at line 6899 of file z3py.py.

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

6899  def assert_exprs(self, *args):
6900  """Assert constraints into the solver.
6901 
6902  >>> x = Int('x')
6903  >>> s = Solver()
6904  >>> s.assert_exprs(x > 0, x < 2)
6905  >>> s
6906  [x > 0, x < 2]
6907  """
6908  args = _get_args(args)
6909  s = BoolSort(self.ctx)
6910  for arg in args:
6911  if isinstance(arg, Goal) or isinstance(arg, AstVector):
6912  for f in arg:
6913  Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast())
6914  else:
6915  arg = s.cast(arg)
6916  Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast())
6917 
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:1655

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

Referenced by Solver.to_smt2().

7138  def assertions(self):
7139  """Return an AST vector containing all added constraints.
7140 
7141  >>> s = Solver()
7142  >>> s.assertions()
7143  []
7144  >>> a = Int('a')
7145  >>> s.add(a > 0)
7146  >>> s.add(a < 10)
7147  >>> s.assertions()
7148  [a > 0, a < 10]
7149  """
7150  return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
7151 
Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s)
Return the set of asserted formulas on the solver.

◆ check()

def check (   self,
  assumptions 
)
Check whether the assertions in the given solver plus the optional assumptions are consistent or not.

>>> x = Int('x')
>>> s = Solver()
>>> s.check()
sat
>>> s.add(x > 0, x < 2)
>>> s.check()
sat
>>> s.model().eval(x)
1
>>> s.add(x < 1)
>>> s.check()
unsat
>>> s.reset()
>>> s.add(2**x == 4)
>>> s.check()
unknown

Definition at line 6985 of file z3py.py.

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

6985  def check(self, *assumptions):
6986  """Check whether the assertions in the given solver plus the optional assumptions are consistent or not.
6987 
6988  >>> x = Int('x')
6989  >>> s = Solver()
6990  >>> s.check()
6991  sat
6992  >>> s.add(x > 0, x < 2)
6993  >>> s.check()
6994  sat
6995  >>> s.model().eval(x)
6996  1
6997  >>> s.add(x < 1)
6998  >>> s.check()
6999  unsat
7000  >>> s.reset()
7001  >>> s.add(2**x == 4)
7002  >>> s.check()
7003  unknown
7004  """
7005  s = BoolSort(self.ctx)
7006  assumptions = _get_args(assumptions)
7007  num = len(assumptions)
7008  _assumptions = (Ast * num)()
7009  for i in range(num):
7010  _assumptions[i] = s.cast(assumptions[i]).as_ast()
7011  r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions)
7012  return CheckSatResult(r)
7013 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3725
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...
def BoolSort(ctx=None)
Definition: z3py.py:1655

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

7069  def consequences(self, assumptions, variables):
7070  """Determine fixed values for the variables based on the solver state and assumptions.
7071  >>> s = Solver()
7072  >>> a, b, c, d = Bools('a b c d')
7073  >>> s.add(Implies(a,b), Implies(b, c))
7074  >>> s.consequences([a],[b,c,d])
7075  (sat, [Implies(a, b), Implies(a, c)])
7076  >>> s.consequences([Not(c),d],[a,b,c,d])
7077  (sat, [Implies(d, d), Implies(Not(c), Not(c)), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))])
7078  """
7079  if isinstance(assumptions, list):
7080  _asms = AstVector(None, self.ctx)
7081  for a in assumptions:
7082  _asms.push(a)
7083  assumptions = _asms
7084  if isinstance(variables, list):
7085  _vars = AstVector(None, self.ctx)
7086  for a in variables:
7087  _vars.push(a)
7088  variables = _vars
7089  _z3_assert(isinstance(assumptions, AstVector), "ast vector expected")
7090  _z3_assert(isinstance(variables, AstVector), "ast vector expected")
7091  consequences = AstVector(None, self.ctx)
7092  r = Z3_solver_get_consequences(self.ctx.ref(), self.solver, assumptions.vector,
7093  variables.vector, consequences.vector)
7094  sz = len(consequences)
7095  consequences = [consequences[i] for i in range(sz)]
7096  return CheckSatResult(r), consequences
7097 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3725
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 7106 of file z3py.py.

7106  def cube(self, vars=None):
7107  """Get set of cubes
7108  The method takes an optional set of variables that restrict which
7109  variables may be used as a starting point for cubing.
7110  If vars is not None, then the first case split is based on a variable in
7111  this set.
7112  """
7113  self.cube_vs = AstVector(None, self.ctx)
7114  if vars is not None:
7115  for v in vars:
7116  self.cube_vs.push(v)
7117  while True:
7118  lvl = self.backtrack_level
7119  self.backtrack_level = 4000000000
7120  r = AstVector(Z3_solver_cube(self.ctx.ref(), self.solver, self.cube_vs.vector, lvl), self.ctx)
7121  if (len(r) == 1 and is_false(r[0])):
7122  return
7123  yield r
7124  if (len(r) == 0):
7125  return
7126 
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:1571

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

7127  def cube_vars(self):
7128  """Access the set of variables that were touched by the most recently generated cube.
7129  This set of variables can be used as a starting point for additional cubes.
7130  The idea is that variables that appear in clauses that are reduced by the most recent
7131  cube are likely more useful to cube on."""
7132  return self.cube_vs
7133 

◆ dimacs()

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

Definition at line 7249 of file z3py.py.

7249  def dimacs(self, include_names=True):
7250  """Return a textual representation of the solver in DIMACS format."""
7251  return Z3_solver_to_dimacs_string(self.ctx.ref(), self.solver, include_names)
7252 
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 7098 of file z3py.py.

7098  def from_file(self, filename):
7099  """Parse assertions from a file"""
7100  Z3_solver_from_file(self.ctx.ref(), self.solver, filename)
7101 
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 7102 of file z3py.py.

7102  def from_string(self, s):
7103  """Parse assertions from a string"""
7104  Z3_solver_from_string(self.ctx.ref(), self.solver, s)
7105 
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 7206 of file z3py.py.

Referenced by Solver.set().

7206  def help(self):
7207  """Display a string describing all available options."""
7208  print(Z3_solver_get_help(self.ctx.ref(), self.solver))
7209 
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 7033 of file z3py.py.

7033  def import_model_converter(self, other):
7034  """Import model converter from other into the current solver"""
7035  Z3_solver_import_model_converter(self.ctx.ref(), other.solver, self.solver)
7036 
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 6944 of file z3py.py.

6944  def insert(self, *args):
6945  """Assert constraints into the solver.
6946 
6947  >>> x = Int('x')
6948  >>> s = Solver()
6949  >>> s.insert(x > 0, x < 2)
6950  >>> s
6951  [x > 0, x < 2]
6952  """
6953  self.assert_exprs(*args)
6954 

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

7014  def model(self):
7015  """Return a model for the last `check()`.
7016 
7017  This function raises an exception if
7018  a model is not available (e.g., last `check()` returned unsat).
7019 
7020  >>> s = Solver()
7021  >>> a = Int('a')
7022  >>> s.add(a + 2 == 0)
7023  >>> s.check()
7024  sat
7025  >>> s.model()
7026  [a = -2]
7027  """
7028  try:
7029  return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx)
7030  except Z3Exception:
7031  raise Z3Exception("model is not available")
7032 
Z3_model Z3_API Z3_solver_get_model(Z3_context c, Z3_solver s)
Retrieve the model for the last Z3_solver_check or Z3_solver_check_assumptions.

◆ non_units()

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

Definition at line 7157 of file z3py.py.

7157  def non_units(self):
7158  """Return an AST vector containing all atomic formulas in solver state that are not units.
7159  """
7160  return AstVector(Z3_solver_get_non_units(self.ctx.ref(), self.solver), self.ctx)
7161 
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 6867 of file z3py.py.

6867  def num_scopes(self):
6868  """Return the current number of backtracking points.
6869 
6870  >>> s = Solver()
6871  >>> s.num_scopes()
6872  0
6873  >>> s.push()
6874  >>> s.num_scopes()
6875  1
6876  >>> s.push()
6877  >>> s.num_scopes()
6878  2
6879  >>> s.pop()
6880  >>> s.num_scopes()
6881  1
6882  """
6883  return Z3_solver_get_num_scopes(self.ctx.ref(), self.solver)
6884 
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 7210 of file z3py.py.

7210  def param_descrs(self):
7211  """Return the parameter description set."""
7212  return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx)
7213 
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 6845 of file z3py.py.

6845  def pop(self, num=1):
6846  """Backtrack \\c num backtracking points.
6847 
6848  >>> x = Int('x')
6849  >>> s = Solver()
6850  >>> s.add(x > 0)
6851  >>> s
6852  [x > 0]
6853  >>> s.push()
6854  >>> s.add(x < 1)
6855  >>> s
6856  [x > 0, x < 1]
6857  >>> s.check()
6858  unsat
6859  >>> s.pop()
6860  >>> s.check()
6861  sat
6862  >>> s
6863  [x > 0]
6864  """
6865  Z3_solver_pop(self.ctx.ref(), self.solver, num)
6866 
void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n)
Backtrack n backtracking points.
def pop(self, num_scopes)
Definition: z3py.py:11242

◆ proof()

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

Definition at line 7134 of file z3py.py.

7134  def proof(self):
7135  """Return a proof for the last `check()`. Proof construction must be enabled."""
7136  return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
7137 
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 6823 of file z3py.py.

Referenced by Solver.reset().

6823  def push(self):
6824  """Create a backtracking point.
6825 
6826  >>> x = Int('x')
6827  >>> s = Solver()
6828  >>> s.add(x > 0)
6829  >>> s
6830  [x > 0]
6831  >>> s.push()
6832  >>> s.add(x < 1)
6833  >>> s
6834  [x > 0, x < 1]
6835  >>> s.check()
6836  unsat
6837  >>> s.pop()
6838  >>> s.check()
6839  sat
6840  >>> s
6841  [x > 0]
6842  """
6843  Z3_solver_push(self.ctx.ref(), self.solver)
6844 
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 7193 of file z3py.py.

7193  def reason_unknown(self):
7194  """Return a string describing why the last `check()` returned `unknown`.
7195 
7196  >>> x = Int('x')
7197  >>> s = SimpleSolver()
7198  >>> s.add(2**x == 4)
7199  >>> s.check()
7200  unknown
7201  >>> s.reason_unknown()
7202  '(incomplete (theory arithmetic))'
7203  """
7204  return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver)
7205 
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 6885 of file z3py.py.

6885  def reset(self):
6886  """Remove all asserted constraints and backtracking points created using `push()`.
6887 
6888  >>> x = Int('x')
6889  >>> s = Solver()
6890  >>> s.add(x > 0)
6891  >>> s
6892  [x > 0]
6893  >>> s.reset()
6894  >>> s
6895  []
6896  """
6897  Z3_solver_reset(self.ctx.ref(), self.solver)
6898 
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 6810 of file z3py.py.

6810  def set(self, *args, **keys):
6811  """Set a configuration option.
6812  The method `help()` return a string containing all available options.
6813 
6814  >>> s = Solver()
6815  >>> # The option MBQI can be set using three different approaches.
6816  >>> s.set(mbqi=True)
6817  >>> s.set('MBQI', True)
6818  >>> s.set(':mbqi', True)
6819  """
6820  p = args2params(args, keys, self.ctx)
6821  Z3_solver_set_params(self.ctx.ref(), self.solver, p.params)
6822 
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:5396

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

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

7237  def sexpr(self):
7238  """Return a formatted string (in Lisp-like format) with all added constraints.
7239  We say the string is in s-expression format.
7240 
7241  >>> x = Int('x')
7242  >>> s = Solver()
7243  >>> s.add(x > 0)
7244  >>> s.add(x < 2)
7245  >>> r = s.sexpr()
7246  """
7247  return Z3_solver_to_string(self.ctx.ref(), self.solver)
7248 
Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s)
Convert a solver into a string.

◆ statistics()

def statistics (   self)
Return statistics for the last `check()`.

>>> s = SimpleSolver()
>>> x = Int('x')
>>> s.add(x > 0)
>>> s.check()
sat
>>> st = s.statistics()
>>> st.get_key_value('final checks')
1
>>> len(st) > 0
True
>>> st[0] != 0
True

Definition at line 7175 of file z3py.py.

7175  def statistics(self):
7176  """Return statistics for the last `check()`.
7177 
7178  >>> s = SimpleSolver()
7179  >>> x = Int('x')
7180  >>> s.add(x > 0)
7181  >>> s.check()
7182  sat
7183  >>> st = s.statistics()
7184  >>> st.get_key_value('final checks')
7185  1
7186  >>> len(st) > 0
7187  True
7188  >>> st[0] != 0
7189  True
7190  """
7191  return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx)
7192 
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 7253 of file z3py.py.

7253  def to_smt2(self):
7254  """return SMTLIB2 formatted benchmark for solver's assertions"""
7255  es = self.assertions()
7256  sz = len(es)
7257  sz1 = sz
7258  if sz1 > 0:
7259  sz1 -= 1
7260  v = (Ast * sz1)()
7261  for i in range(sz1):
7262  v[i] = es[i].as_ast()
7263  if sz > 0:
7264  e = es[sz1].as_ast()
7265  else:
7266  e = BoolVal(True, self.ctx).as_ast()
7268  self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e,
7269  )
7270 
7271 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3725
def BoolVal(val, ctx=None)
Definition: z3py.py:1673
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.

◆ trail()

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

Definition at line 7170 of file z3py.py.

7170  def trail(self):
7171  """Return trail of the solver state after a check() call.
7172  """
7173  return AstVector(Z3_solver_get_trail(self.ctx.ref(), self.solver), self.ctx)
7174 
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...

◆ trail_levels()

def trail_levels (   self)
Return trail and decision levels of the solver state after a check() call.

Definition at line 7162 of file z3py.py.

7162  def trail_levels(self):
7163  """Return trail and decision levels of the solver state after a check() call.
7164  """
7165  trail = self.trail()
7166  levels = (ctypes.c_uint * len(trail))()
7167  Z3_solver_get_levels(self.ctx.ref(), self.solver, trail.vector, len(trail), levels)
7168  return trail, levels
7169 
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 7218 of file z3py.py.

7218  def translate(self, target):
7219  """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
7220 
7221  >>> c1 = Context()
7222  >>> c2 = Context()
7223  >>> s1 = Solver(ctx=c1)
7224  >>> s2 = s1.translate(c2)
7225  """
7226  if z3_debug():
7227  _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
7228  solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref())
7229  return Solver(solver, target)
7230 
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:64

◆ units()

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

Definition at line 7152 of file z3py.py.

7152  def units(self):
7153  """Return an AST vector containing all currently inferred units.
7154  """
7155  return AstVector(Z3_solver_get_units(self.ctx.ref(), self.solver), self.ctx)
7156 
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 7037 of file z3py.py.

7037  def unsat_core(self):
7038  """Return a subset (as an AST vector) of the assumptions provided to the last check().
7039 
7040  These are the assumptions Z3 used in the unsatisfiability proof.
7041  Assumptions are available in Z3. They are used to extract unsatisfiable cores.
7042  They may be also used to "retract" assumptions. Note that, assumptions are not really
7043  "soft constraints", but they can be used to implement them.
7044 
7045  >>> p1, p2, p3 = Bools('p1 p2 p3')
7046  >>> x, y = Ints('x y')
7047  >>> s = Solver()
7048  >>> s.add(Implies(p1, x > 0))
7049  >>> s.add(Implies(p2, y > x))
7050  >>> s.add(Implies(p2, y < 1))
7051  >>> s.add(Implies(p3, y > -3))
7052  >>> s.check(p1, p2, p3)
7053  unsat
7054  >>> core = s.unsat_core()
7055  >>> len(core)
7056  2
7057  >>> p1 in core
7058  True
7059  >>> p2 in core
7060  True
7061  >>> p3 in core
7062  False
7063  >>> # "Retracting" p2
7064  >>> s.check(p1, p3)
7065  sat
7066  """
7067  return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx)
7068 
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 6796 of file z3py.py.

◆ ctx

ctx

Definition at line 6795 of file z3py.py.

Referenced by Probe.__call__(), Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), Fixedpoint.__del__(), Optimize.__del__(), ApplyResult.__del__(), Tactic.__del__(), Probe.__del__(), Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), ApplyResult.__len__(), Probe.__lt__(), Probe.__ne__(), Fixedpoint.add_cover(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), ApplyResult.as_expr(), Optimize.assert_and_track(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Optimize.assertions(), Optimize.check(), Optimize.from_file(), Optimize.from_string(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_ground_sat_answer(), Fixedpoint.get_num_levels(), Fixedpoint.get_rule_names_along_trace(), Fixedpoint.get_rules(), Fixedpoint.get_rules_along_trace(), Fixedpoint.help(), Optimize.help(), Tactic.help(), Optimize.maximize(), Optimize.minimize(), Optimize.model(), Optimize.objectives(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Optimize.pop(), Optimize.push(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), Fixedpoint.reason_unknown(), Optimize.reason_unknown(), Fixedpoint.register_relation(), Fixedpoint.set(), Optimize.set(), Optimize.set_on_model(), Fixedpoint.set_predicate_representation(), Fixedpoint.sexpr(), Optimize.sexpr(), ApplyResult.sexpr(), Tactic.solver(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), Fixedpoint.to_string(), Optimize.unsat_core(), and Fixedpoint.update_rule().

◆ cube_vs

cube_vs

Definition at line 7113 of file z3py.py.

◆ solver

solver

Definition at line 6797 of file z3py.py.