Z3
 
Loading...
Searching...
No Matches
ApplyResult Class Reference
+ Inheritance diagram for ApplyResult:

Public Member Functions

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

Data Fields

 result = result
 
 ctx = ctx
 

Additional Inherited Members

- Protected Member Functions inherited from Z3PPObject
 _repr_html_ (self)
 

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

Constructor & Destructor Documentation

◆ __init__()

__init__ ( self,
result,
ctx )

Definition at line 8265 of file z3py.py.

8265 def __init__(self, result, ctx):
8266 self.result = result
8267 self.ctx = ctx
8268 Z3_apply_result_inc_ref(self.ctx.ref(), self.result)
8269
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.

◆ __del__()

__del__ ( self)

Definition at line 8273 of file z3py.py.

8273 def __del__(self):
8274 if self.ctx.ref() is not None and Z3_apply_result_dec_ref is not None:
8275 Z3_apply_result_dec_ref(self.ctx.ref(), self.result)
8276
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

◆ __deepcopy__()

__deepcopy__ ( self,
memo = {} )

Definition at line 8270 of file z3py.py.

8270 def __deepcopy__(self, memo={}):
8271 return ApplyResult(self.result, self.ctx)
8272

◆ __getitem__()

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

8296 def __getitem__(self, idx):
8297 """Return one of the subgoals stored in ApplyResult object `self`.
8298
8299 >>> a, b = Ints('a b')
8300 >>> g = Goal()
8301 >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b)
8302 >>> t = Tactic('split-clause')
8303 >>> r = t(g)
8304 >>> r[0]
8305 [a == 0, Or(b == 0, b == 1), a > b]
8306 >>> r[1]
8307 [a == 1, Or(b == 0, b == 1), a > b]
8308 """
8309 if idx >= len(self):
8310 raise IndexError
8311 return Goal(goal=Z3_apply_result_get_subgoal(self.ctx.ref(), self.result, idx), ctx=self.ctx)
8312
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.

◆ __len__()

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

8277 def __len__(self):
8278 """Return the number of subgoals in `self`.
8279
8280 >>> a, b = Ints('a b')
8281 >>> g = Goal()
8282 >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b)
8283 >>> t = Tactic('split-clause')
8284 >>> r = t(g)
8285 >>> len(r)
8286 2
8287 >>> t = Then(Tactic('split-clause'), Tactic('split-clause'))
8288 >>> len(t(g))
8289 4
8290 >>> t = Then(Tactic('split-clause'), Tactic('split-clause'), Tactic('propagate-values'))
8291 >>> len(t(g))
8292 1
8293 """
8294 return int(Z3_apply_result_get_num_subgoals(self.ctx.ref(), self.result))
8295
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.

◆ __repr__()

__repr__ ( self)

Definition at line 8313 of file z3py.py.

8313 def __repr__(self):
8314 return obj_to_string(self)
8315

◆ as_expr()

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

8320 def as_expr(self):
8321 """Return a Z3 expression consisting of all subgoals.
8322
8323 >>> x = Int('x')
8324 >>> g = Goal()
8325 >>> g.add(x > 1)
8326 >>> g.add(Or(x == 2, x == 3))
8327 >>> r = Tactic('simplify')(g)
8328 >>> r
8329 [[Not(x <= 1), Or(x == 2, x == 3)]]
8330 >>> r.as_expr()
8331 And(Not(x <= 1), Or(x == 2, x == 3))
8332 >>> r = Tactic('split-clause')(g)
8333 >>> r
8334 [[x > 1, x == 2], [x > 1, x == 3]]
8335 >>> r.as_expr()
8336 Or(And(x > 1, x == 2), And(x > 1, x == 3))
8337 """
8338 sz = len(self)
8339 if sz == 0:
8340 return BoolVal(False, self.ctx)
8341 elif sz == 1:
8342 return self[0].as_expr()
8343 else:
8344 return Or([self[i].as_expr() for i in range(len(self))])
8345

◆ sexpr()

sexpr ( self)
Return a textual representation of the s-expression representing the set of subgoals in `self`.

Definition at line 8316 of file z3py.py.

8316 def sexpr(self):
8317 """Return a textual representation of the s-expression representing the set of subgoals in `self`."""
8318 return Z3_apply_result_to_string(self.ctx.ref(), self.result)
8319
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.

Field Documentation

◆ ctx

ctx = ctx

Definition at line 8267 of file z3py.py.

◆ result

result = result

Definition at line 8266 of file z3py.py.