Z3
 
Loading...
Searching...
No Matches
Probe Class Reference

Public Member Functions

 __init__ (self, probe, ctx=None)
 
 __deepcopy__ (self, memo={})
 
 __del__ (self)
 
 __lt__ (self, other)
 
 __gt__ (self, other)
 
 __le__ (self, other)
 
 __ge__ (self, other)
 
 __eq__ (self, other)
 
 __ne__ (self, other)
 
 __call__ (self, goal)
 

Data Fields

 ctx = _get_ctx(ctx)
 
 probe = None
 

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

Constructor & Destructor Documentation

◆ __init__()

__init__ ( self,
probe,
ctx = None )

Definition at line 8673 of file z3py.py.

8673 def __init__(self, probe, ctx=None):
8674 self.ctx = _get_ctx(ctx)
8675 self.probe = None
8676 if isinstance(probe, ProbeObj):
8677 self.probe = probe
8678 elif isinstance(probe, float):
8679 self.probe = Z3_probe_const(self.ctx.ref(), probe)
8680 elif _is_int(probe):
8681 self.probe = Z3_probe_const(self.ctx.ref(), float(probe))
8682 elif isinstance(probe, bool):
8683 if probe:
8684 self.probe = Z3_probe_const(self.ctx.ref(), 1.0)
8685 else:
8686 self.probe = Z3_probe_const(self.ctx.ref(), 0.0)
8687 else:
8688 if z3_debug():
8689 _z3_assert(isinstance(probe, str), "probe name expected")
8690 try:
8691 self.probe = Z3_mk_probe(self.ctx.ref(), probe)
8692 except Z3Exception:
8693 raise Z3Exception("unknown probe '%s'" % probe)
8694 Z3_probe_inc_ref(self.ctx.ref(), self.probe)
8695
Z3_probe Z3_API Z3_mk_probe(Z3_context c, Z3_string name)
Return a probe associated with the given name. The complete list of probes may be obtained using the ...
void Z3_API Z3_probe_inc_ref(Z3_context c, Z3_probe p)
Increment the reference counter of the given probe.
Z3_probe Z3_API Z3_probe_const(Z3_context x, double val)
Return a probe that always evaluates to val.

◆ __del__()

__del__ ( self)

Definition at line 8699 of file z3py.py.

8699 def __del__(self):
8700 if self.probe is not None and self.ctx.ref() is not None and Z3_probe_dec_ref is not None:
8701 Z3_probe_dec_ref(self.ctx.ref(), self.probe)
8702
void Z3_API Z3_probe_dec_ref(Z3_context c, Z3_probe p)
Decrement the reference counter of the given probe.

Member Function Documentation

◆ __call__()

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

8788 def __call__(self, goal):
8789 """Evaluate the probe `self` in the given goal.
8790
8791 >>> p = Probe('size')
8792 >>> x = Int('x')
8793 >>> g = Goal()
8794 >>> g.add(x > 0)
8795 >>> g.add(x < 10)
8796 >>> p(g)
8797 2.0
8798 >>> g.add(x < 20)
8799 >>> p(g)
8800 3.0
8801 >>> p = Probe('num-consts')
8802 >>> p(g)
8803 1.0
8804 >>> p = Probe('is-propositional')
8805 >>> p(g)
8806 0.0
8807 >>> p = Probe('is-qflia')
8808 >>> p(g)
8809 1.0
8810 """
8811 if z3_debug():
8812 _z3_assert(isinstance(goal, (Goal, BoolRef)), "Z3 Goal or Boolean expression expected")
8813 goal = _to_goal(goal)
8814 return Z3_probe_apply(self.ctx.ref(), self.probe, goal.goal)
8815
8816
double Z3_API Z3_probe_apply(Z3_context c, Z3_probe p, Z3_goal g)
Execute the probe over the goal. The probe always produce a double value. "Boolean" probes return 0....

◆ __deepcopy__()

__deepcopy__ ( self,
memo = {} )

Definition at line 8696 of file z3py.py.

8696 def __deepcopy__(self, memo={}):
8697 return Probe(self.probe, self.ctx)
8698

◆ __eq__()

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

8759 def __eq__(self, other):
8760 """Return a probe that evaluates to "true" when the value returned by `self`
8761 is equal to the value returned by `other`.
8762
8763 >>> p = Probe('size') == 2
8764 >>> x = Int('x')
8765 >>> g = Goal()
8766 >>> g.add(x > 0)
8767 >>> g.add(x < 10)
8768 >>> p(g)
8769 1.0
8770 """
8771 return Probe(Z3_probe_eq(self.ctx.ref(), self.probe, _to_probe(other, self.ctx).probe), self.ctx)
8772
Z3_probe Z3_API Z3_probe_eq(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is equal to the value returned ...

◆ __ge__()

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

8745 def __ge__(self, other):
8746 """Return a probe that evaluates to "true" when the value returned by `self`
8747 is greater than or equal to the value returned by `other`.
8748
8749 >>> p = Probe('size') >= 2
8750 >>> x = Int('x')
8751 >>> g = Goal()
8752 >>> g.add(x > 0)
8753 >>> g.add(x < 10)
8754 >>> p(g)
8755 1.0
8756 """
8757 return Probe(Z3_probe_ge(self.ctx.ref(), self.probe, _to_probe(other, self.ctx).probe), self.ctx)
8758
Z3_probe Z3_API Z3_probe_ge(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is greater than or equal to the...

◆ __gt__()

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

8717 def __gt__(self, other):
8718 """Return a probe that evaluates to "true" when the value returned by `self`
8719 is greater than the value returned by `other`.
8720
8721 >>> p = Probe('size') > 10
8722 >>> x = Int('x')
8723 >>> g = Goal()
8724 >>> g.add(x > 0)
8725 >>> g.add(x < 10)
8726 >>> p(g)
8727 0.0
8728 """
8729 return Probe(Z3_probe_gt(self.ctx.ref(), self.probe, _to_probe(other, self.ctx).probe), self.ctx)
8730
Z3_probe Z3_API Z3_probe_gt(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is greater than the value retur...

◆ __le__()

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

8731 def __le__(self, other):
8732 """Return a probe that evaluates to "true" when the value returned by `self`
8733 is less than or equal to the value returned by `other`.
8734
8735 >>> p = Probe('size') <= 2
8736 >>> x = Int('x')
8737 >>> g = Goal()
8738 >>> g.add(x > 0)
8739 >>> g.add(x < 10)
8740 >>> p(g)
8741 1.0
8742 """
8743 return Probe(Z3_probe_le(self.ctx.ref(), self.probe, _to_probe(other, self.ctx).probe), self.ctx)
8744
Z3_probe Z3_API Z3_probe_le(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than or equal to the va...

◆ __lt__()

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

8703 def __lt__(self, other):
8704 """Return a probe that evaluates to "true" when the value returned by `self`
8705 is less than the value returned by `other`.
8706
8707 >>> p = Probe('size') < 10
8708 >>> x = Int('x')
8709 >>> g = Goal()
8710 >>> g.add(x > 0)
8711 >>> g.add(x < 10)
8712 >>> p(g)
8713 1.0
8714 """
8715 return Probe(Z3_probe_lt(self.ctx.ref(), self.probe, _to_probe(other, self.ctx).probe), self.ctx)
8716
Z3_probe Z3_API Z3_probe_lt(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than the value returned...

◆ __ne__()

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

8773 def __ne__(self, other):
8774 """Return a probe that evaluates to "true" when the value returned by `self`
8775 is not equal to the value returned by `other`.
8776
8777 >>> p = Probe('size') != 2
8778 >>> x = Int('x')
8779 >>> g = Goal()
8780 >>> g.add(x > 0)
8781 >>> g.add(x < 10)
8782 >>> p(g)
8783 0.0
8784 """
8785 p = self.__eq__(other)
8786 return Probe(Z3_probe_not(self.ctx.ref(), p.probe), self.ctx)
8787
Z3_probe Z3_API Z3_probe_not(Z3_context x, Z3_probe p)
Return a probe that evaluates to "true" when p does not evaluate to true.

Field Documentation

◆ ctx

ctx = _get_ctx(ctx)

Definition at line 8674 of file z3py.py.

◆ probe

probe = None

Definition at line 8675 of file z3py.py.