Z3
src/api/java/FuncInterp.java
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 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines