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