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

Public Member Functions

def __init__
 
def __del__ (self)
 
def set (self, args, keys)
 
def push (self)
 
def pop
 
def reset (self)
 
def assert_exprs (self, args)
 
def add (self, args)
 
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 proof (self)
 
def assertions (self)
 
def statistics (self)
 
def reason_unknown (self)
 
def help (self)
 
def param_descrs (self)
 
def __repr__ (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 5715 of file z3py.py.

Constructor & Destructor Documentation

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

Definition at line 5718 of file z3py.py.

5718  def __init__(self, solver=None, ctx=None):
5719  assert solver == None or ctx != None
5720  self.ctx = _get_ctx(ctx)
5721  self.solver = None
5722  if solver == None:
5723  self.solver = Z3_mk_solver(self.ctx.ref())
5724  else:
5725  self.solver = solver
5726  Z3_solver_inc_ref(self.ctx.ref(), self.solver)
5727 
void Z3_API Z3_solver_inc_ref(__in Z3_context c, __in Z3_solver s)
Increment the reference counter of the given solver.
Z3_solver Z3_API Z3_mk_solver(__in Z3_context c)
Create a new (incremental) solver. This solver also uses a set of builtin tactics for handling the fi...
def __init__
Definition: z3py.py:5718
def __del__ (   self)

Definition at line 5728 of file z3py.py.

5728  def __del__(self):
5729  if self.solver != None:
5730  Z3_solver_dec_ref(self.ctx.ref(), self.solver)
5731 
void Z3_API Z3_solver_dec_ref(__in Z3_context c, __in Z3_solver s)
Decrement the reference counter of the given solver.
def __del__(self)
Definition: z3py.py:5728

Member Function Documentation

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

Definition at line 6020 of file z3py.py.

6020  def __repr__(self):
6021  """Return a formatted string with all added constraints."""
6022  return obj_to_string(self)
6023 
def __repr__(self)
Definition: z3py.py:6020
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 5821 of file z3py.py.

5821  def add(self, *args):
5822  """Assert constraints into the solver.
5823 
5824  >>> x = Int('x')
5825  >>> s = Solver()
5826  >>> s.add(x > 0, x < 2)
5827  >>> s
5828  [x > 0, x < 2]
5829  """
5830  self.assert_exprs(*args)
5831 
def assert_exprs(self, args)
Definition: z3py.py:5802
def add(self, args)
Definition: z3py.py:5821
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 5832 of file z3py.py.

5832  def append(self, *args):
5833  """Assert constraints into the solver.
5834 
5835  >>> x = Int('x')
5836  >>> s = Solver()
5837  >>> s.append(x > 0, x < 2)
5838  >>> s
5839  [x > 0, x < 2]
5840  """
5841  self.assert_exprs(*args)
5842 
def assert_exprs(self, args)
Definition: z3py.py:5802
def append(self, args)
Definition: z3py.py:5832
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 5854 of file z3py.py.

5854  def assert_and_track(self, a, p):
5855  """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
5856 
5857  If `p` is a string, it will be automatically converted into a Boolean constant.
5858 
5859  >>> x = Int('x')
5860  >>> p3 = Bool('p3')
5861  >>> s = Solver()
5862  >>> s.set(unsat_core=True)
5863  >>> s.assert_and_track(x > 0, 'p1')
5864  >>> s.assert_and_track(x != 1, 'p2')
5865  >>> s.assert_and_track(x < 0, p3)
5866  >>> print(s.check())
5867  unsat
5868  >>> c = s.unsat_core()
5869  >>> len(c)
5870  2
5871  >>> Bool('p1') in c
5872  True
5873  >>> Bool('p2') in c
5874  False
5875  >>> p3 in c
5876  True
5877  """
5878  if isinstance(p, str):
5879  p = Bool(p, self.ctx)
5880  _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
5881  _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
5882  Z3_solver_assert_and_track(self.ctx.ref(), self.solver, a.as_ast(), p.as_ast())
5883 
void Z3_API Z3_solver_assert_and_track(__in Z3_context c, __in Z3_solver s, __in Z3_ast a, __in Z3_ast p)
Assert a constraint a into the solver, and track it (in the unsat) core using the Boolean constant p...
def is_const(a)
Definition: z3py.py:995
def assert_and_track(self, a, p)
Definition: z3py.py:5854
def Bool
Definition: z3py.py:1360
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 5802 of file z3py.py.

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

5802  def assert_exprs(self, *args):
5803  """Assert constraints into the solver.
5804 
5805  >>> x = Int('x')
5806  >>> s = Solver()
5807  >>> s.assert_exprs(x > 0, x < 2)
5808  >>> s
5809  [x > 0, x < 2]
5810  """
5811  args = _get_args(args)
5812  s = BoolSort(self.ctx)
5813  for arg in args:
5814  if isinstance(arg, Goal) or isinstance(arg, AstVector):
5815  for f in arg:
5816  Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast())
5817  else:
5818  arg = s.cast(arg)
5819  Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast())
5820 
def BoolSort
Definition: z3py.py:1325
def assert_exprs(self, args)
Definition: z3py.py:5802
void Z3_API Z3_solver_assert(__in Z3_context c, __in Z3_solver s, __in Z3_ast a)
Assert a constraint into the solver.
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 5967 of file z3py.py.

Referenced by Solver.to_smt2().

5967  def assertions(self):
5968  """Return an AST vector containing all added constraints.
5969 
5970  >>> s = Solver()
5971  >>> s.assertions()
5972  []
5973  >>> a = Int('a')
5974  >>> s.add(a > 0)
5975  >>> s.add(a < 10)
5976  >>> s.assertions()
5977  [a > 0, a < 10]
5978  """
5979  return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
5980 
def assertions(self)
Definition: z3py.py:5967
Z3_ast_vector Z3_API Z3_solver_get_assertions(__in Z3_context c, __in Z3_solver s)
Return the set of asserted formulas as a goal object.
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 5884 of file z3py.py.

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

5884  def check(self, *assumptions):
5885  """Check whether the assertions in the given solver plus the optional assumptions are consistent or not.
5886 
5887  >>> x = Int('x')
5888  >>> s = Solver()
5889  >>> s.check()
5890  sat
5891  >>> s.add(x > 0, x < 2)
5892  >>> s.check()
5893  sat
5894  >>> s.model()
5895  [x = 1]
5896  >>> s.add(x < 1)
5897  >>> s.check()
5898  unsat
5899  >>> s.reset()
5900  >>> s.add(2**x == 4)
5901  >>> s.check()
5902  unknown
5903  """
5904  assumptions = _get_args(assumptions)
5905  num = len(assumptions)
5906  _assumptions = (Ast * num)()
5907  for i in range(num):
5908  _assumptions[i] = assumptions[i].as_ast()
5909  r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions)
5910  return CheckSatResult(r)
5911 
def check(self, assumptions)
Definition: z3py.py:5884
Z3_lbool Z3_API Z3_solver_check_assumptions(__in Z3_context c, __in Z3_solver s, __in unsigned num_assumptions, __in_ecount(num_assumptions) Z3_ast const assumptions[])
Check whether the assertions in the given solver and optional assumptions are consistent or not...
def help (   self)
Display a string describing all available options.

Definition at line 6012 of file z3py.py.

Referenced by Solver.set().

6012  def help(self):
6013  """Display a string describing all available options."""
6014  print(Z3_solver_get_help(self.ctx.ref(), self.solver))
6015 
def help(self)
Definition: z3py.py:6012
Z3_string Z3_API Z3_solver_get_help(__in Z3_context c, __in Z3_solver s)
Return a string describing all solver available parameters.
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 5843 of file z3py.py.

5843  def insert(self, *args):
5844  """Assert constraints into the solver.
5845 
5846  >>> x = Int('x')
5847  >>> s = Solver()
5848  >>> s.insert(x > 0, x < 2)
5849  >>> s
5850  [x > 0, x < 2]
5851  """
5852  self.assert_exprs(*args)
5853 
def assert_exprs(self, args)
Definition: z3py.py:5802
def insert(self, args)
Definition: z3py.py:5843
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 5912 of file z3py.py.

5912  def model(self):
5913  """Return a model for the last `check()`.
5914 
5915  This function raises an exception if
5916  a model is not available (e.g., last `check()` returned unsat).
5917 
5918  >>> s = Solver()
5919  >>> a = Int('a')
5920  >>> s.add(a + 2 == 0)
5921  >>> s.check()
5922  sat
5923  >>> s.model()
5924  [a = -2]
5925  """
5926  try:
5927  return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx)
5928  except Z3Exception:
5929  raise Z3Exception("model is not available")
5930 
Z3_model Z3_API Z3_solver_get_model(__in Z3_context c, __in Z3_solver s)
Retrieve the model for the last Z3_solver_check or Z3_solver_check_assumptions.
def model(self)
Definition: z3py.py:5912
def param_descrs (   self)
Return the parameter description set.

