Z3
Data Structures | Public Member Functions
FuncInterp< R extends Sort > Class Template Reference
+ Inheritance diagram for FuncInterp< R extends Sort >:

Data Structures

class  Entry
 

Public Member Functions

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

Additional Inherited Members

- Static Public Member Functions inherited from Z3Object
static long[] arrayToNative (Z3Object[] a)
 
static int arrayLength (Z3Object[] a)
 

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 26 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 144 of file FuncInterp.java.

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

◆ getElse()

Expr< R > getElse ( )
inline

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

Exceptions
Z3Exception
Z3Exceptionon error
Returns
an Expr

Definition at line 133 of file FuncInterp.java.

134 {
135 return (Expr<R>) Expr.create(getContext(),
136 Native.funcInterpGetElse(getContext().nCtx(), getNativeObject()));
137 }

◆ getEntries()

Entry< R >[] getEntries ( )
inline

The entries in the function interpretation

Exceptions
Z3Exception
Z3Exceptionon error

Definition at line 116 of file FuncInterp.java.

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

◆ getNumEntries()

int getNumEntries ( )
inline

The number of entries in the function interpretation.

Exceptions
Z3Exceptionon error
Returns
an int

Definition at line 105 of file FuncInterp.java.

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

◆ toString()

String toString ( )
inline

A string representation of the function interpretation.

Definition at line 152 of file FuncInterp.java.

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