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

Constructor & Destructor Documentation

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

Definition at line 5778 of file z3py.py.

5778  def __init__(self, solver=None, ctx=None):
5779  assert solver == None or ctx != None
5780  self.ctx = _get_ctx(ctx)
5781  self.solver = None
5782  if solver == None:
5783  self.solver = Z3_mk_solver(self.ctx.ref())
5784  else:
5785  self.solver = solver
5786  Z3_solver_inc_ref(self.ctx.ref(), self.solver)
5787 
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...
void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s)
Increment the reference counter of the given solver.
def __init__(self, solver=None, ctx=None)
Definition: z3py.py:5778
def __del__ (   self)

Definition at line 5788 of file z3py.py.

5788  def __del__(self):
5789  if self.solver != None:
5790  Z3_solver_dec_ref(self.ctx.ref(), self.solver)
5791 
def __del__(self)
Definition: z3py.py:5788
void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s)
Decrement the reference counter of the given solver.

Member Function Documentation

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

Definition at line 6080 of file z3py.py.

6080  def __repr__(self):
6081  """Return a formatted string with all added constraints."""
6082  return obj_to_string(self)
6083 
def __repr__(self)
Definition: z3py.py:6080
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 5881 of file z3py.py.

5881  def add(self, *args):
5882  """Assert constraints into the solver.
5883 
5884  >>> x = Int('x')
5885  >>> s = Solver()
5886  >>> s.add(x > 0, x < 2)
5887  >>> s
5888  [x > 0, x < 2]
5889  """
5890  self.assert_exprs(*args)
5891 
def assert_exprs(self, args)
Definition: z3py.py:5862
def add(self, args)
Definition: z3py.py:5881
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 5892 of file z3py.py.

5892  def append(self, *args):
5893  """Assert constraints into the solver.
5894 
5895  >>> x = Int('x')
5896  >>> s = Solver()
5897  >>> s.append(x > 0, x < 2)
5898  >>> s
5899  [x > 0, x < 2]
5900  """
5901  self.assert_exprs(*args)
5902 
def assert_exprs(self, args)
Definition: z3py.py:5862
def append(self, args)
Definition: z3py.py:5892
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 5914 of file z3py.py.

5914  def assert_and_track(self, a, p):
5915  """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
5916 
5917  If `p` is a string, it will be automatically converted into a Boolean constant.
5918 
5919  >>> x = Int('x')
5920  >>> p3 = Bool('p3')
5921  >>> s = Solver()
5922  >>> s.set(unsat_core=True)
5923  >>> s.assert_and_track(x > 0, 'p1')
5924  >>> s.assert_and_track(x != 1, 'p2')
5925  >>> s.assert_and_track(x < 0, p3)
5926  >>> print(s.check())
5927  unsat
5928  >>> c = s.unsat_core()
5929  >>> len(c)
5930  2
5931  >>> Bool('p1') in c
5932  True
5933  >>> Bool('p2') in c
5934  False
5935  >>> p3 in c
5936  True
5937  """
5938  if isinstance(p, str):
5939  p = Bool(p, self.ctx)
5940  _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
5941  _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
5942  Z3_solver_assert_and_track(self.ctx.ref(), self.solver, a.as_ast(), p.as_ast())
5943 
def is_const(a)
Definition: z3py.py:1006
def assert_and_track(self, a, p)
Definition: z3py.py:5914
def Bool(name, ctx=None)
Definition: z3py.py:1381
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...
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 5862 of file z3py.py.

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

5862  def assert_exprs(self, *args):
5863  """Assert constraints into the solver.
5864 
5865  >>> x = Int('x')
5866  >>> s = Solver()
5867  >>> s.assert_exprs(x > 0, x < 2)
5868  >>> s
5869  [x > 0, x < 2]
5870  """
5871  args = _get_args(args)
5872  s = BoolSort(self.ctx)
5873  for arg in args:
5874  if isinstance(arg, Goal) or isinstance(arg, AstVector):
5875  for f in arg:
5876  Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast())
5877  else:
5878  arg = s.cast(arg)
5879  Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast())
5880 
def assert_exprs(self, args)
Definition: z3py.py:5862
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:1346
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 6027 of file z3py.py.

Referenced by Solver.to_smt2().

6027  def assertions(self):
6028  """Return an AST vector containing all added constraints.
6029 
6030  >>> s = Solver()
6031  >>> s.assertions()
6032  []
6033  >>> a = Int('a')
6034  >>> s.add(a > 0)
6035  >>> s.add(a < 10)
6036  >>> s.assertions()
6037  [a > 0, a < 10]
6038  """
6039  return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
6040 
Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s)
Return the set of asserted formulas as a goal object.
def assertions(self)
Definition: z3py.py:6027
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 5944 of file z3py.py.

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

