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