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 |
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 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 | ) |
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)
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().
Definition at line 6702 of file z3py.py.
Referenced by Probe.__call__(), Probe.__del__(), Probe.__eq__(), Probe.__ge__(), Probe.__gt__(), Probe.__le__(), and Probe.__lt__().