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

Public Member Functions

def __init__ (self, solver=None, ctx=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 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 __copy__ (self)
 
def __deepcopy__ (self)
 
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 6092 of file z3py.py.

Constructor & Destructor Documentation

§ __init__()

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

Definition at line 6095 of file z3py.py.

6095  def __init__(self, solver=None, ctx=None):
6096  assert solver is None or ctx is not None
6097  self.ctx = _get_ctx(ctx)
6098  self.solver = None
6099  if solver is None:
6100  self.solver = Z3_mk_solver(self.ctx.ref())
6101  else:
6102  self.solver = solver
6103  Z3_solver_inc_ref(self.ctx.ref(), self.solver)
6104 
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 6105 of file z3py.py.

6105  def __del__(self):
6106  if self.solver is not None and self.ctx.ref() is not None:
6107  Z3_solver_dec_ref(self.ctx.ref(), self.solver)
6108 
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 6478 of file z3py.py.

6478  def __copy__(self):
6479  return self.translate(self.ctx)
6480 

§ __deepcopy__()

def __deepcopy__ (   self)

Definition at line 6481 of file z3py.py.

6481  def __deepcopy__(self):
6482  return self.translate(self.ctx)
6483 

§ __iadd__()

def __iadd__ (   self,
  fml 
)

Definition at line 6227 of file z3py.py.

6227  def __iadd__(self, fml):
6228  self.add(fml)
6229  return self
6230 

§ __repr__()

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

Definition at line 6461 of file z3py.py.

6461  def __repr__(self):
6462  """Return a formatted string with all added constraints."""
6463  return obj_to_string(self)
6464 

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

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

6216  def add(self, *args):
6217  """Assert constraints into the solver.
6218 
6219  >>> x = Int('x')
6220  >>> s = Solver()
6221  >>> s.add(x > 0, x < 2)
6222  >>> s
6223  [x > 0, x < 2]
6224  """
6225  self.assert_exprs(*args)
6226 

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

6231  def append(self, *args):
6232  """Assert constraints into the solver.
6233 
6234  >>> x = Int('x')
6235  >>> s = Solver()
6236  >>> s.append(x > 0, x < 2)
6237  >>> s
6238  [x > 0, x < 2]
6239  """
6240  self.assert_exprs(*args)
6241 

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

6253  def assert_and_track(self, a, p):
6254  """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
6255 
6256  If `p` is a string, it will be automatically converted into a Boolean constant.
6257 
6258  >>> x = Int('x')
6259  >>> p3 = Bool('p3')
6260  >>> s = Solver()
6261  >>> s.set(unsat_core=True)
6262  >>> s.assert_and_track(x > 0, 'p1')
6263  >>> s.assert_and_track(x != 1, 'p2')
6264  >>> s.assert_and_track(x < 0, p3)
6265  >>> print(s.check())
6266  unsat
6267  >>> c = s.unsat_core()
6268  >>> len(c)
6269  2
6270  >>> Bool('p1') in c
6271  True
6272  >>> Bool('p2') in c
6273  False
6274  >>> p3 in c
6275  True
6276  """
6277  if isinstance(p, str):
6278  p = Bool(p, self.ctx)
6279  _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
6280  _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
6281  Z3_solver_assert_and_track(self.ctx.ref(), self.solver, a.as_ast(), p.as_ast())
6282 
def is_const(a)
Definition: z3py.py:1094
def Bool(name, ctx=None)
Definition: z3py.py:1484
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 6197 of file z3py.py.

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

6197  def assert_exprs(self, *args):
6198  """Assert constraints into the solver.
6199 
6200  >>> x = Int('x')
6201  >>> s = Solver()
6202  >>> s.assert_exprs(x > 0, x < 2)
6203  >>> s
6204  [x > 0, x < 2]
6205  """
6206  args = _get_args(args)
6207  s = BoolSort(self.ctx)
6208  for arg in args:
6209  if isinstance(arg, Goal) or isinstance(arg, AstVector):
6210  for f in arg:
6211  Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast())
6212  else:
6213  arg = s.cast(arg)
6214  Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast())
6215 
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:1449

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

Referenced by Solver.to_smt2().

6408  def assertions(self):
6409  """Return an AST vector containing all added constraints.
6410 
6411  >>> s = Solver()
6412  >>> s.assertions()
6413  []
6414  >>> a = Int('a')
6415  >>> s.add(a > 0)
6416  >>> s.add(a < 10)
6417  >>> s.assertions()
6418  [a > 0, a < 10]
6419  """
6420  return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
6421 
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 6283 of file z3py.py.

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

6283  def check(self, *assumptions):
6284  """Check whether the assertions in the given solver plus the optional assumptions are consistent or not.
6285 
6286  >>> x = Int('x')
6287  >>> s = Solver()
6288  >>> s.check()
6289  sat
6290  >>> s.add(x > 0, x < 2)
6291  >>> s.check()
6292  sat
6293  >>> s.model()
6294  [x = 1]
6295  >>> s.add(x < 1)
6296  >>> s.check()
6297  unsat
6298  >>> s.reset()
6299  >>> s.add(2**x == 4)
6300  >>> s.check()
6301  unknown
6302  """
6303  assumptions = _get_args(assumptions)
6304  num = len(assumptions)
6305  _assumptions = (Ast * num)()
6306  for i in range(num):
6307  _assumptions[i] = assumptions[i].as_ast()
6308  r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions)
6309  return CheckSatResult(r)
6310 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2868
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 6362 of file z3py.py.

6362  def consequences(self, assumptions, variables):
6363  """Determine fixed values for the variables based on the solver state and assumptions.
6364  >>> s = Solver()
6365  >>> a, b, c, d = Bools('a b c d')
6366  >>> s.add(Implies(a,b), Implies(b, c))
6367  >>> s.consequences([a],[b,c,d])
6368  (sat, [Implies(a, b), Implies(a, c)])
6369  >>> s.consequences([Not(c),d],[a,b,c,d])
6370  (sat, [Implies(d, d), Implies(Not(c), Not(c)), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))])
6371  """
6372  if isinstance(assumptions, list):
6373  _asms = AstVector(None, self.ctx)
6374  for a in assumptions:
6375  _asms.push(a)
6376  assumptions = _asms
6377  if isinstance(variables, list):
6378  _vars = AstVector(None, self.ctx)
6379  for a in variables:
6380  _vars.push(a)
6381  variables = _vars
6382  _z3_assert(isinstance(assumptions, AstVector), "ast vector expected")
6383  _z3_assert(isinstance(variables, AstVector), "ast vector expected")
6384  consequences = AstVector(None, self.ctx)
6385  r = Z3_solver_get_consequences(self.ctx.ref(), self.solver, assumptions.vector, variables.vector, consequences.vector)
6386  sz = len(consequences)
6387  consequences = [ consequences[i] for i in range(sz) ]
6388  return CheckSatResult(r), consequences
6389 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2868
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 6390 of file z3py.py.

6390  def from_file(self, filename):
6391  """Parse assertions from a file"""
6392  try:
6393  Z3_solver_from_file(self.ctx.ref(), self.solver, filename)
6394  except Z3Exception as e:
6395  _handle_parse_error(e, self.ctx)
6396 
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 6397 of file z3py.py.

6397  def from_string(self, s):
6398  """Parse assertions from a string"""
6399  try:
6400  Z3_solver_from_string(self.ctx.ref(), self.solver, s)
6401  except Z3Exception as e:
6402  _handle_parse_error(e, self.ctx)
6403 
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 6453 of file z3py.py.

Referenced by Solver.set().

6453  def help(self):
6454  """Display a string describing all available options."""
6455  print(Z3_solver_get_help(self.ctx.ref(), self.solver))
6456 
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 6242 of file z3py.py.

