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 () |
Package Functions | |
FuncInterp (Context ctx, long obj) throws Z3Exception | |
void | incRef (long o) throws Z3Exception |
void | decRef (long o) throws Z3Exception |
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.
FuncInterp | ( | Context | ctx, |
long | obj | ||
) | throws Z3Exception [inline, package] |
Definition at line 180 of file FuncInterp.java.
{ super(ctx, obj); }
void decRef | ( | long | o | ) | throws Z3Exception [inline, package] |
Reimplemented from Z3Object.
Definition at line 191 of file FuncInterp.java.
{ getContext().funcInterp_DRQ().add(o); super.decRef(o); }
int getArity | ( | ) | throws Z3Exception [inline] |
The arity of the function interpretation
Definition at line 141 of file FuncInterp.java.
{ return Native.funcInterpGetArity(getContext().nCtx(), getNativeObject()); }
Expr getElse | ( | ) | throws Z3Exception [inline] |
The (symbolic) `else' value of the function interpretation.
Z3Exception |
Definition at line 132 of file FuncInterp.java.
Referenced by FuncInterp.toString().
{ return Expr.create(getContext(), Native.funcInterpGetElse(getContext().nCtx(), getNativeObject())); }
Entry [] getEntries | ( | ) | throws Z3Exception [inline] |
The entries in the function interpretation
Z3Exception |
Definition at line 117 of file FuncInterp.java.
Referenced by FuncInterp.toString().
{ int n = getNumEntries(); Entry[] res = new Entry[n]; for (int i = 0; i < n; i++) res[i] = new Entry(getContext(), Native.funcInterpGetEntry(getContext() .nCtx(), getNativeObject(), i)); return res; }
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().
{ return Native.funcInterpGetNumEntries(getContext().nCtx(), getNativeObject()); }
void incRef | ( | long | o | ) | throws Z3Exception [inline, package] |
Reimplemented from Z3Object.
Definition at line 185 of file FuncInterp.java.
{ getContext().funcInterp_DRQ().incAndClear(getContext(), o); super.incRef(o); }
String toString | ( | ) | [inline] |
A string representation of the function interpretation.
Definition at line 149 of file FuncInterp.java.
{ try { String res = ""; res += "["; for (Entry e : getEntries()) { int n = e.getNumArgs(); if (n > 1) res += "["; Expr[] args = e.getArgs(); for (int i = 0; i < n; i++) { if (i != 0) res += ", "; res += args[i]; } if (n > 1) res += "]"; res += " -> " + e.getValue() + ", "; } res += "else -> " + getElse(); res += "]"; return res; } catch (Z3Exception e) { return new String("Z3Exception: " + e.getMessage()); } }