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 ()
 
- Public Member Functions inherited from Z3Object
void dispose ()
 
- Public Member Functions inherited from IDisposable
void dispose ()
 

Additional Inherited Members

- Protected Member Functions inherited from Z3Object
void finalize ()
 

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

int getArity ( )
inline

The arity of the function interpretation

Exceptions
Z3Exceptionon error
Returns
an int

Definition at line 151 of file FuncInterp.java.

152  {
153  return Native.funcInterpGetArity(getContext().nCtx(), getNativeObject());
154  }
Expr getElse ( )
inline

The (symbolic) `else' value of the function interpretation.

Exceptions
Z3Exception
Z3Exceptionon error
Returns
an Expr

Definition at line 140 of file FuncInterp.java.

Referenced by FuncInterp.toString().

141  {
142  return Expr.create(getContext(),
143  Native.funcInterpGetElse(getContext().nCtx(), getNativeObject()));
144  }
Entry [] getEntries ( )
inline

The entries in the function interpretation

Exceptions
Z3Exception
Z3Exceptionon error

Definition at line 123 of file FuncInterp.java.

Referenced by FuncInterp.toString().

124  {
125  int n = getNumEntries();
126  Entry[] res = new Entry[n];
127  for (int i = 0; i < n; i++)
128  res[i] = new Entry(getContext(), Native.funcInterpGetEntry(getContext()
129  .nCtx(), getNativeObject(), i));
130  return res;
131  }
int getNumEntries ( )
inline

The number of entries in the function interpretation.

Exceptions
Z3Exceptionon error
Returns
an int

Definition at line 112 of file FuncInterp.java.

Referenced by FuncInterp.getEntries().

113  {
114  return Native.funcInterpGetNumEntries(getContext().nCtx(), getNativeObject());
115  }
String toString ( )
inline

A string representation of the function interpretation.

Definition at line 159 of file FuncInterp.java.

160  {
161  try
162  {
163  String res = "";
164  res += "[";
165  for (Entry e : getEntries())
166  {
167  int n = e.getNumArgs();
168  if (n > 1)
169  res += "[";
170  Expr[] args = e.getArgs();
171  for (int i = 0; i < n; i++)
172  {
173  if (i != 0)
174  res += ", ";
175  res += args[i];
176  }
177  if (n > 1)
178  res += "]";
179  res += " -> " + e.getValue() + ", ";
180  }
181  res += "else -> " + getElse();
182  res += "]";
183  return res;
184  } catch (Z3Exception e)
185  {
186  return new String("Z3Exception: " + e.getMessage());
187  }
188  }