6242  def insert(self, *args):
6243  """Assert constraints into the solver.
6244 
6245  >>> x = Int('x')
6246  >>> s = Solver()
6247  >>> s.insert(x > 0, x < 2)
6248  >>> s
6249  [x > 0, x < 2]
6250  """
6251  self.assert_exprs(*args)
6252 

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

6311  def model(self):
6312  """Return a model for the last `check()`.
6313 
6314  This function raises an exception if
6315  a model is not available (e.g., last `check()` returned unsat).
6316 
6317  >>> s = Solver()
6318  >>> a = Int('a')
6319  >>> s.add(a + 2 == 0)
6320  >>> s.check()
6321  sat
6322  >>> s.model()
6323  [a = -2]
6324  """
6325  try:
6326  return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx)
6327  except Z3Exception:
6328  raise Z3Exception("model is not available")
6329 
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 6165 of file z3py.py.

6165  def num_scopes(self):
6166  """Return the current number of backtracking points.
6167 
6168  >>> s = Solver()
6169  >>> s.num_scopes()
6170  0L
6171  >>> s.push()
6172  >>> s.num_scopes()
6173  1L
6174  >>> s.push()
6175  >>> s.num_scopes()
6176  2L
6177  >>> s.pop()
6178  >>> s.num_scopes()
6179  1L
6180  """
6181  return Z3_solver_get_num_scopes(self.ctx.ref(), self.solver)
6182 
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 6457 of file z3py.py.

6457  def param_descrs(self):
6458  """Return the parameter description set."""
6459  return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx)
6460 
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 6143 of file z3py.py.

6143  def pop(self, num=1):
6144  """Backtrack \c num backtracking points.
6145 
6146  >>> x = Int('x')
6147  >>> s = Solver()
6148  >>> s.add(x > 0)
6149  >>> s
6150  [x > 0]
6151  >>> s.push()
6152  >>> s.add(x < 1)
6153  >>> s
6154  [x > 0, x < 1]
6155  >>> s.check()
6156  unsat
6157  >>> s.pop()
6158  >>> s.check()
6159  sat
6160  >>> s
6161  [x > 0]
6162  """
6163  Z3_solver_pop(self.ctx.ref(), self.solver, num)
6164 
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 6404 of file z3py.py.

6404  def proof(self):
6405  """Return a proof for the last `check()`. Proof construction must be enabled."""
6406  return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
6407 
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 6121 of file z3py.py.

Referenced by Solver.reset().

6121  def push(self):
6122  """Create a backtracking point.
6123 
6124  >>> x = Int('x')
6125  >>> s = Solver()
6126  >>> s.add(x > 0)
6127  >>> s
6128  [x > 0]
6129  >>> s.push()
6130  >>> s.add(x < 1)
6131  >>> s
6132  [x > 0, x < 1]
6133  >>> s.check()
6134  unsat
6135  >>> s.pop()
6136  >>> s.check()
6137  sat
6138  >>> s
6139  [x > 0]
6140  """
6141  Z3_solver_push(self.ctx.ref(), self.solver)
6142 
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 6440 of file z3py.py.

6440  def reason_unknown(self):
6441  """Return a string describing why the last `check()` returned `unknown`.
6442 
6443  >>> x = Int('x')
6444  >>> s = SimpleSolver()
6445  >>> s.add(2**x == 4)
6446  >>> s.check()
6447  unknown
6448  >>> s.reason_unknown()
6449  '(incomplete (theory arithmetic))'
6450  """
6451  return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver)
6452 
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 6183 of file z3py.py.

6183  def reset(self):
6184  """Remove all asserted constraints and backtracking points created using `push()`.
6185 
6186  >>> x = Int('x')
6187  >>> s = Solver()
6188  >>> s.add(x > 0)
6189  >>> s
6190  [x > 0]
6191  >>> s.reset()
6192  >>> s
6193  []
6194  """
6195  Z3_solver_reset(self.ctx.ref(), self.solver)
6196 
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 6109 of file z3py.py.

