Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules Pages
Public Member Functions | Data Fields
Solver Class Reference
+ Inheritance diagram for Solver:

Public Member Functions

def __init__
 
def __del__
 
def set
 
def push
 
def pop
 
def reset
 
def assert_exprs
 
def add
 
def append
 
def insert
 
def assert_and_track
 
def check
 
def model
 
def unsat_core
 
def proof
 
def assertions
 
def statistics
 
def reason_unknown
 
def help
 
def param_descrs
 
def __repr__
 
def sexpr
 
def to_smt2
 
- Public Member Functions inherited from Z3PPObject
def use_pp
 

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.

5719  def __init__(self, solver=None, ctx=None):
5720  assert solver == None or ctx != None
5721  self.ctx = _get_ctx(ctx)
5722  self.solver = None
5723  if solver == None:
5724  self.solver = Z3_mk_solver(self.ctx.ref())
5725  else:
5726  self.solver = solver
5727  Z3_solver_inc_ref(self.ctx.ref(), self.solver)
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.

5729  def __del__(self):
5730  if self.solver != None:
5731  Z3_solver_dec_ref(self.ctx.ref(), self.solver)
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__
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.

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

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

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

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

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

5968  def assertions(self):
5969  """Return an AST vector containing all added constraints.
5970 
5971  >>> s = Solver()
5972  >>> s.assertions()
5973  []
5974  >>> a = Int('a')
5975  >>> s.add(a > 0)
5976  >>> s.add(a < 10)
5977  >>> s.assertions()
5978  [a > 0, a < 10]
5979  """
5980  return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
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 assertions
Definition: z3py.py:5967
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().

5885  def check(self, *assumptions):
5886  """Check whether the assertions in the given solver plus the optional assumptions are consistent or not.
5887 
5888  >>> x = Int('x')
5889  >>> s = Solver()
5890  >>> s.check()
5891  sat
5892  >>> s.add(x > 0, x < 2)
5893  >>> s.check()
5894  sat
5895  >>> s.model()
5896  [x = 1]
5897  >>> s.add(x < 1)
5898  >>> s.check()
5899  unsat
5900  >>> s.reset()
5901  >>> s.add(2**x == 4)
5902  >>> s.check()
5903  unknown
5904  """
5905  assumptions = _get_args(assumptions)
5906  num = len(assumptions)
5907  _assumptions = (Ast * num)()
5908  for i in range(num):
5909  _assumptions[i] = assumptions[i].as_ast()
5910  r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions)
5911  return CheckSatResult(r)
def check
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().

6013  def help(self):
6014  """Display a string describing all available options."""
6015  print(Z3_solver_get_help(self.ctx.ref(), self.solver))
def help
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.

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

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

Definition at line 6016 of file z3py.py.

6017  def param_descrs(self):
6018  """Return the parameter description set."""
6019  return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx)
def param_descrs
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.

5767  def pop(self, num=1):
5768  """Backtrack \c num backtracking points.
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_pop(self.ctx.ref(), self.solver, num)
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.

5964  def proof(self):
5965  """Return a proof for the last `check()`. Proof construction must be enabled."""
5966  return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
def proof
Definition: z3py.py:5963
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 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().

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

6000  def reason_unknown(self):
6001  """Return a string describing why the last `check()` returned `unknown`.
6002 
6003  >>> x = Int('x')
6004  >>> s = SimpleSolver()
6005  >>> s.add(2**x == 4)
6006  >>> s.check()
6007  unknown
6008  >>> s.reason_unknown()
6009  '(incomplete (theory arithmetic))'
6010  """
6011  return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver)
def reason_unknown
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.

5789  def reset(self):
5790  """Remove all asserted constraints and backtracking points created using `push()`.
5791 
5792  >>> x = Int('x')
5793  >>> s = Solver()
5794  >>> s.add(x > 0)
5795  >>> s
5796  [x > 0]
5797  >>> s.reset()
5798  >>> s
5799  []
5800  """
5801  Z3_solver_reset(self.ctx.ref(), self.solver)
def reset
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.

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

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

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

Definition at line 6035 of file z3py.py.

6036  def to_smt2(self):
6037  """return SMTLIB2 formatted benchmark for solver's assertions"""
6038  es = self.assertions()
6039  sz = len(es)
6040  sz1 = sz
6041  if sz1 > 0:
6042  sz1 -= 1
6043  v = (Ast * sz1)()
6044  for i in range(sz1):
6045  v[i] = es[i].as_ast()
6046  if sz > 0:
6047  e = es[sz1].as_ast()
6048  else:
6049  e = BoolVal(True, self.ctx).as_ast()
6050  return Z3_benchmark_to_smtlib_string(self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e)
6051 
6052 
def BoolVal
Definition: z3py.py:1342
def to_smt2
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
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.

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

Field Documentation

ctx

Definition at line 5720 of file z3py.py.

Referenced by Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), Probe.__ne__(), Fixedpoint.add_rule(), Tactic.apply(), ApplyResult.as_expr(), Solver.assert_and_track(), Solver.assert_exprs(), Fixedpoint.assert_exprs(), Solver.assertions(), ApplyResult.convert_model(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_rules(), Solver.model(), Solver.param_descrs(), Fixedpoint.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Solver.proof(), Solver.set(), Fixedpoint.set(), Tactic.solver(), Solver.statistics(), Fixedpoint.statistics(), Solver.to_smt2(), Solver.unsat_core(), and Fixedpoint.update_rule().

solver

Definition at line 5721 of file z3py.py.

Referenced by Solver.__del__(), Solver.assert_and_track(), Solver.assert_exprs(), Solver.assertions(), Solver.check(), Solver.help(), Solver.model(), Solver.param_descrs(), Solver.pop(), Solver.proof(), Solver.push(), Solver.reason_unknown(), Solver.reset(), Solver.set(), Solver.sexpr(), Solver.statistics(), and Solver.unsat_core().