Public Member Functions | |
def | __init__ |
def | __del__ |
def | else_value |
def | num_entries |
def | arity |
def | entry |
def | as_list |
def | __repr__ |
Data Fields | |
f | |
ctx |
def __init__ | ( | self, | |
f, | |||
ctx | |||
) |
def __del__ | ( | self | ) |
def __repr__ | ( | self | ) |
def arity | ( | self | ) |
Return the number of arguments for each entry in the function interpretation `self`. >>> f = Function('f', IntSort(), IntSort()) >>> s = Solver() >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) >>> s.check() sat >>> m = s.model() >>> m[f].arity() 1
Definition at line 5213 of file z3py.py.
05213 05214 def arity(self): 05215 """Return the number of arguments for each entry in the function interpretation `self`. 05216 05217 >>> f = Function('f', IntSort(), IntSort()) 05218 >>> s = Solver() 05219 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) 05220 >>> s.check() 05221 sat 05222 >>> m = s.model() 05223 >>> m[f].arity() 05224 1 05225 """ 05226 return int(Z3_func_interp_get_arity(self.ctx.ref(), self.f))
def as_list | ( | self | ) |
Return the function interpretation as a Python list. >>> f = Function('f', IntSort(), IntSort()) >>> s = Solver() >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) >>> s.check() sat >>> m = s.model() >>> m[f] [0 -> 1, 1 -> 1, 2 -> 0, else -> 1] >>> m[f].as_list() [[0, 1], [1, 1], [2, 0], 1]
Definition at line 5251 of file z3py.py.
05251 05252 def as_list(self): 05253 """Return the function interpretation as a Python list. 05254 >>> f = Function('f', IntSort(), IntSort()) 05255 >>> s = Solver() 05256 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) 05257 >>> s.check() 05258 sat 05259 >>> m = s.model() 05260 >>> m[f] 05261 [0 -> 1, 1 -> 1, 2 -> 0, else -> 1] 05262 >>> m[f].as_list() 05263 [[0, 1], [1, 1], [2, 0], 1] 05264 """ 05265 r = [ self.entry(i).as_list() for i in range(self.num_entries())] 05266 r.append(self.else_value()) 05267 return r
def else_value | ( | self | ) |
Return the `else` value for a function interpretation. Return None if Z3 did not specify the `else` value for this object. >>> f = Function('f', IntSort(), IntSort()) >>> s = Solver() >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) >>> s.check() sat >>> m = s.model() >>> m[f] [0 -> 1, 1 -> 1, 2 -> 0, else -> 1] >>> m[f].else_value() 1
Definition at line 5174 of file z3py.py.
Referenced by FuncInterp.as_list().
05174 05175 def else_value(self): 05176 """ 05177 Return the `else` value for a function interpretation. 05178 Return None if Z3 did not specify the `else` value for 05179 this object. 05180 05181 >>> f = Function('f', IntSort(), IntSort()) 05182 >>> s = Solver() 05183 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) 05184 >>> s.check() 05185 sat 05186 >>> m = s.model() 05187 >>> m[f] 05188 [0 -> 1, 1 -> 1, 2 -> 0, else -> 1] 05189 >>> m[f].else_value() 05190 1 05191 """ 05192 r = Z3_func_interp_get_else(self.ctx.ref(), self.f) 05193 if r: 05194 return _to_expr_ref(r, self.ctx) 05195 else: 05196 return None
def entry | ( | self, | |
idx | |||
) |
Return an entry at position `idx < self.num_entries()` in the function interpretation `self`. >>> f = Function('f', IntSort(), IntSort()) >>> s = Solver() >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) >>> s.check() sat >>> m = s.model() >>> m[f] [0 -> 1, 1 -> 1, 2 -> 0, else -> 1] >>> m[f].num_entries() 3 >>> m[f].entry(0) [0, 1] >>> m[f].entry(1) [1, 1] >>> m[f].entry(2) [2, 0]
Definition at line 5227 of file z3py.py.
Referenced by FuncInterp.as_list().
05227 05228 def entry(self, idx): 05229 """Return an entry at position `idx < self.num_entries()` in the function interpretation `self`. 05230 05231 >>> f = Function('f', IntSort(), IntSort()) 05232 >>> s = Solver() 05233 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) 05234 >>> s.check() 05235 sat 05236 >>> m = s.model() 05237 >>> m[f] 05238 [0 -> 1, 1 -> 1, 2 -> 0, else -> 1] 05239 >>> m[f].num_entries() 05240 3 05241 >>> m[f].entry(0) 05242 [0, 1] 05243 >>> m[f].entry(1) 05244 [1, 1] 05245 >>> m[f].entry(2) 05246 [2, 0] 05247 """ 05248 if idx >= self.num_entries(): 05249 raise IndexError 05250 return FuncEntry(Z3_func_interp_get_entry(self.ctx.ref(), self.f, idx), self.ctx)
def num_entries | ( | self | ) |
Return the number of entries/points in the function interpretation `self`. >>> f = Function('f', IntSort(), IntSort()) >>> s = Solver() >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) >>> s.check() sat >>> m = s.model() >>> m[f] [0 -> 1, 1 -> 1, 2 -> 0, else -> 1] >>> m[f].num_entries() 3
Definition at line 5197 of file z3py.py.
Referenced by FuncInterp.as_list(), and FuncInterp.entry().
05197 05198 def num_entries(self): 05199 """Return the number of entries/points in the function interpretation `self`. 05200 05201 >>> f = Function('f', IntSort(), IntSort()) 05202 >>> s = Solver() 05203 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) 05204 >>> s.check() 05205 sat 05206 >>> m = s.model() 05207 >>> m[f] 05208 [0 -> 1, 1 -> 1, 2 -> 0, else -> 1] 05209 >>> m[f].num_entries() 05210 3 05211 """ 05212 return int(Z3_func_interp_get_num_entries(self.ctx.ref(), self.f))
Definition at line 5164 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(), ApplyResult.as_expr(), Fixedpoint.assert_exprs(), QuantifierRef.body(), BoolSortRef.cast(), DatatypeSortRef.constructor(), ApplyResult.convert_model(), ExprRef.decl(), RatNumRef.denominator(), FuncDeclRef.domain(), ArraySortRef.domain(), FuncInterp.else_value(), FuncInterp.entry(), 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(), QuantifierRef.var_name(), and QuantifierRef.var_sort().
Definition at line 5164 of file z3py.py.
Referenced by FuncInterp::__del__(), FuncInterp::arity(), FuncInterp::as_list(), FuncInterp::else_value(), FuncInterp::entry(), and FuncInterp::num_entries().