6109  def set(self, *args, **keys):
6110  """Set a configuration option. The method `help()` return a string containing all available options.
6111 
6112  >>> s = Solver()
6113  >>> # The option MBQI can be set using three different approaches.
6114  >>> s.set(mbqi=True)
6115  >>> s.set('MBQI', True)
6116  >>> s.set(':mbqi', True)
6117  """
6118  p = args2params(args, keys, self.ctx)
6119  Z3_solver_set_params(self.ctx.ref(), self.solver, p.params)
6120 
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:4766

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

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

6484  def sexpr(self):
6485  """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
6486 
6487  >>> x = Int('x')
6488  >>> s = Solver()
6489  >>> s.add(x > 0)
6490  >>> s.add(x < 2)
6491  >>> r = s.sexpr()
6492  """
6493  return Z3_solver_to_string(self.ctx.ref(), self.solver)
6494 
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 6422 of file z3py.py.

6422  def statistics(self):
6423  """Return statistics for the last `check()`.
6424 
6425  >>> s = SimpleSolver()
6426  >>> x = Int('x')
6427  >>> s.add(x > 0)
6428  >>> s.check()
6429  sat
6430  >>> st = s.statistics()
6431  >>> st.get_key_value('final checks')
6432  1
6433  >>> len(st) > 0
6434  True
6435  >>> st[0] != 0
6436  True
6437  """
6438  return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx)
6439 
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 6495 of file z3py.py.

6495  def to_smt2(self):
6496  """return SMTLIB2 formatted benchmark for solver's assertions"""
6497  es = self.assertions()
6498  sz = len(es)
6499  sz1 = sz
6500  if sz1 > 0:
6501  sz1 -= 1
6502  v = (Ast * sz1)()
6503  for i in range(sz1):
6504  v[i] = es[i].as_ast()
6505  if sz > 0:
6506  e = es[sz1].as_ast()
6507  else:
6508  e = BoolVal(True, self.ctx).as_ast()
6509  return Z3_benchmark_to_smtlib_string(self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e)
6510 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2868
def BoolVal(val, ctx=None)
Definition: z3py.py:1466
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 6465 of file z3py.py.

6465  def translate(self, target):
6466  """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
6467 
6468  >>> c1 = Context()
6469  >>> c2 = Context()
6470  >>> s1 = Solver(ctx=c1)
6471  >>> s2 = s1.translate(c2)
6472  """
6473  if __debug__:
6474  _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
6475  solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref())
6476  return Solver(solver, target)
6477 
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.

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

6330  def unsat_core(self):
6331  """Return a subset (as an AST vector) of the assumptions provided to the last check().
6332 
6333  These are the assumptions Z3 used in the unsatisfiability proof.
6334  Assumptions are available in Z3. They are used to extract unsatisfiable cores.
6335  They may be also used to "retract" assumptions. Note that, assumptions are not really
6336  "soft constraints", but they can be used to implement them.
6337 
6338  >>> p1, p2, p3 = Bools('p1 p2 p3')
6339  >>> x, y = Ints('x y')
6340  >>> s = Solver()
6341  >>> s.add(Implies(p1, x > 0))
6342  >>> s.add(Implies(p2, y > x))
6343  >>> s.add(Implies(p2, y < 1))
6344  >>> s.add(Implies(p3, y > -3))
6345  >>> s.check(p1, p2, p3)
6346  unsat
6347  >>> core = s.unsat_core()
6348  >>> len(core)
6349  2
6350  >>> p1 in core
6351  True
6352  >>> p2 in core
6353  True
6354  >>> p3 in core
6355  False
6356  >>> # "Retracting" p2
6357  >>> s.check(p1, p3)
6358  sat
6359  """
6360  return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx)
6361 
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 6097 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 6098 of file z3py.py.