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 5221 of file z3py.py.

Constructor & Destructor Documentation

def __init__	(	self,
		f,
		ctx
	)

Definition at line 5224 of file z3py.py.

05224 
05225     def __init__(self, f, ctx):
05226         self.f   = f
05227         self.ctx = ctx
05228         if self.f != None:
05229             Z3_func_interp_inc_ref(self.ctx.ref(), self.f)

def __del__ ( self )

Definition at line 5230 of file z3py.py.

05230 
05231     def __del__(self):
05232         if self.f != None:
05233             Z3_func_interp_dec_ref(self.ctx.ref(), self.f)

Member Function Documentation

def __repr__ ( self )

Definition at line 5328 of file z3py.py.

05328 
05329     def __repr__(self):
05330         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 5273 of file z3py.py.

05273 
05274     def arity(self):
05275         """Return the number of arguments for each entry in the function interpretation `self`.
05276 
05277         >>> f = Function('f', IntSort(), IntSort())
05278         >>> s = Solver()
05279         >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
05280         >>> s.check()
05281         sat
05282         >>> m = s.model()
05283         >>> m[f].arity()
05284         1
05285         """
05286         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 5311 of file z3py.py.

05311 
05312     def as_list(self):
05313         """Return the function interpretation as a Python list.
05314         >>> f = Function('f', IntSort(), IntSort())
05315         >>> s = Solver()
05316         >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
05317         >>> s.check()
05318         sat
05319         >>> m = s.model()
05320         >>> m[f]
05321         [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
05322         >>> m[f].as_list()
05323         [[0, 1], [1, 1], [2, 0], 1]
05324         """
05325         r = [ self.entry(i).as_list() for i in range(self.num_entries())]
05326         r.append(self.else_value())
05327         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 5234 of file z3py.py.

Referenced by FuncInterp.as_list().

05234 
05235     def else_value(self):
05236         """
05237         Return the `else` value for a function interpretation.
05238         Return None if Z3 did not specify the `else` value for
05239         this object.
05240 
05241         >>> f = Function('f', IntSort(), IntSort())
05242         >>> s = Solver()
05243         >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
05244         >>> s.check()
05245         sat
05246         >>> m = s.model()
05247         >>> m[f]
05248         [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
05249         >>> m[f].else_value()
05250         1
05251         """
05252         r = Z3_func_interp_get_else(self.ctx.ref(), self.f)
05253         if r:
05254             return _to_expr_ref(r, self.ctx)
05255         else:
05256             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 5287 of file z3py.py.

Referenced by FuncInterp.as_list().

05287 
05288     def entry(self, idx):
05289         """Return an entry at position `idx < self.num_entries()` in the function interpretation `self`.
05290 
05291         >>> f = Function('f', IntSort(), IntSort())
05292         >>> s = Solver()
05293         >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
05294         >>> s.check()
05295         sat
05296         >>> m = s.model()
05297         >>> m[f]
05298         [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
05299         >>> m[f].num_entries()
05300         3
05301         >>> m[f].entry(0)
05302         [0, 1]
05303         >>> m[f].entry(1)
05304         [1, 1]
05305         >>> m[f].entry(2)
05306         [2, 0]
05307         """
05308         if idx >= self.num_entries():
05309             raise IndexError
05310         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 5257 of file z3py.py.

Referenced by FuncInterp.as_list(), and FuncInterp.entry().

05257 
05258     def num_entries(self):
05259         """Return the number of entries/points in the function interpretation `self`.
05260 
05261         >>> f = Function('f', IntSort(), IntSort())
05262         >>> s = Solver()
05263         >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
05264         >>> s.check()
05265         sat
05266         >>> m = s.model()
05267         >>> m[f]
05268         [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
05269         >>> m[f].num_entries()
05270         3
05271         """
05272         return int(Z3_func_interp_get_num_entries(self.ctx.ref(), self.f))

Field Documentation

ctx

Definition at line 5224 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(), Optimize.add_soft(), 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(), ArrayRef.mk_default(), Optimize.model(), SortRef.name(), FuncDeclRef.name(), QuantifierRef.no_pattern(), RatNumRef.numerator(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), QuantifierRef.pattern(), Fixedpoint.query(), FuncDeclRef.range(), ArraySortRef.range(), DatatypeSortRef.recognizer(), Fixedpoint.set(), Optimize.set(), Tactic.solver(), ExprRef.sort(), BoolRef.sort(), QuantifierRef.sort(), ArithRef.sort(), BitVecRef.sort(), ArrayRef.sort(), DatatypeRef.sort(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), Fixedpoint.update_rule(), QuantifierRef.var_name(), and QuantifierRef.var_sort().

f

Definition at line 5224 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