Z3
src/api/java/FuncDecl.java
Go to the documentation of this file.
00001 
00018 package com.microsoft.z3;
00019 
00020 import com.microsoft.z3.enumerations.Z3_ast_kind;
00021 import com.microsoft.z3.enumerations.Z3_decl_kind;
00022 import com.microsoft.z3.enumerations.Z3_parameter_kind;
00023 
00027 public class FuncDecl extends AST
00028 {
00035     /* Overloaded operators are not translated. */
00036 
00043     /* Overloaded operators are not translated. */
00044 
00048     public boolean equals(Object o)
00049     {
00050         FuncDecl casted = (FuncDecl) o;
00051         if (casted == null)
00052             return false;
00053         return this == casted;
00054     }
00055 
00059     public int hashCode()
00060     {
00061         return super.hashCode();
00062     }
00063 
00067     public String toString()
00068     {
00069         try
00070         {
00071             return Native.funcDeclToString(getContext().nCtx(), getNativeObject());
00072         } catch (Z3Exception e)
00073         {
00074             return "Z3Exception: " + e.getMessage();
00075         }
00076     }
00077 
00081     public int getId() throws Z3Exception
00082     {
00083         return Native.getFuncDeclId(getContext().nCtx(), getNativeObject());
00084     }
00085 
00089     public int getArity() throws Z3Exception
00090     {
00091         return Native.getArity(getContext().nCtx(), getNativeObject());
00092     }
00093 
00098     public int getDomainSize() throws Z3Exception
00099     {
00100         return Native.getDomainSize(getContext().nCtx(), getNativeObject());
00101     }
00102 
00106     public Sort[] getDomain() throws Z3Exception
00107     {
00108 
00109         int n = getDomainSize();
00110 
00111         Sort[] res = new Sort[n];
00112         for (int i = 0; i < n; i++)
00113             res[i] = Sort.create(getContext(),
00114                     Native.getDomain(getContext().nCtx(), getNativeObject(), i));
00115         return res;
00116     }
00117 
00121     public Sort getRange() throws Z3Exception
00122     {
00123 
00124         return Sort.create(getContext(),
00125                 Native.getRange(getContext().nCtx(), getNativeObject()));
00126     }
00127 
00131     public Z3_decl_kind getDeclKind() throws Z3Exception
00132     {
00133         return Z3_decl_kind.fromInt(Native.getDeclKind(getContext().nCtx(),
00134                 getNativeObject()));
00135     }
00136 
00140     public Symbol getName() throws Z3Exception
00141     {
00142 
00143         return Symbol.create(getContext(),
00144                 Native.getDeclName(getContext().nCtx(), getNativeObject()));
00145     }
00146 
00150     public int getNumParameters() throws Z3Exception
00151     {
00152         return Native.getDeclNumParameters(getContext().nCtx(), getNativeObject());
00153     }
00154 
00158     public Parameter[] getParameters() throws Z3Exception
00159     {
00160 
00161         int num = getNumParameters();
00162         Parameter[] res = new Parameter[num];
00163         for (int i = 0; i < num; i++)
00164         {
00165             Z3_parameter_kind k = Z3_parameter_kind.fromInt(Native
00166                     .getDeclParameterKind(getContext().nCtx(), getNativeObject(), i));
00167             switch (k)
00168             {
00169             case Z3_PARAMETER_INT:
00170                 res[i] = new Parameter(k, Native.getDeclIntParameter(getContext()
00171                         .nCtx(), getNativeObject(), i));
00172                 break;
00173             case Z3_PARAMETER_DOUBLE:
00174                 res[i] = new Parameter(k, Native.getDeclDoubleParameter(
00175                         getContext().nCtx(), getNativeObject(), i));
00176                 break;
00177             case Z3_PARAMETER_SYMBOL:
00178                 res[i] = new Parameter(k, Symbol.create(getContext(), Native
00179                         .getDeclSymbolParameter(getContext().nCtx(),
00180                                 getNativeObject(), i)));
00181                 break;
00182             case Z3_PARAMETER_SORT:
00183                 res[i] = new Parameter(k, Sort.create(getContext(), Native
00184                         .getDeclSortParameter(getContext().nCtx(), getNativeObject(),
00185                                 i)));
00186                 break;
00187             case Z3_PARAMETER_AST:
00188                 res[i] = new Parameter(k, new AST(getContext(),
00189                         Native.getDeclAstParameter(getContext().nCtx(),
00190                                 getNativeObject(), i)));
00191                 break;
00192             case Z3_PARAMETER_FUNC_DECL:
00193                 res[i] = new Parameter(k, new FuncDecl(getContext(),
00194                         Native.getDeclFuncDeclParameter(getContext().nCtx(),
00195                                 getNativeObject(), i)));
00196                 break;
00197             case Z3_PARAMETER_RATIONAL:
00198                 res[i] = new Parameter(k, Native.getDeclRationalParameter(
00199                         getContext().nCtx(), getNativeObject(), i));
00200                 break;
00201             default:
00202                 throw new Z3Exception(
00203                         "Unknown function declaration parameter kind encountered");
00204             }
00205         }
00206         return res;
00207     }
00208 
00212     public class Parameter
00213     {
00214         private Z3_parameter_kind kind;
00215         private int i;
00216         private double d;
00217         private Symbol sym;
00218         private Sort srt;
00219         private AST ast;
00220         private FuncDecl fd;
00221         private String r;
00222 
00226         public int getInt() throws Z3Exception
00227         {
00228             if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_INT)
00229                 throw new Z3Exception("parameter is not an int");
00230             return i;
00231         }
00232 
00236         public double getDouble() throws Z3Exception
00237         {
00238             if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_DOUBLE)
00239                 throw new Z3Exception("parameter is not a double ");
00240             return d;
00241         }
00242 
00246         public Symbol getSymbol() throws Z3Exception
00247         {
00248             if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_SYMBOL)
00249                 throw new Z3Exception("parameter is not a Symbol");
00250             return sym;
00251         }
00252 
00256         public Sort getSort() throws Z3Exception
00257         {
00258             if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_SORT)
00259                 throw new Z3Exception("parameter is not a Sort");
00260             return srt;
00261         }
00262 
00266         public AST getAST() throws Z3Exception
00267         {
00268             if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_AST)
00269                 throw new Z3Exception("parameter is not an AST");
00270             return ast;
00271         }
00272 
00276         public FuncDecl getFuncDecl() throws Z3Exception
00277         {
00278             if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_FUNC_DECL)
00279                 throw new Z3Exception("parameter is not a function declaration");
00280             return fd;
00281         }
00282 
00286         public String getRational() throws Z3Exception
00287         {
00288             if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_RATIONAL)
00289                 throw new Z3Exception("parameter is not a rational String");
00290             return r;
00291         }
00292 
00296         public Z3_parameter_kind getParameterKind() throws Z3Exception
00297         {
00298             return kind;
00299         }
00300 
00301         Parameter(Z3_parameter_kind k, int i)
00302         {
00303             this.kind = k;
00304             this.i = i;
00305         }
00306 
00307         Parameter(Z3_parameter_kind k, double d)
00308         {
00309             this.kind = k;
00310             this.d = d;
00311         }
00312 
00313         Parameter(Z3_parameter_kind k, Symbol s)
00314         {
00315             this.kind = k;
00316             this.sym = s;
00317         }
00318 
00319         Parameter(Z3_parameter_kind k, Sort s)
00320         {
00321             this.kind = k;
00322             this.srt = s;
00323         }
00324 
00325         Parameter(Z3_parameter_kind k, AST a)
00326         {
00327             this.kind = k;
00328             this.ast = a;
00329         }
00330 
00331         Parameter(Z3_parameter_kind k, FuncDecl fd)
00332         {
00333             this.kind = k;
00334             this.fd = fd;
00335         }
00336 
00337         Parameter(Z3_parameter_kind k, String r)
00338         {
00339             this.kind = k;
00340             this.r = r;
00341         }
00342     }
00343 
00344     FuncDecl(Context ctx, long obj) throws Z3Exception
00345     {
00346         super(ctx, obj);
00347 
00348     }
00349 
00350     FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range)
00351             throws Z3Exception
00352     {
00353         super(ctx, Native.mkFuncDecl(ctx.nCtx(), name.getNativeObject(),
00354                 AST.arrayLength(domain), AST.arrayToNative(domain),
00355                 range.getNativeObject()));
00356 
00357     }
00358 
00359     FuncDecl(Context ctx, String prefix, Sort[] domain, Sort range)
00360             throws Z3Exception
00361     {
00362         super(ctx, Native.mkFreshFuncDecl(ctx.nCtx(), prefix,
00363                 AST.arrayLength(domain), AST.arrayToNative(domain),
00364                 range.getNativeObject()));
00365 
00366     }
00367 
00368     void checkNativeObject(long obj) throws Z3Exception
00369     {
00370         if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_FUNC_DECL_AST
00371                 .toInt())
00372             throw new Z3Exception(
00373                     "Underlying object is not a function declaration");
00374         super.checkNativeObject(obj);
00375     }
00376 
00383     public Expr apply(Expr ... args) throws Z3Exception
00384     {
00385         getContext().checkContextMatch(args);
00386         return Expr.create(getContext(), this, args);
00387     }
00388 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines