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

Constructor & Destructor Documentation

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

Definition at line 5741 of file z3py.py.

5741  def __init__(self, solver=None, ctx=None):
5742  assert solver == None or ctx != None
5743  self.ctx = _get_ctx(ctx)
5744  self.solver = None
5745  if solver == None:
5746  self.solver = Z3_mk_solver(self.ctx.ref())
5747  else:
5748  self.solver = solver
5749  Z3_solver_inc_ref(self.ctx.ref(), self.solver)
5750 
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:5741
def __del__ (   self)

Definition at line 5751 of file z3py.py.

5751  def __del__(self):
5752  if self.solver != None:
5753  Z3_solver_dec_ref(self.ctx.ref(), self.solver)
5754 
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:5751

Member Function Documentation

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

Definition at line 6043 of file z3py.py.

6043  def __repr__(self):
6044  """Return a formatted string with all added constraints."""
6045  return obj_to_string(self)
6046 
def __repr__(self)
Definition: z3py.py:6043
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 5844 of file z3py.py.

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

5855  def append(self, *args):
5856  """Assert constraints into the solver.
5857 
5858  >>> x = Int('x')
5859  >>> s = Solver()
5860  >>> s.append(x > 0, x < 2)
5861  >>> s
5862  [x > 0, x < 2]
5863  """
5864  self.assert_exprs(*args)
5865 
def assert_exprs(self, args)
Definition: z3py.py:5825
def append(self, args)
Definition: z3py.py:5855
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 5877 of file z3py.py.

5877  def assert_and_track(self, a, p):
5878  """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
5879 
5880  If `p` is a string, it will be automatically converted into a Boolean constant.
5881 
5882  >>> x = Int('x')
5883  >>> p3 = Bool('p3')
5884  >>> s = Solver()
5885  >>> s.set(unsat_core=True)
5886  >>> s.assert_and_track(x > 0, 'p1')
5887  >>> s.assert_and_track(x != 1, 'p2')
5888  >>> s.assert_and_track(x < 0, p3)
5889  >>> print(s.check())
5890  unsat
5891  >>> c = s.unsat_core()
5892  >>> len(c)
5893  2
5894  >>> Bool('p1') in c
5895  True
5896  >>> Bool('p2') in c
5897  False
5898  >>> p3 in c
5899  True
5900  """
5901  if isinstance(p, str):
5902  p = Bool(p, self.ctx)
5903  _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
5904  _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
5905  Z3_solver_assert_and_track(self.ctx.ref(), self.solver, a.as_ast(), p.as_ast())
5906 
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:1006
def assert_and_track(self, a, p)
Definition: z3py.py:5877
def Bool
Definition: z3py.py:1371
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 5825 of file z3py.py.

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

5825  def assert_exprs(self, *args):
5826  """Assert constraints into the solver.
5827 
5828  >>> x = Int('x')
5829  >>> s = Solver()
5830  >>> s.assert_exprs(x > 0, x < 2)
5831  >>> s
5832  [x > 0, x < 2]
5833  """
5834  args = _get_args(args)
5835  s = BoolSort(self.ctx)
5836  for arg in args:
5837  if isinstance(arg, Goal) or isinstance(arg, AstVector):
5838  for f in arg:
5839  Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast())
5840  else:
5841  arg = s.cast(arg)
5842  Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast())
5843 
def BoolSort
Definition: z3py.py:1336
def assert_exprs(self, args)
Definition: z3py.py:5825
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 5990 of file z3py.py.

Referenced by Solver.to_smt2().

5990  def assertions(self):
5991  """Return an AST vector containing all added constraints.
5992 
5993  >>> s = Solver()
5994  >>> s.assertions()
5995  []
5996  >>> a = Int('a')
5997  >>> s.add(a > 0)
5998  >>> s.add(a < 10)
5999  >>> s.assertions()
6000  [a > 0, a < 10]
6001  """
6002  return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
6003 
def assertions(self)
Definition: z3py.py:5990
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 5907 of file z3py.py.

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

5907  def check(self, *assumptions):
5908  """Check whether the assertions in the given solver plus the optional assumptions are consistent or not.
5909 
5910  >>> x = Int('x')
5911  >>> s = Solver()
5912  >>> s.check()
5913  sat
5914  >>> s.add(x > 0, x < 2)
5915  >>> s.check()
5916  sat
5917  >>> s.model()
5918  [x = 1]
5919  >>> s.add(x < 1)
5920  >>> s.check()
5921  unsat
5922  >>> s.reset()
5923  >>> s.add(2**x == 4)
5924  >>> s.check()
5925  unknown
5926  """
5927  assumptions = _get_args(assumptions)
5928  num = len(assumptions)
5929  _assumptions = (Ast * num)()
5930  for i in range(num):
5931  _assumptions[i] = assumptions[i].as_ast()
5932  r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions)
5933  return CheckSatResult(r)
5934 
def check(self, assumptions)
Definition: z3py.py:5907
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 6035 of file z3py.py.

Referenced by Solver.set().

6035  def help(self):
6036  """Display a string describing all available options."""
6037  print(Z3_solver_get_help(self.ctx.ref(), self.solver))
6038 
def help(self)
Definition: z3py.py:6035
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 5866 of file z3py.py.

5866  def insert(self, *args):
5867  """Assert constraints into the solver.
5868 
5869  >>> x = Int('x')
5870  >>> s = Solver()
5871  >>> s.insert(x > 0, x < 2)
5872  >>> s
5873  [x > 0, x < 2]
5874  """
5875  self.assert_exprs(*args)
5876 
def assert_exprs(self, args)
Definition: z3py.py:5825
def insert(self, args)
Definition: z3py.py:5866
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 5935 of file z3py.py.

5935  def model(self):
5936  """Return a model for the last `check()`.
5937 
5938  This function raises an exception if
5939  a model is not available (e.g., last `check()` returned unsat).
5940 
5941  >>> s = Solver()
5942  >>> a = Int('a')
5943  >>> s.add(a + 2 == 0)
5944  >>> s.check()
5945  sat
5946  >>> s.model()
5947  [a = -2]
5948  """
5949  try:
5950  return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx)
5951  except Z3Exception:
5952  raise Z3Exception("model is not available")
5953 
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:5935
def param_descrs (   self)
Return the parameter description set.

Definition at line 6039 of file z3py.py.

6039  def param_descrs(self):
6040  """Return the parameter description set."""
6041  return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx)
6042 
def param_descrs(self)
Definition: z3py.py:6039
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 5789 of file z3py.py.

5789  def pop(self, num=1):
5790  """Backtrack \c num backtracking points.
5791 
5792  >>> x = Int('x')
5793  >>> s = Solver()
5794  >>> s.add(x > 0)
5795  >>> s
5796  [x > 0]
5797  >>> s.push()
5798  >>> s.add(x < 1)
5799  >>> s
5800  [x > 0, x < 1]
5801  >>> s.check()
5802  unsat
5803  >>> s.pop()
5804  >>> s.check()
5805  sat
5806  >>> s
5807  [x > 0]
5808  """
5809  Z3_solver_pop(self.ctx.ref(), self.solver, num)
5810 
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:5789
def proof (   self)
Return a proof for the last `check()`. Proof construction must be enabled.

Definition at line 5986 of file z3py.py.

5986  def proof(self):
5987  """Return a proof for the last `check()`. Proof construction must be enabled."""
5988  return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
5989 
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:5986
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 5767 of file z3py.py.

Referenced by Solver.reset().

5767  def push(self):
5768  """Create a backtracking point.
5769 
5770  >>> x = Int('x')
5771  >>> s = Solver()
5772  >>> s.add(x > 0)
5773  >>> s
5774  [x > 0]
5775  >>> s.push()
5776  >>> s.add(x < 1)
5777  >>> s
5778  [x > 0, x < 1]
5779  >>> s.check()
5780  unsat
5781  >>> s.pop()
5782  >>> s.check()
5783  sat
5784  >>> s
5785  [x > 0]
5786  """
5787  Z3_solver_push(self.ctx.ref(), self.solver)
5788 
def push(self)
Definition: z3py.py:5767
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 6022 of file z3py.py.

6022  def reason_unknown(self):
6023  """Return a string describing why the last `check()` returned `unknown`.
6024 
6025  >>> x = Int('x')
6026  >>> s = SimpleSolver()
6027  >>> s.add(2**x == 4)
6028  >>> s.check()
6029  unknown
6030  >>> s.reason_unknown()
6031  '(incomplete (theory arithmetic))'
6032  """
6033  return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver)
6034 
def reason_unknown(self)
Definition: z3py.py:6022
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 5811 of file z3py.py.

5811  def reset(self):
5812  """Remove all asserted constraints and backtracking points created using `push()`.
5813 
5814  >>> x = Int('x')
5815  >>> s = Solver()
5816  >>> s.add(x > 0)
5817  >>> s
5818  [x > 0]
5819  >>> s.reset()
5820  >>> s
5821  []
5822  """
5823  Z3_solver_reset(self.ctx.ref(), self.solver)
5824 
def reset(self)
Definition: z3py.py:5811
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 5755 of file z3py.py.

5755  def set(self, *args, **keys):
5756  """Set a configuration option. The method `help()` return a string containing all available options.
5757 
5758  >>> s = Solver()
5759  >>> # The option MBQI can be set using three different approaches.
5760  >>> s.set(mbqi=True)
5761  >>> s.set('MBQI', True)
5762  >>> s.set(':mbqi', True)
5763  """
5764  p = args2params(args, keys, self.ctx)
5765  Z3_solver_set_params(self.ctx.ref(), self.solver, p.params)
5766 
def args2params
Definition: z3py.py:4490
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:5755
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 6047 of file z3py.py.

Referenced by Fixedpoint.__repr__().

6047  def sexpr(self):
6048  """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
6049 
6050  >>> x = Int('x')
6051  >>> s = Solver()
6052  >>> s.add(x > 0)
6053  >>> s.add(x < 2)
6054  >>> r = s.sexpr()
6055  """
6056  return Z3_solver_to_string(self.ctx.ref(), self.solver)
6057 
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:6047
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 6004 of file z3py.py.

6004  def statistics(self):
6005  """Return statistics for the last `check()`.
6006 
6007  >>> s = SimpleSolver()
6008  >>> x = Int('x')
6009  >>> s.add(x > 0)
6010  >>> s.check()
6011  sat
6012  >>> st = s.statistics()
6013  >>> st.get_key_value('final checks')
6014  1
6015  >>> len(st) > 0
6016  True
6017  >>> st[0] != 0
6018  True
6019  """
6020  return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx)
6021 
Statistics.
Definition: z3py.py:5567
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:6004
def to_smt2 (   self)
return SMTLIB2 formatted benchmark for solver's assertions

Definition at line 6058 of file z3py.py.

6058  def to_smt2(self):
6059  """return SMTLIB2 formatted benchmark for solver's assertions"""
6060  es = self.assertions()
6061  sz = len(es)
6062  sz1 = sz
6063  if sz1 > 0:
6064  sz1 -= 1
6065  v = (Ast * sz1)()
6066  for i in range(sz1):
6067  v[i] = es[i].as_ast()
6068  if sz > 0:
6069  e = es[sz1].as_ast()
6070  else:
6071  e = BoolVal(True, self.ctx).as_ast()
6072  return Z3_benchmark_to_smtlib_string(self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e)
6073 
6074 
6075 
def BoolVal
Definition: z3py.py:1353
def to_smt2(self)
Definition: z3py.py:6058
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:5990
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 5954 of file z3py.py.

5954  def unsat_core(self):
5955  """Return a subset (as an AST vector) of the assumptions provided to the last check().
5956 
5957  These are the assumptions Z3 used in the unsatisfiability proof.
5958  Assumptions are available in Z3. They are used to extract unsatisfiable cores.
5959  They may be also used to "retract" assumptions. Note that, assumptions are not really
5960  "soft constraints", but they can be used to implement them.
5961 
5962  >>> p1, p2, p3 = Bools('p1 p2 p3')
5963  >>> x, y = Ints('x y')
5964  >>> s = Solver()
5965  >>> s.add(Implies(p1, x > 0))
5966  >>> s.add(Implies(p2, y > x))
5967  >>> s.add(Implies(p2, y < 1))
5968  >>> s.add(Implies(p3, y > -3))
5969  >>> s.check(p1, p2, p3)
5970  unsat
5971  >>> core = s.unsat_core()
5972  >>> len(core)
5973  2
5974  >>> p1 in core
5975  True
5976  >>> p2 in core
5977  True
5978  >>> p3 in core
5979  False
5980  >>> # "Retracting" p2
5981  >>> s.check(p1, p3)
5982  sat
5983  """
5984  return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx)
5985 
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:5954

Field Documentation

ctx
solver