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

Constructor & Destructor Documentation

§ __init__()

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

Definition at line 5903 of file z3py.py.

5903  def __init__(self, solver=None, ctx=None):
5904  assert solver is None or ctx is not None
5905  self.ctx = _get_ctx(ctx)
5906  self.solver = None
5907  if solver is None:
5908  self.solver = Z3_mk_solver(self.ctx.ref())
5909  else:
5910  self.solver = solver
5911  Z3_solver_inc_ref(self.ctx.ref(), self.solver)
5912 
void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s)
Increment the reference counter of the given solver.
Z3_solver Z3_API Z3_mk_solver(Z3_context c)
Create a new (incremental) solver. This solver also uses a set of builtin tactics for handling the fi...

§ __del__()

def __del__ (   self)

Definition at line 5913 of file z3py.py.

5913  def __del__(self):
5914  if self.solver is not None and self.ctx.ref() is not None:
5915  Z3_solver_dec_ref(self.ctx.ref(), self.solver)
5916 
void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s)
Decrement the reference counter of the given solver.

Member Function Documentation

§ __iadd__()

def __iadd__ (   self,
  fml 
)

Definition at line 6017 of file z3py.py.

6017  def __iadd__(self, fml):
6018  self.add(fml)
6019  return self
6020 

§ __repr__()

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

Definition at line 6237 of file z3py.py.

6237  def __repr__(self):
6238  """Return a formatted string with all added constraints."""
6239  return obj_to_string(self)
6240 

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

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

6006  def add(self, *args):
6007  """Assert constraints into the solver.
6008 
6009  >>> x = Int('x')
6010  >>> s = Solver()
6011  >>> s.add(x > 0, x < 2)
6012  >>> s
6013  [x > 0, x < 2]
6014  """
6015  self.assert_exprs(*args)
6016 

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

6021  def append(self, *args):
6022  """Assert constraints into the solver.
6023 
6024  >>> x = Int('x')
6025  >>> s = Solver()
6026  >>> s.append(x > 0, x < 2)
6027  >>> s
6028  [x > 0, x < 2]
6029  """
6030  self.assert_exprs(*args)
6031 

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

6043  def assert_and_track(self, a, p):
6044  """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
6045 
6046  If `p` is a string, it will be automatically converted into a Boolean constant.
6047 
6048  >>> x = Int('x')
6049  >>> p3 = Bool('p3')
6050  >>> s = Solver()
6051  >>> s.set(unsat_core=True)
6052  >>> s.assert_and_track(x > 0, 'p1')
6053  >>> s.assert_and_track(x != 1, 'p2')
6054  >>> s.assert_and_track(x < 0, p3)
6055  >>> print(s.check())
6056  unsat
6057  >>> c = s.unsat_core()
6058  >>> len(c)
6059  2
6060  >>> Bool('p1') in c
6061  True
6062  >>> Bool('p2') in c
6063  False
6064  >>> p3 in c
6065  True
6066  """
6067  if isinstance(p, str):
6068  p = Bool(p, self.ctx)
6069  _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
6070  _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
6071  Z3_solver_assert_and_track(self.ctx.ref(), self.solver, a.as_ast(), p.as_ast())
6072 
def is_const(a)
Definition: z3py.py:1054
def Bool(name, ctx=None)
Definition: z3py.py:1442
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 5987 of file z3py.py.

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

5987  def assert_exprs(self, *args):
5988  """Assert constraints into the solver.
5989 
5990  >>> x = Int('x')
5991  >>> s = Solver()
5992  >>> s.assert_exprs(x > 0, x < 2)
5993  >>> s
5994  [x > 0, x < 2]
5995  """
5996  args = _get_args(args)
5997  s = BoolSort(self.ctx)
5998  for arg in args:
5999  if isinstance(arg, Goal) or isinstance(arg, AstVector):
6000  for f in arg:
6001  Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast())
6002  else:
6003  arg = s.cast(arg)
6004  Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast())
6005 
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:1407

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

Referenced by Solver.to_smt2().

6184  def assertions(self):
6185  """Return an AST vector containing all added constraints.
6186 
6187  >>> s = Solver()
6188  >>> s.assertions()
6189  []
6190  >>> a = Int('a')
6191  >>> s.add(a > 0)
6192  >>> s.add(a < 10)
6193  >>> s.assertions()
6194  [a > 0, a < 10]
6195  """
6196  return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
6197 
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 6073 of file z3py.py.

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

6073  def check(self, *assumptions):
6074  """Check whether the assertions in the given solver plus the optional assumptions are consistent or not.
6075 
6076  >>> x = Int('x')
6077  >>> s = Solver()
6078  >>> s.check()
6079  sat
6080  >>> s.add(x > 0, x < 2)
6081  >>> s.check()
6082  sat
6083  >>> s.model()
6084  [x = 1]
6085  >>> s.add(x < 1)
6086  >>> s.check()
6087  unsat
6088  >>> s.reset()
6089  >>> s.add(2**x == 4)
6090  >>> s.check()
6091  unknown
6092  """
6093  assumptions = _get_args(assumptions)
6094  num = len(assumptions)
6095  _assumptions = (Ast * num)()
6096  for i in range(num):
6097  _assumptions[i] = assumptions[i].as_ast()
6098  r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions)
6099  return CheckSatResult(r)
6100 
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(Not(c), Not(c)), Implies(d, d), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))])

Definition at line 6152 of file z3py.py.

6152  def consequences(self, assumptions, variables):
6153  """Determine fixed values for the variables based on the solver state and assumptions.
6154  >>> s = Solver()
6155  >>> a, b, c, d = Bools('a b c d')
6156  >>> s.add(Implies(a,b), Implies(b, c))
6157  >>> s.consequences([a],[b,c,d])
6158  (sat, [Implies(a, b), Implies(a, c)])
6159  >>> s.consequences([Not(c),d],[a,b,c,d])
6160  (sat, [Implies(Not(c), Not(c)), Implies(d, d), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))])
6161  """
6162  if isinstance(assumptions, list):
6163  _asms = AstVector(None, self.ctx)
6164  for a in assumptions:
6165  _asms.push(a)
6166  assumptions = _asms
6167  if isinstance(variables, list):
6168  _vars = AstVector(None, self.ctx)
6169  for a in variables:
6170  _vars.push(a)
6171  variables = _vars
6172  _z3_assert(isinstance(assumptions, AstVector), "ast vector expected")
6173  _z3_assert(isinstance(variables, AstVector), "ast vector expected")
6174  consequences = AstVector(None, self.ctx)
6175  r = Z3_solver_get_consequences(self.ctx.ref(), self.solver, assumptions.vector, variables.vector, consequences.vector)
6176  sz = len(consequences)
6177  consequences = [ consequences[i] for i in range(sz) ]
6178  return CheckSatResult(r), consequences
6179 
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.

§ help()

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

Definition at line 6229 of file z3py.py.

Referenced by Solver.set().

6229  def help(self):
6230  """Display a string describing all available options."""
6231  print(Z3_solver_get_help(self.ctx.ref(), self.solver))
6232 
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 6032 of file z3py.py.

6032  def insert(self, *args):
6033  """Assert constraints into the solver.
6034 
6035  >>> x = Int('x')
6036  >>> s = Solver()
6037  >>> s.insert(x > 0, x < 2)
6038  >>> s
6039  [x > 0, x < 2]
6040  """
6041  self.assert_exprs(*args)
6042 

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

6101  def model(self):
6102  """Return a model for the last `check()`.
6103 
6104  This function raises an exception if
6105  a model is not available (e.g., last `check()` returned unsat).
6106 
6107  >>> s = Solver()
6108  >>> a = Int('a')
6109  >>> s.add(a + 2 == 0)
6110  >>> s.check()
6111  sat
6112  >>> s.model()
6113  [a = -2]
6114  """
6115  try:
6116  return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx)
6117  except Z3Exception:
6118  raise Z3Exception("model is not available")
6119 
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.

§ param_descrs()

def param_descrs (   self)
Return the parameter description set.

Definition at line 6233 of file z3py.py.

6233  def param_descrs(self):
6234  """Return the parameter description set."""
6235  return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx)
6236 
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 5951 of file z3py.py.

5951  def pop(self, num=1):
5952  """Backtrack \c num backtracking points.
5953 
5954  >>> x = Int('x')
5955  >>> s = Solver()
5956  >>> s.add(x > 0)
5957  >>> s
5958  [x > 0]
5959  >>> s.push()
5960  >>> s.add(x < 1)
5961  >>> s
5962  [x > 0, x < 1]
5963  >>> s.check()
5964  unsat
5965  >>> s.pop()
5966  >>> s.check()
5967  sat
5968  >>> s
5969  [x > 0]
5970  """
5971  Z3_solver_pop(self.ctx.ref(), self.solver, num)
5972 
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 6180 of file z3py.py.

6180  def proof(self):
6181  """Return a proof for the last `check()`. Proof construction must be enabled."""
6182  return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
6183 
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 5929 of file z3py.py.

Referenced by Solver.reset().

5929  def push(self):
5930  """Create a backtracking point.
5931 
5932  >>> x = Int('x')
5933  >>> s = Solver()
5934  >>> s.add(x > 0)
5935  >>> s
5936  [x > 0]
5937  >>> s.push()
5938  >>> s.add(x < 1)
5939  >>> s
5940  [x > 0, x < 1]
5941  >>> s.check()
5942  unsat
5943  >>> s.pop()
5944  >>> s.check()
5945  sat
5946  >>> s
5947  [x > 0]
5948  """
5949  Z3_solver_push(self.ctx.ref(), self.solver)
5950 
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 6216 of file z3py.py.

6216  def reason_unknown(self):
6217  """Return a string describing why the last `check()` returned `unknown`.
6218 
6219  >>> x = Int('x')
6220  >>> s = SimpleSolver()
6221  >>> s.add(2**x == 4)
6222  >>> s.check()
6223  unknown
6224  >>> s.reason_unknown()
6225  '(incomplete (theory arithmetic))'
6226  """
6227  return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver)
6228 
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 5973 of file z3py.py.

5973  def reset(self):
5974  """Remove all asserted constraints and backtracking points created using `push()`.
5975 
5976  >>> x = Int('x')
5977  >>> s = Solver()
5978  >>> s.add(x > 0)
5979  >>> s
5980  [x > 0]
5981  >>> s.reset()
5982  >>> s
5983  []
5984  """
5985  Z3_solver_reset(self.ctx.ref(), self.solver)
5986 
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 5917 of file z3py.py.

5917  def set(self, *args, **keys):
5918  """Set a configuration option. The method `help()` return a string containing all available options.
5919 
5920  >>> s = Solver()
5921  >>> # The option MBQI can be set using three different approaches.
5922  >>> s.set(mbqi=True)
5923  >>> s.set('MBQI', True)
5924  >>> s.set(':mbqi', True)
5925  """
5926  p = args2params(args, keys, self.ctx)
5927  Z3_solver_set_params(self.ctx.ref(), self.solver, p.params)
5928 
def args2params(arguments, keywords, ctx=None)
Definition: z3py.py:4644
void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p)
Set the given solver using the given parameters.

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

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

6254  def sexpr(self):
6255  """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
6256 
6257  >>> x = Int('x')
6258  >>> s = Solver()
6259  >>> s.add(x > 0)
6260  >>> s.add(x < 2)
6261  >>> r = s.sexpr()
6262  """
6263  return Z3_solver_to_string(self.ctx.ref(), self.solver)
6264 
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 6198 of file z3py.py.

6198  def statistics(self):
6199  """Return statistics for the last `check()`.
6200 
6201  >>> s = SimpleSolver()
6202  >>> x = Int('x')
6203  >>> s.add(x > 0)
6204  >>> s.check()
6205  sat
6206  >>> st = s.statistics()
6207  >>> st.get_key_value('final checks')
6208  1
6209  >>> len(st) > 0
6210  True
6211  >>> st[0] != 0
6212  True
6213  """
6214  return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx)
6215 
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 6265 of file z3py.py.

6265  def to_smt2(self):
6266  """return SMTLIB2 formatted benchmark for solver's assertions"""
6267  es = self.assertions()
6268  sz = len(es)
6269  sz1 = sz
6270  if sz1 > 0:
6271  sz1 -= 1
6272  v = (Ast * sz1)()
6273  for i in range(sz1):
6274  v[i] = es[i].as_ast()
6275  if sz > 0:
6276  e = es[sz1].as_ast()
6277  else:
6278  e = BoolVal(True, self.ctx).as_ast()
6279  return Z3_benchmark_to_smtlib_string(self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e)
6280 
def BoolVal(val, ctx=None)
Definition: z3py.py:1424
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 6241 of file z3py.py.

6241  def translate(self, target):
6242  """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
6243 
6244  >>> c1 = Context()
6245  >>> c2 = Context()
6246  >>> s1 = Solver(ctx=c1)
6247  >>> s2 = s1.translate(c2)
6248  """
6249  if __debug__:
6250  _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
6251  solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref())
6252  return Solver(solver, target)
6253 
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 6120 of file z3py.py.

6120  def unsat_core(self):
6121  """Return a subset (as an AST vector) of the assumptions provided to the last check().
6122 
6123  These are the assumptions Z3 used in the unsatisfiability proof.
6124  Assumptions are available in Z3. They are used to extract unsatisfiable cores.
6125  They may be also used to "retract" assumptions. Note that, assumptions are not really
6126  "soft constraints", but they can be used to implement them.
6127 
6128  >>> p1, p2, p3 = Bools('p1 p2 p3')
6129  >>> x, y = Ints('x y')
6130  >>> s = Solver()
6131  >>> s.add(Implies(p1, x > 0))
6132  >>> s.add(Implies(p2, y > x))
6133  >>> s.add(Implies(p2, y < 1))
6134  >>> s.add(Implies(p3, y > -3))
6135  >>> s.check(p1, p2, p3)
6136  unsat
6137  >>> core = s.unsat_core()
6138  >>> len(core)
6139  2
6140  >>> p1 in core
6141  True
6142  >>> p2 in core
6143  True
6144  >>> p3 in core
6145  False
6146  >>> # "Retracting" p2
6147  >>> s.check(p1, p3)
6148  sat
6149  """
6150  return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx)
6151 
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

§ solver

solver

Definition at line 5906 of file z3py.py.