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 | |
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.
__init__ | ( | self, | |
probe, | |||
ctx = None ) |
Definition at line 8673 of file z3py.py.
__del__ | ( | self | ) |
Definition at line 8699 of file z3py.py.
__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.
__deepcopy__ | ( | self, | |
memo = {} ) |
__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.
__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.
__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.
__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.
__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.
__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.