Go to the documentation of this file.00001
00018 package com.microsoft.z3;
00019
00025 public class FuncInterp extends Z3Object
00026 {
00031 public class Entry extends Z3Object
00032 {
00038 public Expr getValue() throws Z3Exception
00039 {
00040 return Expr.create(getContext(),
00041 Native.funcEntryGetValue(getContext().nCtx(), getNativeObject()));
00042 }
00043
00047 public int getNumArgs() throws Z3Exception
00048 {
00049 return Native.funcEntryGetNumArgs(getContext().nCtx(), getNativeObject());
00050 }
00051
00057 public Expr[] getArgs() throws Z3Exception
00058 {
00059 int n = getNumArgs();
00060 Expr[] res = new Expr[n];
00061 for (int i = 0; i < n; i++)
00062 res[i] = Expr.create(getContext(), Native.funcEntryGetArg(
00063 getContext().nCtx(), getNativeObject(), i));
00064 return res;
00065 }
00066
00070 public String toString()
00071 {
00072 try
00073 {
00074 int n = getNumArgs();
00075 String res = "[";
00076 Expr[] args = getArgs();
00077 for (int i = 0; i < n; i++)
00078 res += args[i] + ", ";
00079 return res + getValue() + "]";
00080 } catch (Z3Exception e)
00081 {
00082 return new String("Z3Exception: " + e.getMessage());
00083 }
00084 }
00085
00086 Entry(Context ctx, long obj) throws Z3Exception
00087 {
00088 super(ctx, obj);
00089 }
00090
00091 void incRef(long o) throws Z3Exception
00092 {
00093 getContext().funcEntry_DRQ().incAndClear(getContext(), o);
00094 super.incRef(o);
00095 }
00096
00097 void decRef(long o) throws Z3Exception
00098 {
00099 getContext().funcEntry_DRQ().add(o);
00100 super.decRef(o);
00101 }
00102 };
00103
00107 public int getNumEntries() throws Z3Exception
00108 {
00109 return Native.funcInterpGetNumEntries(getContext().nCtx(), getNativeObject());
00110 }
00111
00117 public Entry[] getEntries() throws Z3Exception
00118 {
00119 int n = getNumEntries();
00120 Entry[] res = new Entry[n];
00121 for (int i = 0; i < n; i++)
00122 res[i] = new Entry(getContext(), Native.funcInterpGetEntry(getContext()
00123 .nCtx(), getNativeObject(), i));
00124 return res;
00125 }
00126
00132 public Expr getElse() throws Z3Exception
00133 {
00134 return Expr.create(getContext(),
00135 Native.funcInterpGetElse(getContext().nCtx(), getNativeObject()));
00136 }
00137
00141 public int getArity() throws Z3Exception
00142 {
00143 return Native.funcInterpGetArity(getContext().nCtx(), getNativeObject());
00144 }
00145
00149 public String toString()
00150 {
00151 try
00152 {
00153 String res = "";
00154 res += "[";
00155 for (Entry e : getEntries())
00156 {
00157 int n = e.getNumArgs();
00158 if (n > 1)
00159 res += "[";
00160 Expr[] args = e.getArgs();
00161 for (int i = 0; i < n; i++)
00162 {
00163 if (i != 0)
00164 res += ", ";
00165 res += args[i];
00166 }
00167 if (n > 1)
00168 res += "]";
00169 res += " -> " + e.getValue() + ", ";
00170 }
00171 res += "else -> " + getElse();
00172 res += "]";
00173 return res;
00174 } catch (Z3Exception e)
00175 {
00176 return new String("Z3Exception: " + e.getMessage());
00177 }
00178 }
00179
00180 FuncInterp(Context ctx, long obj) throws Z3Exception
00181 {
00182 super(ctx, obj);
00183 }
00184
00185 void incRef(long o) throws Z3Exception
00186 {
00187 getContext().funcInterp_DRQ().incAndClear(getContext(), o);
00188 super.incRef(o);
00189 }
00190
00191 void decRef(long o) throws Z3Exception
00192 {
00193 getContext().funcInterp_DRQ().add(o);
00194 super.decRef(o);
00195 }
00196 }