Definition at line 6016 of file z3py.py.

6016  def param_descrs(self):
6017  """Return the parameter description set."""
6018  return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx)
6019 
def param_descrs(self)
Definition: z3py.py:6016
Z3_param_descrs Z3_API Z3_solver_get_param_descrs(__in Z3_context c, __in Z3_solver s)
Return the parameter description set for the given solver object.
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 5766 of file z3py.py.

5766  def pop(self, num=1):
5767  """Backtrack \c num backtracking points.
5768 
5769  >>> x = Int('x')
5770  >>> s = Solver()
5771  >>> s.add(x > 0)
5772  >>> s
5773  [x > 0]
5774  >>> s.push()
5775  >>> s.add(x < 1)
5776  >>> s
5777  [x > 0, x < 1]
5778  >>> s.check()
5779  unsat
5780  >>> s.pop()
5781  >>> s.check()
5782  sat
5783  >>> s
5784  [x > 0]
5785  """
5786  Z3_solver_pop(self.ctx.ref(), self.solver, num)
5787 
void Z3_API Z3_solver_pop(__in Z3_context c, __in Z3_solver s, unsigned n)
Backtrack n backtracking points.
def pop
Definition: z3py.py:5766
def proof (   self)
Return a proof for the last `check()`. Proof construction must be enabled.

Definition at line 5963 of file z3py.py.

5963  def proof(self):
5964  """Return a proof for the last `check()`. Proof construction must be enabled."""
5965  return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
5966 
Z3_ast Z3_API Z3_solver_get_proof(__in Z3_context c, __in Z3_solver s)
Retrieve the proof for the last Z3_solver_check or Z3_solver_check_assumptions.
def proof(self)
Definition: z3py.py:5963
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 5744 of file z3py.py.

Referenced by Solver.reset().

5744  def push(self):
5745  """Create a backtracking point.
5746 
5747  >>> x = Int('x')
5748  >>> s = Solver()
5749  >>> s.add(x > 0)
5750  >>> s
5751  [x > 0]
5752  >>> s.push()
5753  >>> s.add(x < 1)
5754  >>> s
5755  [x > 0, x < 1]
5756  >>> s.check()
5757  unsat
5758  >>> s.pop()
5759  >>> s.check()
5760  sat
5761  >>> s
5762  [x > 0]
5763  """
5764  Z3_solver_push(self.ctx.ref(), self.solver)
5765 
def push(self)
Definition: z3py.py:5744
void Z3_API Z3_solver_push(__in Z3_context c, __in Z3_solver s)
Create a backtracking point.
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 5999 of file z3py.py.

5999  def reason_unknown(self):
6000  """Return a string describing why the last `check()` returned `unknown`.
6001 
6002  >>> x = Int('x')
6003  >>> s = SimpleSolver()
6004  >>> s.add(2**x == 4)
6005  >>> s.check()
6006  unknown
6007  >>> s.reason_unknown()
6008  '(incomplete (theory arithmetic))'
6009  """
6010  return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver)
6011 
def reason_unknown(self)
Definition: z3py.py:5999
Z3_string Z3_API Z3_solver_get_reason_unknown(__in Z3_context c, __in Z3_solver s)
Return a brief justification for an "unknown" result (i.e., Z3_L_UNDEF) for the commands Z3_solver_ch...
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 5788 of file z3py.py.

5788  def reset(self):
5789  """Remove all asserted constraints and backtracking points created using `push()`.
5790 
5791  >>> x = Int('x')
5792  >>> s = Solver()
5793  >>> s.add(x > 0)
5794  >>> s
5795  [x > 0]
5796  >>> s.reset()
5797  >>> s
5798  []
5799  """
5800  Z3_solver_reset(self.ctx.ref(), self.solver)
5801 
def reset(self)
Definition: z3py.py:5788
void Z3_API Z3_solver_reset(__in Z3_context c, __in Z3_solver s)
Remove all assertions from the solver.
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 5732 of file z3py.py.

5732  def set(self, *args, **keys):
5733  """Set a configuration option. The method `help()` return a string containing all available options.
5734 
5735  >>> s = Solver()
5736  >>> # The option MBQI can be set using three different approaches.
5737  >>> s.set(mbqi=True)
5738  >>> s.set('MBQI', True)
5739  >>> s.set(':mbqi', True)
5740  """
5741  p = args2params(args, keys, self.ctx)
5742  Z3_solver_set_params(self.ctx.ref(), self.solver, p.params)
5743 
def args2params
Definition: z3py.py:4467
void Z3_API Z3_solver_set_params(__in Z3_context c, __in Z3_solver s, __in Z3_params p)
Set the given solver using the given parameters.
def set(self, args, keys)
Definition: z3py.py:5732
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 6024 of file z3py.py.

Referenced by Fixedpoint.__repr__().

6024  def sexpr(self):
6025  """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
6026 
6027  >>> x = Int('x')
6028  >>> s = Solver()
6029  >>> s.add(x > 0)
6030  >>> s.add(x < 2)
6031  >>> r = s.sexpr()
6032  """
6033  return Z3_solver_to_string(self.ctx.ref(), self.solver)
6034 
Z3_string Z3_API Z3_solver_to_string(__in Z3_context c, __in Z3_solver s)
Convert a solver into a string.
def sexpr(self)
Definition: z3py.py:6024
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 5981 of file z3py.py.

5981  def statistics(self):
5982  """Return statistics for the last `check()`.
5983 
5984  >>> s = SimpleSolver()
5985  >>> x = Int('x')
5986  >>> s.add(x > 0)
5987  >>> s.check()
5988  sat
5989  >>> st = s.statistics()
5990  >>> st.get_key_value('final checks')
5991  1
5992  >>> len(st) > 0
5993  True
5994  >>> st[0] != 0
5995  True
5996  """
5997  return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx)
5998 
Statistics.
Definition: z3py.py:5544
Z3_stats Z3_API Z3_solver_get_statistics(__in Z3_context c, __in Z3_solver s)
Return statistics for the given solver.
def statistics(self)
Definition: z3py.py:5981
def to_smt2 (   self)
return SMTLIB2 formatted benchmark for solver's assertions

Definition at line 6035 of file z3py.py.

6035  def to_smt2(self):
6036  """return SMTLIB2 formatted benchmark for solver's assertions"""
6037  es = self.assertions()
6038  sz = len(es)
6039  sz1 = sz
6040  if sz1 > 0:
6041  sz1 -= 1
6042  v = (Ast * sz1)()
6043  for i in range(sz1):
6044  v[i] = es[i].as_ast()
6045  if sz > 0:
6046  e = es[sz1].as_ast()
6047  else:
6048  e = BoolVal(True, self.ctx).as_ast()
6049  return Z3_benchmark_to_smtlib_string(self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e)
6050 
6051 
6052 
def BoolVal
Definition: z3py.py:1342
def to_smt2(self)
Definition: z3py.py:6035
Z3_string Z3_API Z3_benchmark_to_smtlib_string(__in Z3_context c, __in Z3_string name, __in Z3_string logic, __in Z3_string status, __in Z3_string attributes, __in unsigned num_assumptions, __in_ecount(num_assumptions) Z3_ast const assumptions[], __in Z3_ast formula)
Convert the given benchmark into SMT-LIB formatted string.
def assertions(self)
Definition: z3py.py:5967
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 5931 of file z3py.py.

5931  def unsat_core(self):
5932  """Return a subset (as an AST vector) of the assumptions provided to the last check().
5933 
5934  These are the assumptions Z3 used in the unsatisfiability proof.
5935  Assumptions are available in Z3. They are used to extract unsatisfiable cores.
5936  They may be also used to "retract" assumptions. Note that, assumptions are not really
5937  "soft constraints", but they can be used to implement them.
5938 
5939  >>> p1, p2, p3 = Bools('p1 p2 p3')
5940  >>> x, y = Ints('x y')
5941  >>> s = Solver()
5942  >>> s.add(Implies(p1, x > 0))
5943  >>> s.add(Implies(p2, y > x))
5944  >>> s.add(Implies(p2, y < 1))
5945  >>> s.add(Implies(p3, y > -3))
5946  >>> s.check(p1, p2, p3)
5947  unsat
5948  >>> core = s.unsat_core()
5949  >>> len(core)
5950  2
5951  >>> p1 in core
5952  True
5953  >>> p2 in core
5954  True
5955  >>> p3 in core
5956  False
5957  >>> # "Retracting" p2
5958  >>> s.check(p1, p3)
5959  sat
5960  """
5961  return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx)
5962 
Z3_ast_vector Z3_API Z3_solver_get_unsat_core(__in Z3_context c, __in Z3_solver s)
Retrieve the unsat core for the last Z3_solver_check_assumptions The unsat core is a subset of the as...
def unsat_core(self)
Definition: z3py.py:5931

Field Documentation

ctx
solver