5944  def check(self, *assumptions):
5945  """Check whether the assertions in the given solver plus the optional assumptions are consistent or not.
5946 
5947  >>> x = Int('x')
5948  >>> s = Solver()
5949  >>> s.check()
5950  sat
5951  >>> s.add(x > 0, x < 2)
5952  >>> s.check()
5953  sat
5954  >>> s.model()
5955  [x = 1]
5956  >>> s.add(x < 1)
5957  >>> s.check()
5958  unsat
5959  >>> s.reset()
5960  >>> s.add(2**x == 4)
5961  >>> s.check()
5962  unknown
5963  """
5964  assumptions = _get_args(assumptions)
5965  num = len(assumptions)
5966  _assumptions = (Ast * num)()
5967  for i in range(num):
5968  _assumptions[i] = assumptions[i].as_ast()
5969  r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions)
5970  return CheckSatResult(r)
5971 
Z3_lbool Z3_API Z3_solver_check_assumptions(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[])
Check whether the assertions in the given solver and optional assumptions are consistent or not...
def check(self, assumptions)
Definition: z3py.py:5944
def help (   self)
Display a string describing all available options.

Definition at line 6072 of file z3py.py.

Referenced by Solver.set().

6072  def help(self):
6073  """Display a string describing all available options."""
6074  print(Z3_solver_get_help(self.ctx.ref(), self.solver))
6075 
def help(self)
Definition: z3py.py:6072
Z3_string Z3_API Z3_solver_get_help(Z3_context c, 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 5903 of file z3py.py.

5903  def insert(self, *args):
5904  """Assert constraints into the solver.
5905 
5906  >>> x = Int('x')
5907  >>> s = Solver()
5908  >>> s.insert(x > 0, x < 2)
5909  >>> s
5910  [x > 0, x < 2]
5911  """
5912  self.assert_exprs(*args)
5913 
def assert_exprs(self, args)
Definition: z3py.py:5862
def insert(self, args)
Definition: z3py.py:5903
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 5972 of file z3py.py.

5972  def model(self):
5973  """Return a model for the last `check()`.
5974 
5975  This function raises an exception if
5976  a model is not available (e.g., last `check()` returned unsat).
5977 
5978  >>> s = Solver()
5979  >>> a = Int('a')
5980  >>> s.add(a + 2 == 0)
5981  >>> s.check()
5982  sat
5983  >>> s.model()
5984  [a = -2]
5985  """
5986  try:
5987  return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx)
5988  except Z3Exception:
5989  raise Z3Exception("model is not available")
5990 
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.
def model(self)
Definition: z3py.py:5972
def param_descrs (   self)
Return the parameter description set.

Definition at line 6076 of file z3py.py.

6076  def param_descrs(self):
6077  """Return the parameter description set."""
6078  return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx)
6079 
def param_descrs(self)
Definition: z3py.py:6076
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.
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 5826 of file z3py.py.

5826  def pop(self, num=1):
5827  """Backtrack \c num backtracking points.
5828 
5829  >>> x = Int('x')
5830  >>> s = Solver()
5831  >>> s.add(x > 0)
5832  >>> s
5833  [x > 0]
5834  >>> s.push()
5835  >>> s.add(x < 1)
5836  >>> s
5837  [x > 0, x < 1]
5838  >>> s.check()
5839  unsat
5840  >>> s.pop()
5841  >>> s.check()
5842  sat
5843  >>> s
5844  [x > 0]
5845  """
5846  Z3_solver_pop(self.ctx.ref(), self.solver, num)
5847 
void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n)
Backtrack n backtracking points.
def pop(self, num=1)
Definition: z3py.py:5826
def proof (   self)
Return a proof for the last `check()`. Proof construction must be enabled.

Definition at line 6023 of file z3py.py.

6023  def proof(self):
6024  """Return a proof for the last `check()`. Proof construction must be enabled."""
6025  return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
6026 
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.
def proof(self)
Definition: z3py.py:6023
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 5804 of file z3py.py.

Referenced by Solver.reset().

5804  def push(self):
5805  """Create a backtracking point.
5806 
5807  >>> x = Int('x')
5808  >>> s = Solver()
5809  >>> s.add(x > 0)
5810  >>> s
5811  [x > 0]
5812  >>> s.push()
5813  >>> s.add(x < 1)
5814  >>> s
5815  [x > 0, x < 1]
5816  >>> s.check()
5817  unsat
5818  >>> s.pop()
5819  >>> s.check()
5820  sat
5821  >>> s
5822  [x > 0]
5823  """
5824  Z3_solver_push(self.ctx.ref(), self.solver)
5825 
void Z3_API Z3_solver_push(Z3_context c, Z3_solver s)
Create a backtracking point.
def push(self)
Definition: z3py.py:5804
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 6059 of file z3py.py.

