Public Member Functions | |
def | __init__ (self, probe, ctx=None) |
def | __del__ (self) |
def | __lt__ (self, other) |
def | __gt__ (self, other) |
def | __le__ (self, other) |
def | __ge__ (self, other) |
def | __eq__ (self, other) |
def | __ne__ (self, other) |
def | __call__ (self, goal) |
Data Fields | |
ctx | |
probe | |
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.
def __init__ | ( | self, | |
probe, | |||
ctx = None |
|||
) |
Definition at line 7214 of file z3py.py.
def __del__ | ( | self | ) |
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
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 7293 of file z3py.py.
Referenced by Probe.__ne__().
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 7280 of file z3py.py.
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 7254 of file z3py.py.
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 7267 of file z3py.py.
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 7241 of file z3py.py.
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
ctx |
Definition at line 7215 of file z3py.py.
Referenced by Probe.__call__(), Probe.__del__(), Probe.__eq__(), Probe.__ge__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), and Probe.__ne__().
probe |
Definition at line 7216 of file z3py.py.
Referenced by Probe.__call__(), Probe.__del__(), Probe.__eq__(), Probe.__ge__(), Probe.__gt__(), Probe.__le__(), and Probe.__lt__().