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

Public Member Functions

def __init__ (self, solver=None, ctx=None)
 
def __deepcopy__ (self, memo={})
 
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 unsat_core (self)
 
def consequences (self, assumptions, variables)
 
def from_file (self, filename)
 
def from_string (self, s)
 
def proof (self)
 
def assertions (self)
 
def statistics (self)
 
def reason_unknown (self)
 
def help (self)
 
def param_descrs (self)
 
def __repr__ (self)
 
def translate (self, target)
 
def sexpr (self)
 
def to_smt2 (self)
 
- Public Member Functions inherited from Z3PPObject
def use_pp (self)
 

Data Fields

 ctx
 
 solver
 

Detailed Description

Solver API provides methods for implementing the main SMT 2.0 commands: push, pop, check, get-model, etc.

Definition at line 6027 of file z3py.py.

Constructor & Destructor Documentation

§ __init__()

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

Definition at line 6030 of file z3py.py.

6030  def __init__(self, solver=None, ctx=None):
6031  assert solver is None or ctx is not None
6032  self.ctx = _get_ctx(ctx)
6033  self.solver = None
6034  if solver is None:
6035  self.solver = Z3_mk_solver(self.ctx.ref())
6036  else:
6037  self.solver = solver
6038  Z3_solver_inc_ref(self.ctx.ref(), self.solver)
6039 
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 6043 of file z3py.py.

6043  def __del__(self):
6044  if self.solver is not None and self.ctx.ref() is not None:
6045  Z3_solver_dec_ref(self.ctx.ref(), self.solver)
6046 
void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s)
Decrement the reference counter of the given solver.

Member Function Documentation

§ __deepcopy__()

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 6040 of file z3py.py.

6040  def __deepcopy__(self, memo={}):
6041  return Solver(self.solver, self.ctx)
6042 

§ __iadd__()

def __iadd__ (   self,
  fml 
)

Definition at line 6165 of file z3py.py.

6165  def __iadd__(self, fml):
6166  self.add(fml)
6167  return self
6168 

§ __repr__()

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

Definition at line 6399 of file z3py.py.

6399  def __repr__(self):
6400  """Return a formatted string with all added constraints."""
6401  return obj_to_string(self)
6402 

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

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

6154  def add(self, *args):
6155  """Assert constraints into the solver.
6156 
6157  >>> x = Int('x')
6158  >>> s = Solver()
6159  >>> s.add(x > 0, x < 2)
6160  >>> s
6161  [x > 0, x < 2]
6162  """
6163  self.assert_exprs(*args)
6164 

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

6169  def append(self, *args):
6170  """Assert constraints into the solver.
6171 
6172  >>> x = Int('x')
6173  >>> s = Solver()
6174  >>> s.append(x > 0, x < 2)
6175  >>> s
6176  [x > 0, x < 2]
6177  """
6178  self.assert_exprs(*args)
6179 

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

6191  def assert_and_track(self, a, p):
6192  """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
6193 
6194  If `p` is a string, it will be automatically converted into a Boolean constant.
6195 
6196  >>> x = Int('x')
6197  >>> p3 = Bool('p3')
6198  >>> s = Solver()
6199  >>> s.set(unsat_core=True)
6200  >>> s.assert_and_track(x > 0, 'p1')
6201  >>> s.assert_and_track(x != 1, 'p2')
6202  >>> s.assert_and_track(x < 0, p3)
6203  >>> print(s.check())
6204  unsat
6205  >>> c = s.unsat_core()
6206  >>> len(c)
6207  2
6208  >>> Bool('p1') in c
6209  True
6210  >>> Bool('p2') in c
6211  False
6212  >>> p3 in c
6213  True
6214  """
6215  if isinstance(p, str):
6216  p = Bool(p, self.ctx)
6217  _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
6218  _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
6219  Z3_solver_assert_and_track(self.ctx.ref(), self.solver, a.as_ast(), p.as_ast())
6220 
def is_const(a)
Definition: z3py.py:1080
def Bool(name, ctx=None)
Definition: z3py.py:1470
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 6135 of file z3py.py.

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

6135  def assert_exprs(self, *args):
6136  """Assert constraints into the solver.
6137 
6138  >>> x = Int('x')
6139  >>> s = Solver()
6140  >>> s.assert_exprs(x > 0, x < 2)
6141  >>> s
6142  [x > 0, x < 2]
6143  """
6144  args = _get_args(args)
6145  s = BoolSort(self.ctx)
6146  for arg in args:
6147  if isinstance(arg, Goal) or isinstance(arg, AstVector):
6148  for f in arg:
6149  Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast())
6150  else:
6151  arg = s.cast(arg)
6152  Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast())
6153 
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:1435

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

Referenced by Solver.to_smt2().

6346  def assertions(self):
6347  """Return an AST vector containing all added constraints.
6348 
6349  >>> s = Solver()
6350  >>> s.assertions()
6351  []
6352  >>> a = Int('a')
6353  >>> s.add(a > 0)
6354  >>> s.add(a < 10)
6355  >>> s.assertions()
6356  [a > 0, a < 10]
6357  """
6358  return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
6359 
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()
[x = 1]
>>> s.add(x < 1)
>>> s.check()
unsat
>>> s.reset()
>>> s.add(2**x == 4)
>>> s.check()
unknown

Definition at line 6221 of file z3py.py.

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

6221  def check(self, *assumptions):
6222  """Check whether the assertions in the given solver plus the optional assumptions are consistent or not.
6223 
6224  >>> x = Int('x')
6225  >>> s = Solver()
6226  >>> s.check()
6227  sat
6228  >>> s.add(x > 0, x < 2)
6229  >>> s.check()
6230  sat
6231  >>> s.model()
6232  [x = 1]
6233  >>> s.add(x < 1)
6234  >>> s.check()
6235  unsat
6236  >>> s.reset()
6237  >>> s.add(2**x == 4)
6238  >>> s.check()
6239  unknown
6240  """
6241  assumptions = _get_args(assumptions)
6242  num = len(assumptions)
6243  _assumptions = (Ast * num)()
6244  for i in range(num):
6245  _assumptions[i] = assumptions[i].as_ast()
6246  r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions)
6247  return CheckSatResult(r)
6248 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2813
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...

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

6300  def consequences(self, assumptions, variables):
6301  """Determine fixed values for the variables based on the solver state and assumptions.
6302  >>> s = Solver()
6303  >>> a, b, c, d = Bools('a b c d')
6304  >>> s.add(Implies(a,b), Implies(b, c))
6305  >>> s.consequences([a],[b,c,d])
6306  (sat, [Implies(a, b), Implies(a, c)])
6307  >>> s.consequences([Not(c),d],[a,b,c,d])
6308  (sat, [Implies(d, d), Implies(Not(c), Not(c)), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))])
6309  """
6310  if isinstance(assumptions, list):
6311  _asms = AstVector(None, self.ctx)
6312  for a in assumptions:
6313  _asms.push(a)
6314  assumptions = _asms
6315  if isinstance(variables, list):
6316  _vars = AstVector(None, self.ctx)
6317  for a in variables:
6318  _vars.push(a)
6319  variables = _vars
6320  _z3_assert(isinstance(assumptions, AstVector), "ast vector expected")
6321  _z3_assert(isinstance(variables, AstVector), "ast vector expected")
6322  consequences = AstVector(None, self.ctx)
6323  r = Z3_solver_get_consequences(self.ctx.ref(), self.solver, assumptions.vector, variables.vector, consequences.vector)
6324  sz = len(consequences)
6325  consequences = [ consequences[i] for i in range(sz) ]
6326  return CheckSatResult(r), consequences
6327 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2813
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.

§ from_file()

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

Definition at line 6328 of file z3py.py.

6328  def from_file(self, filename):
6329  """Parse assertions from a file"""
6330  try:
6331  Z3_solver_from_file(self.ctx.ref(), self.solver, filename)
6332  except Z3Exception as e:
6333  _handle_parse_error(e, self.ctx)
6334 
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 6335 of file z3py.py.

6335  def from_string(self, s):
6336  """Parse assertions from a string"""
6337  try:
6338  Z3_solver_from_string(self.ctx.ref(), self.solver, s)
6339  except Z3Exception as e:
6340  _handle_parse_error(e, self.ctx)
6341 
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 6391 of file z3py.py.

Referenced by Solver.set().

6391  def help(self):
6392  """Display a string describing all available options."""
6393  print(Z3_solver_get_help(self.ctx.ref(), self.solver))
6394 
Z3_string Z3_API Z3_solver_get_help(Z3_context c, Z3_solver s)
Return a string describing all solver available parameters.

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

