Public Member Functions | |
def | __init__ |
def | __del__ |
def | num_args |
def | arg_value |
def | value |
def | as_list |
def | __repr__ |
Data Fields | |
entry | |
ctx |
Store the value of the interpretation of a function in a particular point.
def __init__ | ( | self, | |
entry, | |||
ctx | |||
) |
def __del__ | ( | self | ) |
def __repr__ | ( | self | ) |
def arg_value | ( | self, | |
idx | |||
) |
Return the value of argument `idx`. >>> f = Function('f', IntSort(), IntSort(), IntSort()) >>> s = Solver() >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10) >>> s.check() sat >>> m = s.model() >>> f_i = m[f] >>> f_i.num_entries() 3 >>> e = f_i.entry(0) >>> e [0, 1, 10] >>> e.num_args() 2 >>> e.arg_value(0) 0 >>> e.arg_value(1) 1 >>> try: ... e.arg_value(2) ... except IndexError: ... print("index error") index error
Definition at line 5086 of file z3py.py.
05086 05087 def arg_value(self, idx): 05088 """Return the value of argument `idx`. 05089 05090 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 05091 >>> s = Solver() 05092 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10) 05093 >>> s.check() 05094 sat 05095 >>> m = s.model() 05096 >>> f_i = m[f] 05097 >>> f_i.num_entries() 05098 3 05099 >>> e = f_i.entry(0) 05100 >>> e 05101 [0, 1, 10] 05102 >>> e.num_args() 05103 2 05104 >>> e.arg_value(0) 05105 0 05106 >>> e.arg_value(1) 05107 1 05108 >>> try: 05109 ... e.arg_value(2) 05110 ... except IndexError: 05111 ... print("index error") 05112 index error 05113 """ 05114 if idx >= self.num_args(): 05115 raise IndexError 05116 return _to_expr_ref(Z3_func_entry_get_arg(self.ctx.ref(), self.entry, idx), self.ctx)
def as_list | ( | self | ) |
Return entry `self` as a Python list. >>> f = Function('f', IntSort(), IntSort(), IntSort()) >>> s = Solver() >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10) >>> s.check() sat >>> m = s.model() >>> f_i = m[f] >>> f_i.num_entries() 3 >>> e = f_i.entry(0) >>> e.as_list() [0, 1, 10]
Definition at line 5139 of file z3py.py.
Referenced by FuncEntry.__repr__().
05139 05140 def as_list(self): 05141 """Return entry `self` as a Python list. 05142 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 05143 >>> s = Solver() 05144 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10) 05145 >>> s.check() 05146 sat 05147 >>> m = s.model() 05148 >>> f_i = m[f] 05149 >>> f_i.num_entries() 05150 3 05151 >>> e = f_i.entry(0) 05152 >>> e.as_list() 05153 [0, 1, 10] 05154 """ 05155 args = [ self.arg_value(i) for i in range(self.num_args())] 05156 args.append(self.value()) 05157 return args
def num_args | ( | self | ) |
Return the number of arguments in the given entry. >>> f = Function('f', IntSort(), IntSort(), IntSort()) >>> s = Solver() >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10) >>> s.check() sat >>> m = s.model() >>> f_i = m[f] >>> f_i.num_entries() 3 >>> e = f_i.entry(0) >>> e.num_args() 2
Definition at line 5068 of file z3py.py.
Referenced by FuncEntry.arg_value(), and FuncEntry.as_list().
05068 05069 def num_args(self): 05070 """Return the number of arguments in the given entry. 05071 05072 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 05073 >>> s = Solver() 05074 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10) 05075 >>> s.check() 05076 sat 05077 >>> m = s.model() 05078 >>> f_i = m[f] 05079 >>> f_i.num_entries() 05080 3 05081 >>> e = f_i.entry(0) 05082 >>> e.num_args() 05083 2 05084 """ 05085 return int(Z3_func_entry_get_num_args(self.ctx.ref(), self.entry))
def value | ( | self | ) |
Return the value of the function at point `self`. >>> f = Function('f', IntSort(), IntSort(), IntSort()) >>> s = Solver() >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10) >>> s.check() sat >>> m = s.model() >>> f_i = m[f] >>> f_i.num_entries() 3 >>> e = f_i.entry(0) >>> e [0, 1, 10] >>> e.num_args() 2 >>> e.value() 10
Definition at line 5117 of file z3py.py.
Referenced by FuncEntry.as_list().
05117 05118 def value(self): 05119 """Return the value of the function at point `self`. 05120 05121 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 05122 >>> s = Solver() 05123 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10) 05124 >>> s.check() 05125 sat 05126 >>> m = s.model() 05127 >>> f_i = m[f] 05128 >>> f_i.num_entries() 05129 3 05130 >>> e = f_i.entry(0) 05131 >>> e 05132 [0, 1, 10] 05133 >>> e.num_args() 05134 2 05135 >>> e.value() 05136 10 05137 """ 05138 return _to_expr_ref(Z3_func_entry_get_value(self.ctx.ref(), self.entry), self.ctx)
Definition at line 5060 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__(), ApplyResult.__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(), Fixedpoint.add_rule(), Tactic.apply(), AlgebraicNumRef.approx(), ExprRef.arg(), FuncEntry.arg_value(), ApplyResult.as_expr(), Fixedpoint.assert_exprs(), QuantifierRef.body(), BoolSortRef.cast(), DatatypeSortRef.constructor(), ApplyResult.convert_model(), ExprRef.decl(), RatNumRef.denominator(), FuncDeclRef.domain(), ArraySortRef.domain(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_rules(), SortRef.kind(), SortRef.name(), FuncDeclRef.name(), QuantifierRef.no_pattern(), RatNumRef.numerator(), Fixedpoint.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), QuantifierRef.pattern(), FuncDeclRef.range(), ArraySortRef.range(), DatatypeSortRef.recognizer(), Fixedpoint.set(), Tactic.solver(), ExprRef.sort(), BoolRef.sort(), QuantifierRef.sort(), ArithRef.sort(), BitVecRef.sort(), ArrayRef.sort(), DatatypeRef.sort(), Fixedpoint.statistics(), Solver.to_smt2(), Fixedpoint.update_rule(), FuncEntry.value(), QuantifierRef.var_name(), and QuantifierRef.var_sort().
Definition at line 5060 of file z3py.py.
Referenced by FuncEntry::__del__(), FuncEntry::arg_value(), FuncEntry::num_args(), and FuncEntry::value().