Inheritance diagram for FuncInterp:

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

Detailed Description

Stores the interpretation of a function in a Z3 model.

Definition at line 5161 of file z3py.py.

Constructor & Destructor Documentation

def __init__	(	self,
		f,
		ctx
	)

Definition at line 5164 of file z3py.py.

05164 
05165     def __init__(self, f, ctx):
05166         self.f   = f
05167         self.ctx = ctx
05168         if self.f != None:
05169             Z3_func_interp_inc_ref(self.ctx.ref(), self.f)

def __del__ ( self )

Definition at line 5170 of file z3py.py.

05170 
05171     def __del__(self):
05172         if self.f != None:
05173             Z3_func_interp_dec_ref(self.ctx.ref(), self.f)

Member Function Documentation

def __repr__ ( self )

Definition at line 5268 of file z3py.py.

05268 
05269     def __repr__(self):
05270         return obj_to_string(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))

Field Documentation

ctx

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().

f

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().

Public Member Functions

Data Fields

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation

Field Documentation