Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups 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
 
- 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 5624 of file z3py.py.

Constructor & Destructor Documentation

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

Definition at line 5627 of file z3py.py.

5627 
5628  def __init__(self, solver=None, ctx=None):
5629  assert solver == None or ctx != None
5630  self.ctx = _get_ctx(ctx)
5631  self.solver = None
5632  if solver == None:
5633  self.solver = Z3_mk_solver(self.ctx.ref())
5634  else:
5635  self.solver = solver
5636  Z3_solver_inc_ref(self.ctx.ref(), self.solver)
def __del__ (   self)

Definition at line 5637 of file z3py.py.

5637 
5638  def __del__(self):
5639  if self.solver != None:
5640  Z3_solver_dec_ref(self.ctx.ref(), self.solver)

Member Function Documentation

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

Definition at line 5922 of file z3py.py.

5922 
5923  def __repr__(self):
5924  """Return a formatted string with all added constraints."""
5925  return obj_to_string(self)
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 5730 of file z3py.py.

5730 
5731  def add(self, *args):
5732  """Assert constraints into the solver.
5733 
5734  >>> x = Int('x')
5735  >>> s = Solver()
5736  >>> s.add(x > 0, x < 2)
5737  >>> s
5738  [x > 0, x < 2]
5739  """
5740  self.assert_exprs(*args)
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 5741 of file z3py.py.

5741 
5742  def append(self, *args):
5743  """Assert constraints into the solver.
5744 
5745  >>> x = Int('x')
5746  >>> s = Solver()
5747  >>> s.append(x > 0, x < 2)
5748  >>> s
5749  [x > 0, x < 2]
5750  """
5751  self.assert_exprs(*args)
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
>>> print s.unsat_core()
[p3, p1]

Definition at line 5763 of file z3py.py.

5763 
5764  def assert_and_track(self, a, p):
5765  """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
5766 
5767  If `p` is a string, it will be automatically converted into a Boolean constant.
5768 
5769  >>> x = Int('x')
5770  >>> p3 = Bool('p3')
5771  >>> s = Solver()
5772  >>> s.set(unsat_core=True)
5773  >>> s.assert_and_track(x > 0, 'p1')
5774  >>> s.assert_and_track(x != 1, 'p2')
5775  >>> s.assert_and_track(x < 0, p3)
5776  >>> print s.check()
5777  unsat
5778  >>> print s.unsat_core()
5779  [p3, p1]
5780  """
5781  if isinstance(p, str):
5782  p = Bool(p, self.ctx)
5783  _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
5784  _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
5785  Z3_solver_assert_and_track(self.ctx.ref(), self.solver, a.as_ast(), p.as_ast())
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 5711 of file z3py.py.

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

5711 
5712  def assert_exprs(self, *args):
5713  """Assert constraints into the solver.
5714 
5715  >>> x = Int('x')
5716  >>> s = Solver()
5717  >>> s.assert_exprs(x > 0, x < 2)
5718  >>> s
5719  [x > 0, x < 2]
5720  """
5721  args = _get_args(args)
5722  s = BoolSort(self.ctx)
5723  for arg in args:
5724  if isinstance(arg, Goal) or isinstance(arg, AstVector):
5725  for f in arg:
5726  Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast())
5727  else:
5728  arg = s.cast(arg)
5729  Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast())
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 5869 of file z3py.py.

5869 
5870  def assertions(self):
5871  """Return an AST vector containing all added constraints.
5872 
5873  >>> s = Solver()
5874  >>> s.assertions()
5875  []
5876  >>> a = Int('a')
5877  >>> s.add(a > 0)
5878  >>> s.add(a < 10)
5879  >>> s.assertions()
5880  [a > 0, a < 10]
5881  """
5882  return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
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 5786 of file z3py.py.

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

5786 
5787  def check(self, *assumptions):
5788  """Check whether the assertions in the given solver plus the optional assumptions are consistent or not.
5789 
5790  >>> x = Int('x')
5791  >>> s = Solver()
5792  >>> s.check()
5793  sat
5794  >>> s.add(x > 0, x < 2)
5795  >>> s.check()
5796  sat
5797  >>> s.model()
5798  [x = 1]
5799  >>> s.add(x < 1)
5800  >>> s.check()
5801  unsat
5802  >>> s.reset()
5803  >>> s.add(2**x == 4)
5804  >>> s.check()
5805  unknown
5806  """
5807  assumptions = _get_args(assumptions)
5808  num = len(assumptions)
5809  _assumptions = (Ast * num)()
5810  for i in range(num):
5811  _assumptions[i] = assumptions[i].as_ast()
5812  r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions)
5813  return CheckSatResult(r)
def help (   self) 
Display a string describing all available options.

Definition at line 5914 of file z3py.py.

Referenced by Solver.set().

5914 
5915  def help(self):
5916  """Display a string describing all available options."""
5917  print Z3_solver_get_help(self.ctx.ref(), self.solver)
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 5752 of file z3py.py.

5752 
5753  def insert(self, *args):
5754  """Assert constraints into the solver.
5755 
5756  >>> x = Int('x')
5757  >>> s = Solver()
5758  >>> s.insert(x > 0, x < 2)
5759  >>> s
5760  [x > 0, x < 2]
5761  """
5762  self.assert_exprs(*args)
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 5814 of file z3py.py.

5814 
5815  def model(self):
5816  """Return a model for the last `check()`.
5817 
5818  This function raises an exception if
5819  a model is not available (e.g., last `check()` returned unsat).
5820 
5821  >>> s = Solver()
5822  >>> a = Int('a')
5823  >>> s.add(a + 2 == 0)
5824  >>> s.check()
5825  sat
5826  >>> s.model()
5827  [a = -2]
5828  """
5829  try:
5830  return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx)
5831  except Z3Exception:
5832  raise Z3Exception("model is not available")
def param_descrs (   self) 
Return the parameter description set.

