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

  Z3Exception | on 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 |
  Z3Exception | on 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 |
  Z3Exception | on 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 }
com.microsoft.z3.FuncInterp.getNumEntries
int getNumEntries()
Definition: FuncInterp.java:105

## ◆ getNumEntries()

int getNumEntries | ( |  | ) |
| inline

The number of entries in the function interpretation.

Exceptions

  Z3Exception | on 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 }
com.microsoft.z3.FuncInterp.getElse
Expr< R > getElse()
Definition: FuncInterp.java:133
com.microsoft.z3.FuncInterp.getEntries
Entry< R >[] getEntries()
Definition: FuncInterp.java:116
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10693