6180  def insert(self, *args):
6181  """Assert constraints into the solver.
6182 
6183  >>> x = Int('x')
6184  >>> s = Solver()
6185  >>> s.insert(x > 0, x < 2)
6186  >>> s
6187  [x > 0, x < 2]
6188  """
6189  self.assert_exprs(*args)
6190 

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

6249  def model(self):
6250  """Return a model for the last `check()`.
6251 
6252  This function raises an exception if
6253  a model is not available (e.g., last `check()` returned unsat).
6254 
6255  >>> s = Solver()
6256  >>> a = Int('a')
6257  >>> s.add(a + 2 == 0)
6258  >>> s.check()
6259  sat
6260  >>> s.model()
6261  [a = -2]
6262  """
6263  try:
6264  return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx)
6265  except Z3Exception:
6266  raise Z3Exception("model is not available")
6267 
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.

§ num_scopes()

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

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

Definition at line 6103 of file z3py.py.

6103  def num_scopes(self):
6104  """Return the current number of backtracking points.
6105 
6106  >>> s = Solver()
6107  >>> s.num_scopes()
6108  0L
6109  >>> s.push()
6110  >>> s.num_scopes()
6111  1L
6112  >>> s.push()
6113  >>> s.num_scopes()
6114  2L
6115  >>> s.pop()
6116  >>> s.num_scopes()
6117  1L
6118  """
6119  return Z3_solver_get_num_scopes(self.ctx.ref(), self.solver)
6120 
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 6395 of file z3py.py.

6395  def param_descrs(self):
6396  """Return the parameter description set."""
6397  return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx)
6398 
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 6081 of file z3py.py.

6081  def pop(self, num=1):
6082  """Backtrack \c num backtracking points.
6083 
6084  >>> x = Int('x')
6085  >>> s = Solver()
6086  >>> s.add(x > 0)
6087  >>> s
6088  [x > 0]
6089  >>> s.push()
6090  >>> s.add(x < 1)
6091  >>> s
6092  [x > 0, x < 1]
6093  >>> s.check()
6094  unsat
6095  >>> s.pop()
6096  >>> s.check()
6097  sat
6098  >>> s
6099  [x > 0]
6100  """
6101  Z3_solver_pop(self.ctx.ref(), self.solver, num)
6102 
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 6342 of file z3py.py.

6342  def proof(self):
6343  """Return a proof for the last `check()`. Proof construction must be enabled."""
6344  return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
6345 
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 6059 of file z3py.py.

Referenced by Solver.reset().

6059  def push(self):
6060  """Create a backtracking point.
6061 
6062  >>> x = Int('x')
6063  >>> s = Solver()
6064  >>> s.add(x > 0)
6065  >>> s
6066  [x > 0]
6067  >>> s.push()
6068  >>> s.add(x < 1)
6069  >>> s
6070  [x > 0, x < 1]
6071  >>> s.check()
6072  unsat
6073  >>> s.pop()
6074  >>> s.check()
6075  sat
6076  >>> s
6077  [x > 0]
6078  """
6079  Z3_solver_push(self.ctx.ref(), self.solver)
6080 
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 6378 of file z3py.py.

6378  def reason_unknown(self):
6379  """Return a string describing why the last `check()` returned `unknown`.
6380 
6381  >>> x = Int('x')
6382  >>> s = SimpleSolver()
6383  >>> s.add(2**x == 4)
6384  >>> s.check()
6385  unknown
6386  >>> s.reason_unknown()
6387  '(incomplete (theory arithmetic))'
6388  """
6389  return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver)
6390 
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 6121 of file z3py.py.

6121  def reset(self):
6122  """Remove all asserted constraints and backtracking points created using `push()`.
6123 
6124  >>> x = Int('x')
6125  >>> s = Solver()
6126  >>> s.add(x > 0)
6127  >>> s
6128  [x > 0]
6129  >>> s.reset()
6130  >>> s
6131  []
6132  """
6133  Z3_solver_reset(self.ctx.ref(), self.solver)
6134 
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 6047 of file z3py.py.