Definition at line 5918 of file z3py.py.

5918 
5919  def param_descrs(self):
5920  """Return the parameter description set."""
5921  return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx)
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 5675 of file z3py.py.

5675 
5676  def pop(self, num=1):
5677  """Backtrack \c num backtracking points.
5678 
5679  >>> x = Int('x')
5680  >>> s = Solver()
5681  >>> s.add(x > 0)
5682  >>> s
5683  [x > 0]
5684  >>> s.push()
5685  >>> s.add(x < 1)
5686  >>> s
5687  [x > 0, x < 1]
5688  >>> s.check()
5689  unsat
5690  >>> s.pop()
5691  >>> s.check()
5692  sat
5693  >>> s
5694  [x > 0]
5695  """
5696  Z3_solver_pop(self.ctx.ref(), self.solver, num)
def proof (   self) 
Return a proof for the last `check()`. Proof construction must be enabled.

Definition at line 5865 of file z3py.py.

5865 
5866  def proof(self):
5867  """Return a proof for the last `check()`. Proof construction must be enabled."""
5868  return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
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 5653 of file z3py.py.

Referenced by Solver.reset().

5653 
5654  def push(self):
5655  """Create a backtracking point.
5656 
5657  >>> x = Int('x')
5658  >>> s = Solver()
5659  >>> s.add(x > 0)
5660  >>> s
5661  [x > 0]
5662  >>> s.push()
5663  >>> s.add(x < 1)
5664  >>> s
5665  [x > 0, x < 1]
5666  >>> s.check()
5667  unsat
5668  >>> s.pop()
5669  >>> s.check()
5670  sat
5671  >>> s
5672  [x > 0]
5673  """
5674  Z3_solver_push(self.ctx.ref(), self.solver)
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 5901 of file z3py.py.

5901 
5902  def reason_unknown(self):
5903  """Return a string describing why the last `check()` returned `unknown`.
5904 
5905  >>> x = Int('x')
5906  >>> s = SimpleSolver()
5907  >>> s.add(2**x == 4)
5908  >>> s.check()
5909  unknown
5910  >>> s.reason_unknown()
5911  '(incomplete (theory arithmetic))'
5912  """
5913  return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver)
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 5697 of file z3py.py.

5697 
5698  def reset(self):
5699  """Remove all asserted constraints and backtracking points created using `push()`.
5700 
5701  >>> x = Int('x')
5702  >>> s = Solver()
5703  >>> s.add(x > 0)
5704  >>> s
5705  [x > 0]
5706  >>> s.reset()
5707  >>> s
5708  []
5709  """
5710  Z3_solver_reset(self.ctx.ref(), self.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 5641 of file z3py.py.

5641 
5642  def set(self, *args, **keys):
5643  """Set a configuration option. The method `help()` return a string containing all available options.
5644 
5645  >>> s = Solver()
5646  >>> # The option MBQI can be set using three different approaches.
5647  >>> s.set(mbqi=True)
5648  >>> s.set('MBQI', True)
5649  >>> s.set(':mbqi', True)
5650  """
5651  p = args2params(args, keys, self.ctx)
5652  Z3_solver_set_params(self.ctx.ref(), self.solver, p.params)
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 5926 of file z3py.py.

5926 
5927  def sexpr(self):
5928  """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
5929 
5930  >>> x = Int('x')
5931  >>> s = Solver()
5932  >>> s.add(x > 0)
5933  >>> s.add(x < 2)
5934  >>> r = s.sexpr()
5935  """
5936  return Z3_solver_to_string(self.ctx.ref(), self.solver)
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 5883 of file z3py.py.

5883 
5884  def statistics(self):
5885  """Return statistics for the last `check()`.
5886 
5887  >>> s = SimpleSolver()
5888  >>> x = Int('x')
5889  >>> s.add(x > 0)
5890  >>> s.check()
5891  sat
5892  >>> st = s.statistics()
5893  >>> st.get_key_value('final checks')
5894  1
5895  >>> len(st) > 0
5896  True
5897  >>> st[0] != 0
5898  True
5899  """
5900  return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx)
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 5833 of file z3py.py.

5833 
5834  def unsat_core(self):
5835  """Return a subset (as an AST vector) of the assumptions provided to the last check().
5836 
5837  These are the assumptions Z3 used in the unsatisfiability proof.
5838  Assumptions are available in Z3. They are used to extract unsatisfiable cores.
5839  They may be also used to "retract" assumptions. Note that, assumptions are not really
5840  "soft constraints", but they can be used to implement them.
5841 
5842  >>> p1, p2, p3 = Bools('p1 p2 p3')
5843  >>> x, y = Ints('x y')
5844  >>> s = Solver()
5845  >>> s.add(Implies(p1, x > 0))
5846  >>> s.add(Implies(p2, y > x))
5847  >>> s.add(Implies(p2, y < 1))
5848  >>> s.add(Implies(p3, y > -3))
5849  >>> s.check(p1, p2, p3)
5850  unsat
5851  >>> core = s.unsat_core()
5852  >>> len(core)
5853  2
5854  >>> p1 in core
5855  True
5856  >>> p2 in core
5857  True
5858  >>> p3 in core
5859  False
5860  >>> # "Retracting" p2
5861  >>> s.check(p1, p3)
5862  sat
5863  """
5864  return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx)

Field Documentation

ctx

Definition at line 5629 of file z3py.py.

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

solver

Definition at line 5630 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().

Generated on Thu Nov 22 2012 18:37:33 for Z3 by   doxygen 1.8.2