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

Public Member Functions

def __init__ (self, result, ctx)
 
def __deepcopy__
 
def __del__ (self)
 
def __len__ (self)
 
def __getitem__ (self, idx)
 
def __repr__ (self)
 
def sexpr (self)
 
def as_expr (self)
 
- Public Member Functions inherited from Z3PPObject
def use_pp (self)
 

Data Fields

 result
 
 ctx
 

Detailed Description

An ApplyResult object contains the subgoals produced by a tactic when applied to a goal.
It also contains model and proof converters.

Definition at line 8150 of file z3py.py.

Constructor & Destructor Documentation

def __init__ (   self,
  result,
  ctx 
)

Definition at line 8155 of file z3py.py.

8155  def __init__(self, result, ctx):
8156  self.result = result
8157  self.ctx = ctx
8158  Z3_apply_result_inc_ref(self.ctx.ref(), self.result)
8159 
void Z3_API Z3_apply_result_inc_ref(Z3_context c, Z3_apply_result r)
Increment the reference counter of the given Z3_apply_result object.
def __init__(self, result, ctx)
Definition: z3py.py:8155
def __del__ (   self)

Definition at line 8163 of file z3py.py.

8163  def __del__(self):
8164  if self.ctx.ref() is not None and Z3_apply_result_dec_ref is not None:
8165  Z3_apply_result_dec_ref(self.ctx.ref(), self.result)
8166 
def __del__(self)
Definition: z3py.py:8163
void Z3_API Z3_apply_result_dec_ref(Z3_context c, Z3_apply_result r)
Decrement the reference counter of the given Z3_apply_result object.

Member Function Documentation

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 8160 of file z3py.py.

8160  def __deepcopy__(self, memo={}):
8161  return ApplyResult(self.result, self.ctx)
8162 
def __deepcopy__
Definition: z3py.py:8160
def __getitem__ (   self,
  idx 
)
Return one of the subgoals stored in ApplyResult object `self`.

>>> a, b = Ints('a b')
>>> g = Goal()
>>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b)
>>> t = Tactic('split-clause')
>>> r = t(g)
>>> r[0]
[a == 0, Or(b == 0, b == 1), a > b]
>>> r[1]
[a == 1, Or(b == 0, b == 1), a > b]

Definition at line 8186 of file z3py.py.

8186  def __getitem__(self, idx):
8187  """Return one of the subgoals stored in ApplyResult object `self`.
8188 
8189  >>> a, b = Ints('a b')
8190  >>> g = Goal()
8191  >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b)
8192  >>> t = Tactic('split-clause')
8193  >>> r = t(g)
8194  >>> r[0]
8195  [a == 0, Or(b == 0, b == 1), a > b]
8196  >>> r[1]
8197  [a == 1, Or(b == 0, b == 1), a > b]
8198  """
8199  if idx >= len(self):
8200  raise IndexError
8201  return Goal(goal=Z3_apply_result_get_subgoal(self.ctx.ref(), self.result, idx), ctx=self.ctx)
8202 
def __getitem__(self, idx)
Definition: z3py.py:8186
Z3_goal Z3_API Z3_apply_result_get_subgoal(Z3_context c, Z3_apply_result r, unsigned i)
Return one of the subgoals in the Z3_apply_result object returned by Z3_tactic_apply.
def __len__ (   self)
Return the number of subgoals in `self`.

>>> a, b = Ints('a b')
>>> g = Goal()
>>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b)
>>> t = Tactic('split-clause')
>>> r = t(g)
>>> len(r)
2
>>> t = Then(Tactic('split-clause'), Tactic('split-clause'))
>>> len(t(g))
4
>>> t = Then(Tactic('split-clause'), Tactic('split-clause'), Tactic('propagate-values'))
>>> len(t(g))
1

Definition at line 8167 of file z3py.py.

8167  def __len__(self):
8168  """Return the number of subgoals in `self`.
8169 
8170  >>> a, b = Ints('a b')
8171  >>> g = Goal()
8172  >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b)
8173  >>> t = Tactic('split-clause')
8174  >>> r = t(g)
8175  >>> len(r)
8176  2
8177  >>> t = Then(Tactic('split-clause'), Tactic('split-clause'))
8178  >>> len(t(g))
8179  4
8180  >>> t = Then(Tactic('split-clause'), Tactic('split-clause'), Tactic('propagate-values'))
8181  >>> len(t(g))
8182  1
8183  """
8184  return int(Z3_apply_result_get_num_subgoals(self.ctx.ref(), self.result))
8185 
def __len__(self)
Definition: z3py.py:8167
unsigned Z3_API Z3_apply_result_get_num_subgoals(Z3_context c, Z3_apply_result r)
Return the number of subgoals in the Z3_apply_result object returned by Z3_tactic_apply.
def __repr__ (   self)

Definition at line 8203 of file z3py.py.

8203  def __repr__(self):
8204  return obj_to_string(self)
8205 
def __repr__(self)
Definition: z3py.py:8203
def as_expr (   self)
Return a Z3 expression consisting of all subgoals.

>>> x = Int('x')
>>> g = Goal()
>>> g.add(x > 1)
>>> g.add(Or(x == 2, x == 3))
>>> r = Tactic('simplify')(g)
>>> r
[[Not(x <= 1), Or(x == 2, x == 3)]]
>>> r.as_expr()
And(Not(x <= 1), Or(x == 2, x == 3))
>>> r = Tactic('split-clause')(g)
>>> r
[[x > 1, x == 2], [x > 1, x == 3]]
>>> r.as_expr()
Or(And(x > 1, x == 2), And(x > 1, x == 3))

Definition at line 8210 of file z3py.py.

8210  def as_expr(self):
8211  """Return a Z3 expression consisting of all subgoals.
8212 
8213  >>> x = Int('x')
8214  >>> g = Goal()
8215  >>> g.add(x > 1)
8216  >>> g.add(Or(x == 2, x == 3))
8217  >>> r = Tactic('simplify')(g)
8218  >>> r
8219  [[Not(x <= 1), Or(x == 2, x == 3)]]
8220  >>> r.as_expr()
8221  And(Not(x <= 1), Or(x == 2, x == 3))
8222  >>> r = Tactic('split-clause')(g)
8223  >>> r
8224  [[x > 1, x == 2], [x > 1, x == 3]]
8225  >>> r.as_expr()
8226  Or(And(x > 1, x == 2), And(x > 1, x == 3))
8227  """
8228  sz = len(self)
8229  if sz == 0:
8230  return BoolVal(False, self.ctx)
8231  elif sz == 1:
8232  return self[0].as_expr()
8233  else:
8234  return Or([self[i].as_expr() for i in range(len(self))])
8235 
def BoolVal
Definition: z3py.py:1749
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:4085
def Or(args)
Definition: z3py.py:1922
def as_expr(self)
Definition: z3py.py:8210
def sexpr (   self)
Return a textual representation of the s-expression representing the set of subgoals in `self`.

Definition at line 8206 of file z3py.py.

8206  def sexpr(self):
8207  """Return a textual representation of the s-expression representing the set of subgoals in `self`."""
8208  return Z3_apply_result_to_string(self.ctx.ref(), self.result)
8209 
Z3_string Z3_API Z3_apply_result_to_string(Z3_context c, Z3_apply_result r)
Convert the Z3_apply_result object returned by Z3_tactic_apply into a string.
def sexpr(self)
Definition: z3py.py:8206

Field Documentation

ctx
result