1 /** 2 Copyright (c) 2012-2014 Microsoft Corporation 3 4 Module Name: 5 6 FuncDecl.java 7 8 Abstract: 9 10 Author: 11 12 @author Christoph Wintersteiger (cwinter) 2012-03-15 13 14 Notes: 15 16 **/ 17 18 package com.microsoft.z3; 19 20 import com.microsoft.z3.enumerations.Z3_ast_kind; 21 import com.microsoft.z3.enumerations.Z3_decl_kind; 22 import com.microsoft.z3.enumerations.Z3_parameter_kind; 23 24 /** 25 * Function declarations. 26 **/ 27 public class FuncDecl<R extends Sort> extends AST 28 { 29 /** 30 * Object comparison. 31 **/ 32 @Override equals(Object o)33 public boolean equals(Object o) 34 { 35 if (o == this) return true; 36 if (!(o instanceof FuncDecl)) return false; 37 FuncDecl<?> other = (FuncDecl<?>) o; 38 39 return 40 (getContext().nCtx() == other.getContext().nCtx()) && 41 (Native.isEqFuncDecl( 42 getContext().nCtx(), 43 getNativeObject(), 44 other.getNativeObject())); 45 } 46 47 @Override toString()48 public String toString() 49 { 50 return Native.funcDeclToString(getContext().nCtx(), getNativeObject()); 51 } 52 53 /** 54 * Returns a unique identifier for the function declaration. 55 **/ 56 @Override getId()57 public int getId() 58 { 59 return Native.getFuncDeclId(getContext().nCtx(), getNativeObject()); 60 } 61 62 /** 63 * Translates (copies) the function declaration to the Context {@code ctx}. 64 * @param ctx A context 65 * 66 * @return A copy of the function declaration which is associated with {@code ctx} 67 * @throws Z3Exception on error 68 **/ 69 @SuppressWarnings("unchecked") translate(Context ctx)70 public FuncDecl<R> translate(Context ctx) 71 { 72 return (FuncDecl<R>) super.translate(ctx); 73 } 74 75 /** 76 * The arity of the function declaration 77 **/ getArity()78 public int getArity() 79 { 80 return Native.getArity(getContext().nCtx(), getNativeObject()); 81 } 82 83 /** 84 * The size of the domain of the function declaration 85 * @see #getArity 86 **/ getDomainSize()87 public int getDomainSize() 88 { 89 return Native.getDomainSize(getContext().nCtx(), getNativeObject()); 90 } 91 92 /** 93 * The domain of the function declaration 94 **/ getDomain()95 public Sort[] getDomain() 96 { 97 98 int n = getDomainSize(); 99 100 Sort[] res = new Sort[n]; 101 for (int i = 0; i < n; i++) 102 res[i] = Sort.create(getContext(), 103 Native.getDomain(getContext().nCtx(), getNativeObject(), i)); 104 return res; 105 } 106 107 /** 108 * The range of the function declaration 109 **/ 110 @SuppressWarnings("unchecked") getRange()111 public R getRange() 112 { 113 return (R) Sort.create(getContext(), 114 Native.getRange(getContext().nCtx(), getNativeObject())); 115 } 116 117 /** 118 * The kind of the function declaration. 119 **/ getDeclKind()120 public Z3_decl_kind getDeclKind() 121 { 122 return Z3_decl_kind.fromInt(Native.getDeclKind(getContext().nCtx(), 123 getNativeObject())); 124 } 125 126 /** 127 * The name of the function declaration 128 **/ getName()129 public Symbol getName() 130 { 131 132 return Symbol.create(getContext(), 133 Native.getDeclName(getContext().nCtx(), getNativeObject())); 134 } 135 136 /** 137 * The number of parameters of the function declaration 138 **/ getNumParameters()139 public int getNumParameters() 140 { 141 return Native.getDeclNumParameters(getContext().nCtx(), getNativeObject()); 142 } 143 144 /** 145 * The parameters of the function declaration 146 **/ getParameters()147 public Parameter[] getParameters() 148 { 149 150 int num = getNumParameters(); 151 Parameter[] res = new Parameter[num]; 152 for (int i = 0; i < num; i++) 153 { 154 Z3_parameter_kind k = Z3_parameter_kind.fromInt(Native 155 .getDeclParameterKind(getContext().nCtx(), getNativeObject(), i)); 156 switch (k) 157 { 158 case Z3_PARAMETER_INT: 159 res[i] = new Parameter(k, Native.getDeclIntParameter(getContext() 160 .nCtx(), getNativeObject(), i)); 161 break; 162 case Z3_PARAMETER_DOUBLE: 163 res[i] = new Parameter(k, Native.getDeclDoubleParameter( 164 getContext().nCtx(), getNativeObject(), i)); 165 break; 166 case Z3_PARAMETER_SYMBOL: 167 res[i] = new Parameter(k, Symbol.create(getContext(), Native 168 .getDeclSymbolParameter(getContext().nCtx(), 169 getNativeObject(), i))); 170 break; 171 case Z3_PARAMETER_SORT: 172 res[i] = new Parameter(k, Sort.create(getContext(), Native 173 .getDeclSortParameter(getContext().nCtx(), getNativeObject(), 174 i))); 175 break; 176 case Z3_PARAMETER_AST: 177 res[i] = new Parameter(k, new AST(getContext(), 178 Native.getDeclAstParameter(getContext().nCtx(), 179 getNativeObject(), i))); 180 break; 181 case Z3_PARAMETER_FUNC_DECL: 182 res[i] = new Parameter(k, new FuncDecl<>(getContext(), 183 Native.getDeclFuncDeclParameter(getContext().nCtx(), 184 getNativeObject(), i))); 185 break; 186 case Z3_PARAMETER_RATIONAL: 187 res[i] = new Parameter(k, Native.getDeclRationalParameter( 188 getContext().nCtx(), getNativeObject(), i)); 189 break; 190 default: 191 throw new Z3Exception( 192 "Unknown function declaration parameter kind encountered"); 193 } 194 } 195 return res; 196 } 197 198 /** 199 * Function declarations can have Parameters associated with them. 200 **/ 201 public static class Parameter 202 { 203 private Z3_parameter_kind kind; 204 private int i; 205 private double d; 206 private Symbol sym; 207 private Sort srt; 208 private AST ast; 209 private FuncDecl<?> fd; 210 private String r; 211 212 /** 213 * The int value of the parameter. 214 **/ getInt()215 public int getInt() 216 { 217 if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_INT) 218 throw new Z3Exception("parameter is not an int"); 219 return i; 220 } 221 222 /** 223 * The double value of the parameter. 224 **/ getDouble()225 public double getDouble() 226 { 227 if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_DOUBLE) 228 throw new Z3Exception("parameter is not a double "); 229 return d; 230 } 231 232 /** 233 * The Symbol value of the parameter. 234 **/ getSymbol()235 public Symbol getSymbol() 236 { 237 if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_SYMBOL) 238 throw new Z3Exception("parameter is not a Symbol"); 239 return sym; 240 } 241 242 /** 243 * The Sort value of the parameter. 244 **/ getSort()245 public Sort getSort() 246 { 247 if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_SORT) 248 throw new Z3Exception("parameter is not a Sort"); 249 return srt; 250 } 251 252 /** 253 * The AST value of the parameter. 254 **/ getAST()255 public AST getAST() 256 { 257 if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_AST) 258 throw new Z3Exception("parameter is not an AST"); 259 return ast; 260 } 261 262 /** 263 * The FunctionDeclaration value of the parameter. 264 **/ getFuncDecl()265 public FuncDecl<?> getFuncDecl() 266 { 267 if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_FUNC_DECL) 268 throw new Z3Exception("parameter is not a function declaration"); 269 return fd; 270 } 271 272 /** 273 * The rational string value of the parameter. 274 **/ getRational()275 public String getRational() 276 { 277 if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_RATIONAL) 278 throw new Z3Exception("parameter is not a rational String"); 279 return r; 280 } 281 282 /** 283 * The kind of the parameter. 284 **/ getParameterKind()285 public Z3_parameter_kind getParameterKind() 286 { 287 return kind; 288 } 289 Parameter(Z3_parameter_kind k, int i)290 Parameter(Z3_parameter_kind k, int i) 291 { 292 this.kind = k; 293 this.i = i; 294 } 295 Parameter(Z3_parameter_kind k, double d)296 Parameter(Z3_parameter_kind k, double d) 297 { 298 this.kind = k; 299 this.d = d; 300 } 301 Parameter(Z3_parameter_kind k, Symbol s)302 Parameter(Z3_parameter_kind k, Symbol s) 303 { 304 this.kind = k; 305 this.sym = s; 306 } 307 Parameter(Z3_parameter_kind k, Sort s)308 Parameter(Z3_parameter_kind k, Sort s) 309 { 310 this.kind = k; 311 this.srt = s; 312 } 313 Parameter(Z3_parameter_kind k, AST a)314 Parameter(Z3_parameter_kind k, AST a) 315 { 316 this.kind = k; 317 this.ast = a; 318 } 319 Parameter(Z3_parameter_kind k, FuncDecl<?> fd)320 Parameter(Z3_parameter_kind k, FuncDecl<?> fd) 321 { 322 this.kind = k; 323 this.fd = fd; 324 } 325 Parameter(Z3_parameter_kind k, String r)326 Parameter(Z3_parameter_kind k, String r) 327 { 328 this.kind = k; 329 this.r = r; 330 } 331 } 332 FuncDecl(Context ctx, long obj)333 FuncDecl(Context ctx, long obj) 334 { 335 super(ctx, obj); 336 337 } 338 FuncDecl(Context ctx, Symbol name, Sort[] domain, R range)339 FuncDecl(Context ctx, Symbol name, Sort[] domain, R range) 340 { 341 super(ctx, Native.mkFuncDecl(ctx.nCtx(), name.getNativeObject(), 342 AST.arrayLength(domain), AST.arrayToNative(domain), 343 range.getNativeObject())); 344 } 345 FuncDecl(Context ctx, Symbol name, Sort[] domain, R range, boolean is_rec)346 FuncDecl(Context ctx, Symbol name, Sort[] domain, R range, boolean is_rec) 347 { 348 super(ctx, Native.mkRecFuncDecl(ctx.nCtx(), name.getNativeObject(), 349 AST.arrayLength(domain), AST.arrayToNative(domain), 350 range.getNativeObject())); 351 352 } 353 FuncDecl(Context ctx, String prefix, Sort[] domain, R range)354 FuncDecl(Context ctx, String prefix, Sort[] domain, R range) 355 { 356 super(ctx, Native.mkFreshFuncDecl(ctx.nCtx(), prefix, 357 AST.arrayLength(domain), AST.arrayToNative(domain), 358 range.getNativeObject())); 359 360 } 361 checkNativeObject(long obj)362 void checkNativeObject(long obj) 363 { 364 if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_FUNC_DECL_AST 365 .toInt()) 366 throw new Z3Exception( 367 "Underlying object is not a function declaration"); 368 super.checkNativeObject(obj); 369 } 370 371 /** 372 * Create expression that applies function to arguments. 373 **/ apply(Expr<?> .... args)374 public Expr<R> apply(Expr<?> ... args) 375 { 376 getContext().checkContextMatch(args); 377 return Expr.create(getContext(), this, args); 378 } 379 } 380