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

Public Member Functions

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

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

The arguments of the function entry.

Exceptions
Z3Exception

Definition at line 57 of file FuncInterp.java.

Referenced by FuncInterp.Entry.toString().

58  {
59  int n = getNumArgs();
60  Expr[] res = new Expr[n];
61  for (int i = 0; i < n; i++)
62  res[i] = Expr.create(getContext(), Native.funcEntryGetArg(
63  getContext().nCtx(), getNativeObject(), i));
64  return res;
65  }
int getNumArgs()
Definition: FuncInterp.java:47
int getNumArgs ( ) throws Z3Exception
inline

The number of arguments of the entry.

Definition at line 47 of file FuncInterp.java.

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

48  {
49  return Native.funcEntryGetNumArgs(getContext().nCtx(), getNativeObject());
50  }
Expr getValue ( ) throws Z3Exception
inline

Return the (symbolic) value of this entry.

Exceptions
Z3Exception

Definition at line 38 of file FuncInterp.java.

Referenced by FuncInterp.Entry.toString().

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

A string representation of the function entry.

Definition at line 70 of file FuncInterp.java.

71  {
72  try
73  {
74  int n = getNumArgs();
75  String res = "[";
76  Expr[] args = getArgs();
77  for (int i = 0; i < n; i++)
78  res += args[i] + ", ";
79  return res + getValue() + "]";
80  } catch (Z3Exception e)
81  {
82  return new String("Z3Exception: " + e.getMessage());
83  }
84  }
Expr[] getArgs()
Definition: FuncInterp.java:57
int getNumArgs()
Definition: FuncInterp.java:47
Expr getValue()
Definition: FuncInterp.java:38