Z3
Data Structures | Public Member Functions
FuncInterp Class Reference
+ Inheritance diagram for FuncInterp:

Data Structures

class  Entry
 

Public Member Functions

int getNumEntries ()
 
Entry[] getEntries ()
 
Expr getElse ()
 
int getArity ()
 
String toString ()
 

Detailed Description

A function interpretation is represented as a finite map and an 'else' value. Each entry in the finite map represents the value of a function given a set of arguments.

Definition at line 25 of file FuncInterp.java.

Member Function Documentation

◆ getArity()

int getArity ( )
inline

The arity of the function interpretation

Exceptions
Z3Exceptionon error
Returns
an int

Definition at line 143 of file FuncInterp.java.

144 {
145 return Native.funcInterpGetArity(getContext().nCtx(), getNativeObject());
146 }

◆ getElse()

Expr getElse ( )
inline

The (symbolic) ‘else’ value of the function interpretation.

Exceptions
Z3Exception
Z3Exceptionon error
Returns
an Expr

Definition at line 132 of file FuncInterp.java.

133 {
134 return Expr.create(getContext(),
135 Native.funcInterpGetElse(getContext().nCtx(), getNativeObject()));
136 }

Referenced by FuncInterp.toString().

◆ getEntries()

Entry[] getEntries ( )
inline

The entries in the function interpretation

Exceptions
Z3Exception
Z3Exceptionon error

Definition at line 115 of file FuncInterp.java.

116 {
117 int n = getNumEntries();
118 Entry[] res = new Entry[n];
119 for (int i = 0; i < n; i++)
120 res[i] = new Entry(getContext(), Native.funcInterpGetEntry(getContext()
121 .nCtx(), getNativeObject(), i));
122 return res;
123 }

Referenced by FuncInterp.toString().

◆ getNumEntries()

int getNumEntries ( )
inline

The number of entries in the function interpretation.

Exceptions
Z3Exceptionon error
Returns
an int

Definition at line 104 of file FuncInterp.java.

105 {
106 return Native.funcInterpGetNumEntries(getContext().nCtx(), getNativeObject());
107 }

Referenced by FuncInterp.getEntries().

◆ toString()

String toString ( )
inline

A string representation of the function interpretation.

Definition at line 151 of file FuncInterp.java.

152 {
153 String res = "";
154 res += "[";
155 for (Entry e : getEntries())
156 {
157 int n = e.getNumArgs();
158 if (n > 1)
159 res += "[";
160 Expr[] args = e.getArgs();
161 for (int i = 0; i < n; i++)
162 {
163 if (i != 0)
164 res += ", ";
165 res += args[i];
166 }
167 if (n > 1)
168 res += "]";
169 res += " -> " + e.getValue() + ", ";
170 }
171 res += "else -> " + getElse();
172 res += "]";
173 return res;
174 }
def String(name, ctx=None)
Definition: z3py.py:10085