Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Data Fields
Probe Class Reference

Public Member Functions

def __init__
def __del__
def __lt__
def __gt__
def __le__
def __ge__
def __eq__
def __ne__
def __call__

Data Fields

 ctx
 probe

Detailed Description

Probes are used to inspect a goal (aka problem) and collect information that may be used to decide which solver and/or preprocessing step will be used.

Definition at line 6700 of file z3py.py.


Constructor & Destructor Documentation

def __init__ (   self,
  probe,
  ctx = None 
)

Definition at line 6702 of file z3py.py.

06702 
06703     def __init__(self, probe, ctx=None):
06704         self.ctx    = _get_ctx(ctx)
06705         self.probe  = None
06706         if isinstance(probe, ProbeObj):
06707             self.probe = probe
06708         elif isinstance(probe, float):
06709             self.probe = Z3_probe_const(self.ctx.ref(), probe)
06710         elif _is_int(probe):
06711             self.probe = Z3_probe_const(self.ctx.ref(), float(probe))
06712         elif isinstance(probe, bool):
06713             if probe:
06714                 self.probe = Z3_probe_const(self.ctx.ref(), 1.0)
06715             else:
06716                 self.probe = Z3_probe_const(self.ctx.ref(), 0.0)
06717         else:
06718             if __debug__:
06719                 _z3_assert(isinstance(probe, str), "probe name expected")
06720             try:
06721                 self.probe = Z3_mk_probe(self.ctx.ref(), probe)
06722             except Z3Exception:
06723                 raise Z3Exception("unknown probe '%s'" % probe)
06724         Z3_probe_inc_ref(self.ctx.ref(), self.probe)

def __del__ (   self)

Definition at line 6725 of file z3py.py.

06725 
06726     def __del__(self):
06727         if self.probe != None:
06728             Z3_probe_dec_ref(self.ctx.ref(), self.probe)


Member Function Documentation

def __call__ (   self,
  goal 
)
Evaluate the probe `self` in the given goal.

>>> p = Probe('size')
>>> x = Int('x')
>>> g = Goal()
>>> g.add(x > 0)
>>> g.add(x < 10)
>>> p(g)
2.0
>>> g.add(x < 20)
>>> p(g)
3.0
>>> p = Probe('num-consts')
>>> p(g)
1.0
>>> p = Probe('is-propositional')
>>> p(g)
0.0
>>> p = Probe('is-qflia')
>>> p(g)
1.0

Definition at line 6808 of file z3py.py.

06808 
06809     def __call__(self, goal):
06810         """Evaluate the probe `self` in the given goal.
06811         
06812         >>> p = Probe('size')
06813         >>> x = Int('x')
06814         >>> g = Goal()
06815         >>> g.add(x > 0)
06816         >>> g.add(x < 10)
06817         >>> p(g)
06818         2.0
06819         >>> g.add(x < 20)
06820         >>> p(g)
06821         3.0
06822         >>> p = Probe('num-consts')
06823         >>> p(g)
06824         1.0
06825         >>> p = Probe('is-propositional')
06826         >>> p(g)
06827         0.0
06828         >>> p = Probe('is-qflia')
06829         >>> p(g)
06830         1.0
06831         """
06832         if __debug__:
06833             _z3_assert(isinstance(goal, Goal) or isinstance(goal, BoolRef), "Z3 Goal or Boolean expression expected") 
06834         goal = _to_goal(goal)
06835         return Z3_probe_apply(self.ctx.ref(), self.probe, goal.goal)

def __eq__ (   self,
  other 
)
Return a probe that evaluates to "true" when the value returned by `self` is equal to the value returned by `other`.

>>> p = Probe('size') == 2
>>> x = Int('x')
>>> g = Goal()
>>> g.add(x > 0)
>>> g.add(x < 10)
>>> p(g)
1.0

Definition at line 6781 of file z3py.py.

Referenced by Probe.__ne__().

06781 
06782     def __eq__(self, other):
06783         """Return a probe that evaluates to "true" when the value returned by `self` is equal to the value returned by `other`.
06784 
06785         >>> p = Probe('size') == 2
06786         >>> x = Int('x')
06787         >>> g = Goal()
06788         >>> g.add(x > 0)
06789         >>> g.add(x < 10)
06790         >>> p(g)
06791         1.0
06792         """
06793         return Probe(Z3_probe_eq(self.ctx.ref(), self.probe, _to_probe(other, self.ctx).probe), self.ctx)

def __ge__ (   self,
  other 
)
Return a probe that evaluates to "true" when the value returned by `self` is greater than or equal to the value returned by `other`.

>>> p = Probe('size') >= 2
>>> x = Int('x')
>>> g = Goal()
>>> g.add(x > 0)
>>> g.add(x < 10)
>>> p(g)
1.0

Definition at line 6768 of file z3py.py.

06768 
06769     def __ge__(self, other):
06770         """Return a probe that evaluates to "true" when the value returned by `self` is greater than or equal to the value returned by `other`.
06771 
06772         >>> p = Probe('size') >= 2
06773         >>> x = Int('x')
06774         >>> g = Goal()
06775         >>> g.add(x > 0)
06776         >>> g.add(x < 10)
06777         >>> p(g)
06778         1.0
06779         """
06780         return Probe(Z3_probe_ge(self.ctx.ref(), self.probe, _to_probe(other, self.ctx).probe), self.ctx)

def __gt__ (   self,
  other 
)
Return a probe that evaluates to "true" when the value returned by `self` is greater than the value returned by `other`.

>>> p = Probe('size') > 10
>>> x = Int('x')
>>> g = Goal()
>>> g.add(x > 0)
>>> g.add(x < 10)
>>> p(g)
0.0

Definition at line 6742 of file z3py.py.

06742 
06743     def __gt__(self, other):
06744         """Return a probe that evaluates to "true" when the value returned by `self` is greater than the value returned by `other`.
06745 
06746         >>> p = Probe('size') > 10
06747         >>> x = Int('x')
06748         >>> g = Goal()
06749         >>> g.add(x > 0)
06750         >>> g.add(x < 10)
06751         >>> p(g)
06752         0.0
06753         """
06754         return Probe(Z3_probe_gt(self.ctx.ref(), self.probe, _to_probe(other, self.ctx).probe), self.ctx)

def __le__ (   self,
  other 
)
Return a probe that evaluates to "true" when the value returned by `self` is less than or equal to the value returned by `other`.

>>> p = Probe('size') <= 2
>>> x = Int('x')
>>> g = Goal()
>>> g.add(x > 0)
>>> g.add(x < 10)
>>> p(g)
1.0

Definition at line 6755 of file z3py.py.

06755 
06756     def __le__(self, other):
06757         """Return a probe that evaluates to "true" when the value returned by `self` is less than or equal to the value returned by `other`.
06758 
06759         >>> p = Probe('size') <= 2
06760         >>> x = Int('x')
06761         >>> g = Goal()
06762         >>> g.add(x > 0)
06763         >>> g.add(x < 10)
06764         >>> p(g)
06765         1.0
06766         """
06767         return Probe(Z3_probe_le(self.ctx.ref(), self.probe, _to_probe(other, self.ctx).probe), self.ctx)

def __lt__ (   self,
  other 
)
Return a probe that evaluates to "true" when the value returned by `self` is less than the value returned by `other`.

>>> p = Probe('size') < 10
>>> x = Int('x')
>>> g = Goal()
>>> g.add(x > 0)
>>> g.add(x < 10)
>>> p(g)
1.0

Definition at line 6729 of file z3py.py.

06729 
06730     def __lt__(self, other):
06731         """Return a probe that evaluates to "true" when the value returned by `self` is less than the value returned by `other`.
06732 
06733         >>> p = Probe('size') < 10
06734         >>> x = Int('x')
06735         >>> g = Goal()
06736         >>> g.add(x > 0)
06737         >>> g.add(x < 10)
06738         >>> p(g)
06739         1.0
06740         """
06741         return Probe(Z3_probe_lt(self.ctx.ref(), self.probe, _to_probe(other, self.ctx).probe), self.ctx)

def __ne__ (   self,
  other 
)
Return a probe that evaluates to "true" when the value returned by `self` is not equal to the value returned by `other`.

>>> p = Probe('size') != 2
>>> x = Int('x')
>>> g = Goal()
>>> g.add(x > 0)
>>> g.add(x < 10)
>>> p(g)
0.0

Definition at line 6794 of file z3py.py.

06794 
06795     def __ne__(self, other):
06796         """Return a probe that evaluates to "true" when the value returned by `self` is not equal to the value returned by `other`.
06797 
06798         >>> p = Probe('size') != 2
06799         >>> x = Int('x')
06800         >>> g = Goal()
06801         >>> g.add(x > 0)
06802         >>> g.add(x < 10)
06803         >>> p(g)
06804         0.0
06805         """
06806         p = self.__eq__(other)
06807         return Probe(Z3_probe_not(self.ctx.ref(), p.probe), self.ctx)


Field Documentation

ctx

Definition at line 6702 of file z3py.py.

Referenced by ArithRef::__add__(), BitVecRef::__add__(), BitVecRef::__and__(), FuncDeclRef::__call__(), ArithRef::__div__(), BitVecRef::__div__(), ExprRef::__eq__(), Probe::__eq__(), ArithRef::__ge__(), BitVecRef::__ge__(), Probe::__ge__(), ArrayRef::__getitem__(), ArithRef::__gt__(), BitVecRef::__gt__(), Probe::__gt__(), BitVecRef::__invert__(), ArithRef::__le__(), BitVecRef::__le__(), Probe::__le__(), BitVecRef::__lshift__(), ArithRef::__lt__(), BitVecRef::__lt__(), Probe::__lt__(), ArithRef::__mod__(), BitVecRef::__mod__(), ArithRef::__mul__(), BitVecRef::__mul__(), ExprRef::__ne__(), Probe::__ne__(), ArithRef::__neg__(), BitVecRef::__neg__(), BitVecRef::__or__(), ArithRef::__pow__(), ArithRef::__radd__(), BitVecRef::__radd__(), BitVecRef::__rand__(), ArithRef::__rdiv__(), BitVecRef::__rdiv__(), BitVecRef::__rlshift__(), ArithRef::__rmod__(), BitVecRef::__rmod__(), ArithRef::__rmul__(), BitVecRef::__rmul__(), BitVecRef::__ror__(), ArithRef::__rpow__(), BitVecRef::__rrshift__(), BitVecRef::__rshift__(), ArithRef::__rsub__(), BitVecRef::__rsub__(), BitVecRef::__rxor__(), ArithRef::__sub__(), BitVecRef::__sub__(), BitVecRef::__xor__(), DatatypeSortRef::accessor(), AlgebraicNumRef::approx(), ExprRef::arg(), QuantifierRef::body(), BoolSortRef::cast(), DatatypeSortRef::constructor(), ExprRef::decl(), RatNumRef::denominator(), FuncDeclRef::domain(), ArraySortRef::domain(), SortRef::kind(), SortRef::name(), FuncDeclRef::name(), QuantifierRef::no_pattern(), RatNumRef::numerator(), QuantifierRef::pattern(), FuncDeclRef::range(), ArraySortRef::range(), DatatypeSortRef::recognizer(), ExprRef::sort(), BoolRef::sort(), QuantifierRef::sort(), ArithRef::sort(), BitVecRef::sort(), ArrayRef::sort(), DatatypeRef::sort(), QuantifierRef::var_name(), and QuantifierRef::var_sort().

 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines