Public Member Functions | |
Expr | getValue () throws Z3Exception |
int | getNumArgs () throws Z3Exception |
Expr[] | getArgs () throws Z3Exception |
String | toString () |
Package Functions | |
Entry (Context ctx, long obj) throws Z3Exception | |
void | incRef (long o) throws Z3Exception |
void | decRef (long o) throws Z3Exception |
An Entry object represents an element in the finite map used to encode a function interpretation.
Definition at line 31 of file FuncInterp.java.
Entry | ( | Context | ctx, |
long | obj | ||
) | throws Z3Exception [inline, package] |
Definition at line 86 of file FuncInterp.java.
{ super(ctx, obj); }
void decRef | ( | long | o | ) | throws Z3Exception [inline, package] |
Reimplemented from Z3Object.
Definition at line 97 of file FuncInterp.java.
{ getContext().funcEntry_DRQ().add(o); super.decRef(o); }
Expr [] getArgs | ( | ) | throws Z3Exception [inline] |
The arguments of the function entry.
Z3Exception |
Definition at line 57 of file FuncInterp.java.
Referenced by FuncInterp.Entry.toString().
{ int n = getNumArgs(); Expr[] res = new Expr[n]; for (int i = 0; i < n; i++) res[i] = Expr.create(getContext(), Native.funcEntryGetArg( getContext().nCtx(), getNativeObject(), i)); return res; }
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().
{ return Native.funcEntryGetNumArgs(getContext().nCtx(), getNativeObject()); }
Expr getValue | ( | ) | throws Z3Exception [inline] |
Return the (symbolic) value of this entry.
Z3Exception |
Definition at line 38 of file FuncInterp.java.
Referenced by FuncInterp.Entry.toString().
{ return Expr.create(getContext(), Native.funcEntryGetValue(getContext().nCtx(), getNativeObject())); }
void incRef | ( | long | o | ) | throws Z3Exception [inline, package] |
Reimplemented from Z3Object.
Definition at line 91 of file FuncInterp.java.
{ getContext().funcEntry_DRQ().incAndClear(getContext(), o); super.incRef(o); }
String toString | ( | ) | [inline] |
A string representation of the function entry.
Definition at line 70 of file FuncInterp.java.
{ try { int n = getNumArgs(); String res = "["; Expr[] args = getArgs(); for (int i = 0; i < n; i++) res += args[i] + ", "; return res + getValue() + "]"; } catch (Z3Exception e) { return new String("Z3Exception: " + e.getMessage()); } }