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
00036
00043
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 }