Z3
Public Member Functions
FuncInterp.Entry Class Reference
+ Inheritance diagram for FuncInterp.Entry:

Public Member Functions

Expr getValue ()
 
int getNumArgs ()
 
Expr[] getArgs ()
 
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

An Entry object represents an element in the finite map used to encode a function interpretation.

Definition at line 31 of file FuncInterp.java.

Member Function Documentation

Expr [] getArgs ( )
inline

The arguments of the function entry.

Exceptions
Z3Exception
Z3Exceptionon error

Definition at line 60 of file FuncInterp.java.

Referenced by FuncInterp.Entry.toString().

61  {
62  int n = getNumArgs();
63  Expr[] res = new Expr[n];
64  for (int i = 0; i < n; i++)
65  res[i] = Expr.create(getContext(), Native.funcEntryGetArg(
66  getContext().nCtx(), getNativeObject(), i));
67  return res;
68  }
int getNumArgs()
Definition: FuncInterp.java:49
int getNumArgs ( )
inline

The number of arguments of the entry.

Exceptions
Z3Exceptionon error

Definition at line 49 of file FuncInterp.java.

Referenced by FuncInterp.Entry.getArgs(), and FuncInterp.Entry.toString().

50  {
51  return Native.funcEntryGetNumArgs(getContext().nCtx(), getNativeObject());
52  }
Expr getValue ( )
inline

Return the (symbolic) value of this entry.

Exceptions
Z3Exception
Z3Exceptionon error

Definition at line 39 of file FuncInterp.java.

Referenced by FuncInterp.Entry.toString().

40  {
41  return Expr.create(getContext(),
42  Native.funcEntryGetValue(getContext().nCtx(), getNativeObject()));
43  }
String toString ( )
inline

A string representation of the function entry.

Definition at line 73 of file FuncInterp.java.

74  {
75  try
76  {
77  int n = getNumArgs();
78  String res = "[";
79  Expr[] args = getArgs();
80  for (int i = 0; i < n; i++)
81  res += args[i] + ", ";
82  return res + getValue() + "]";
83  } catch (Z3Exception e)
84  {
85  return new String("Z3Exception: " + e.getMessage());
86  }
87  }
Expr[] getArgs()
Definition: FuncInterp.java:60
int getNumArgs()
Definition: FuncInterp.java:49
Expr getValue()
Definition: FuncInterp.java:39