6059  def reason_unknown(self):
6060  """Return a string describing why the last `check()` returned `unknown`.
6061 
6062  >>> x = Int('x')
6063  >>> s = SimpleSolver()
6064  >>> s.add(2**x == 4)
6065  >>> s.check()
6066  unknown
6067  >>> s.reason_unknown()
6068  '(incomplete (theory arithmetic))'
6069  """
6070  return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver)
6071 
def reason_unknown(self)
Definition: z3py.py:6059
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...
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 5848 of file z3py.py.

5848  def reset(self):
5849  """Remove all asserted constraints and backtracking points created using `push()`.
5850 
5851  >>> x = Int('x')
5852  >>> s = Solver()
5853  >>> s.add(x > 0)
5854  >>> s
5855  [x > 0]
5856  >>> s.reset()
5857  >>> s
5858  []
5859  """
5860  Z3_solver_reset(self.ctx.ref(), self.solver)
5861 
void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)
Remove all assertions from the solver.
def reset(self)
Definition: z3py.py:5848
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 5792 of file z3py.py.

5792  def set(self, *args, **keys):
5793  """Set a configuration option. The method `help()` return a string containing all available options.
5794 
5795  >>> s = Solver()
5796  >>> # The option MBQI can be set using three different approaches.
5797  >>> s.set(mbqi=True)
5798  >>> s.set('MBQI', True)
5799  >>> s.set(':mbqi', True)
5800  """
5801  p = args2params(args, keys, self.ctx)
5802  Z3_solver_set_params(self.ctx.ref(), self.solver, p.params)
5803 
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:4527
def set(self, args, keys)
Definition: z3py.py:5792
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 6084 of file z3py.py.

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

6084  def sexpr(self):
6085  """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
6086 
6087  >>> x = Int('x')
6088  >>> s = Solver()
6089  >>> s.add(x > 0)
6090  >>> s.add(x < 2)
6091  >>> r = s.sexpr()
6092  """
6093  return Z3_solver_to_string(self.ctx.ref(), self.solver)
6094 
def sexpr(self)
Definition: z3py.py:6084
Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s)
Convert a solver into a string.
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 6041 of file z3py.py.

6041  def statistics(self):
6042  """Return statistics for the last `check()`.
6043 
6044  >>> s = SimpleSolver()
6045  >>> x = Int('x')
6046  >>> s.add(x > 0)
6047  >>> s.check()
6048  sat
6049  >>> st = s.statistics()
6050  >>> st.get_key_value('final checks')
6051  1
6052  >>> len(st) > 0
6053  True
6054  >>> st[0] != 0
6055  True
6056  """
6057  return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx)
6058 
Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s)
Return statistics for the given solver.
Statistics.
Definition: z3py.py:5604
def statistics(self)
Definition: z3py.py:6041
def to_smt2 (   self)
return SMTLIB2 formatted benchmark for solver's assertions

Definition at line 6095 of file z3py.py.

6095  def to_smt2(self):
6096  """return SMTLIB2 formatted benchmark for solver's assertions"""
6097  es = self.assertions()
6098  sz = len(es)
6099  sz1 = sz
6100  if sz1 > 0:
6101  sz1 -= 1
6102  v = (Ast * sz1)()
6103  for i in range(sz1):
6104  v[i] = es[i].as_ast()
6105  if sz > 0:
6106  e = es[sz1].as_ast()
6107  else:
6108  e = BoolVal(True, self.ctx).as_ast()
6109  return Z3_benchmark_to_smtlib_string(self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e)
6110 
def to_smt2(self)
Definition: z3py.py:6095
def assertions(self)
Definition: z3py.py:6027
def BoolVal(val, ctx=None)
Definition: z3py.py:1363
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.
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 5991 of file z3py.py.

5991  def unsat_core(self):
5992  """Return a subset (as an AST vector) of the assumptions provided to the last check().
5993 
5994  These are the assumptions Z3 used in the unsatisfiability proof.
5995  Assumptions are available in Z3. They are used to extract unsatisfiable cores.
5996  They may be also used to "retract" assumptions. Note that, assumptions are not really
5997  "soft constraints", but they can be used to implement them.
5998 
5999  >>> p1, p2, p3 = Bools('p1 p2 p3')
6000  >>> x, y = Ints('x y')
6001  >>> s = Solver()
6002  >>> s.add(Implies(p1, x > 0))
6003  >>> s.add(Implies(p2, y > x))
6004  >>> s.add(Implies(p2, y < 1))
6005  >>> s.add(Implies(p3, y > -3))
6006  >>> s.check(p1, p2, p3)
6007  unsat
6008  >>> core = s.unsat_core()
6009  >>> len(core)
6010  2
6011  >>> p1 in core
6012  True
6013  >>> p2 in core
6014  True
6015  >>> p3 in core
6016  False
6017  >>> # "Retracting" p2
6018  >>> s.check(p1, p3)
6019  sat
6020  """
6021  return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx)
6022 
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...
def unsat_core(self)
Definition: z3py.py:5991

Field Documentation

ctx
solver