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

Data Structures

class  Entry
 

Public Member Functions

int getNumEntries () throws Z3Exception
 
Entry[] getEntries () throws Z3Exception
 
Expr getElse () throws Z3Exception
 
int getArity () throws Z3Exception
 
String toString ()
 
- Public Member Functions inherited from Z3Object
void dispose () throws Z3Exception
 
- Public Member Functions inherited from IDisposable
void dispose () throws Z3Exception
 

Additional Inherited Members

- Protected Member Functions inherited from Z3Object
void finalize () throws Z3Exception
 

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 ( ) throws Z3Exception
inline

The arity of the function interpretation

Definition at line 141 of file FuncInterp.java.

142  {
143  return Native.funcInterpGetArity(getContext().nCtx(), getNativeObject());
144  }
Expr getElse ( ) throws Z3Exception
inline

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

Exceptions
Z3Exception

Definition at line 132 of file FuncInterp.java.

Referenced by FuncInterp.toString().

133  {
134  return Expr.create(getContext(),
135  Native.funcInterpGetElse(getContext().nCtx(), getNativeObject()));
136  }
Entry [] getEntries ( ) throws Z3Exception
inline

The entries in the function interpretation

Exceptions
Z3Exception

Definition at line 117 of file FuncInterp.java.

Referenced by FuncInterp.toString().

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

The number of entries in the function interpretation.

Definition at line 107 of file FuncInterp.java.

Referenced by FuncInterp.getEntries().

108  {
109  return Native.funcInterpGetNumEntries(getContext().nCtx(), getNativeObject());
110  }
String toString ( )
inline

A string representation of the function interpretation.

Definition at line 149 of file FuncInterp.java.

150  {
151  try
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  } catch (Z3Exception e)
175  {
176  return new String("Z3Exception: " + e.getMessage());
177  }
178  }