6047  def set(self, *args, **keys):
6048  """Set a configuration option. The method `help()` return a string containing all available options.
6049 
6050  >>> s = Solver()
6051  >>> # The option MBQI can be set using three different approaches.
6052  >>> s.set(mbqi=True)
6053  >>> s.set('MBQI', True)
6054  >>> s.set(':mbqi', True)
6055  """
6056  p = args2params(args, keys, self.ctx)
6057  Z3_solver_set_params(self.ctx.ref(), self.solver, p.params)
6058 
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:4744

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

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

6416  def sexpr(self):
6417  """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
6418 
6419  >>> x = Int('x')
6420  >>> s = Solver()
6421  >>> s.add(x > 0)
6422  >>> s.add(x < 2)
6423  >>> r = s.sexpr()
6424  """
6425  return Z3_solver_to_string(self.ctx.ref(), self.solver)
6426 
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 6360 of file z3py.py.

6360  def statistics(self):
6361  """Return statistics for the last `check()`.
6362 
6363  >>> s = SimpleSolver()
6364  >>> x = Int('x')
6365  >>> s.add(x > 0)
6366  >>> s.check()
6367  sat
6368  >>> st = s.statistics()
6369  >>> st.get_key_value('final checks')
6370  1
6371  >>> len(st) > 0
6372  True
6373  >>> st[0] != 0
6374  True
6375  """
6376  return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx)
6377 
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 6427 of file z3py.py.

6427  def to_smt2(self):
6428  """return SMTLIB2 formatted benchmark for solver's assertions"""
6429  es = self.assertions()
6430  sz = len(es)
6431  sz1 = sz
6432  if sz1 > 0:
6433  sz1 -= 1
6434  v = (Ast * sz1)()
6435  for i in range(sz1):
6436  v[i] = es[i].as_ast()
6437  if sz > 0:
6438  e = es[sz1].as_ast()
6439  else:
6440  e = BoolVal(True, self.ctx).as_ast()
6441  return Z3_benchmark_to_smtlib_string(self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e)
6442 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2813
def BoolVal(val, ctx=None)
Definition: z3py.py:1452
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.

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

6403  def translate(self, target):
6404  """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
6405 
6406  >>> c1 = Context()
6407  >>> c2 = Context()
6408  >>> s1 = Solver(ctx=c1)
6409  >>> s2 = s1.translate(c2)
6410  """
6411  if __debug__:
6412  _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
6413  solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref())
6414  return Solver(solver, target)
6415 
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 a the context target.

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

6268  def unsat_core(self):
6269  """Return a subset (as an AST vector) of the assumptions provided to the last check().
6270 
6271  These are the assumptions Z3 used in the unsatisfiability proof.
6272  Assumptions are available in Z3. They are used to extract unsatisfiable cores.
6273  They may be also used to "retract" assumptions. Note that, assumptions are not really
6274  "soft constraints", but they can be used to implement them.
6275 
6276  >>> p1, p2, p3 = Bools('p1 p2 p3')
6277  >>> x, y = Ints('x y')
6278  >>> s = Solver()
6279  >>> s.add(Implies(p1, x > 0))
6280  >>> s.add(Implies(p2, y > x))
6281  >>> s.add(Implies(p2, y < 1))
6282  >>> s.add(Implies(p3, y > -3))
6283  >>> s.check(p1, p2, p3)
6284  unsat
6285  >>> core = s.unsat_core()
6286  >>> len(core)
6287  2
6288  >>> p1 in core
6289  True
6290  >>> p2 in core
6291  True
6292  >>> p3 in core
6293  False
6294  >>> # "Retracting" p2
6295  >>> s.check(p1, p3)
6296  sat
6297  """
6298  return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx)
6299 
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

§ ctx

ctx

Definition at line 6032 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(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Optimize.assertions(), Optimize.check(), ApplyResult.convert_model(), 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(), Fixedpoint.pop(), Optimize.pop(), Fixedpoint.push(), Optimize.push(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), Fixedpoint.reason_unknown(), Optimize.reason_unknown(), Fixedpoint.register_relation(), Fixedpoint.set(), Optimize.set(), Fixedpoint.set_predicate_representation(), Fixedpoint.sexpr(), Optimize.sexpr(), ApplyResult.sexpr(), Tactic.solver(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), Fixedpoint.to_string(), and Fixedpoint.update_rule().

§ solver

solver

Definition at line 6033 of file z3py.py.