Z3
FuncDecl.cs
Go to the documentation of this file.
1/*++
2Copyright (c) 2012 Microsoft Corporation
3
4Module Name:
5
6 FuncDecl.cs
7
8Abstract:
9
10 Z3 Managed API: Function Declarations
11
12Author:
13
14 Christoph Wintersteiger (cwinter) 2012-03-16
15
16Notes:
17
18--*/
19
20using System;
21using System.Diagnostics;
22using System.Linq;
23
24
25namespace Microsoft.Z3
26{
30 public class FuncDecl : AST
31 {
36 public static bool operator ==(FuncDecl a, FuncDecl b)
37 {
38 return Object.ReferenceEquals(a, b) ||
39 (!Object.ReferenceEquals(a, null) &&
40 !Object.ReferenceEquals(b, null) &&
41 a.Context.nCtx == b.Context.nCtx &&
42 Native.Z3_is_eq_func_decl(a.Context.nCtx, a.NativeObject, b.NativeObject) != 0);
43 }
44
49 public static bool operator !=(FuncDecl a, FuncDecl b)
50 {
51 return !(a == b);
52 }
53
57 public override bool Equals(object o)
58 {
59 FuncDecl casted = o as FuncDecl;
60 if (casted == null) return false;
61 return this == casted;
62 }
63
67 public override int GetHashCode()
68 {
69 return base.GetHashCode();
70 }
71
75 public override string ToString()
76 {
77 return Native.Z3_func_decl_to_string(Context.nCtx, NativeObject);
78 }
79
83 new public uint Id
84 {
85 get { return Native.Z3_get_func_decl_id(Context.nCtx, NativeObject); }
86 }
87
91 public uint Arity
92 {
93 get { return Native.Z3_get_arity(Context.nCtx, NativeObject); }
94 }
95
100 public uint DomainSize
101 {
102 get { return Native.Z3_get_domain_size(Context.nCtx, NativeObject); }
103 }
104
108 public Sort[] Domain
109 {
110 get
111 {
112
113 uint n = DomainSize;
114
115 Sort[] res = new Sort[n];
116 for (uint i = 0; i < n; i++)
117 res[i] = Sort.Create(Context, Native.Z3_get_domain(Context.nCtx, NativeObject, i));
118 return res;
119 }
120 }
121
125 public Sort Range
126 {
127 get
128 {
129 return Sort.Create(Context, Native.Z3_get_range(Context.nCtx, NativeObject));
130 }
131 }
132
137 {
138 get { return (Z3_decl_kind)Native.Z3_get_decl_kind(Context.nCtx, NativeObject); }
139 }
140
145 {
146 get
147 {
148 return Symbol.Create(Context, Native.Z3_get_decl_name(Context.nCtx, NativeObject));
149 }
150 }
151
155 public uint NumParameters
156 {
157 get { return Native.Z3_get_decl_num_parameters(Context.nCtx, NativeObject); }
158 }
159
164 {
165 get
166 {
167
168 uint num = NumParameters;
169 Parameter[] res = new Parameter[num];
170 for (uint i = 0; i < num; i++)
171 {
172 Z3_parameter_kind k = (Z3_parameter_kind)Native.Z3_get_decl_parameter_kind(Context.nCtx, NativeObject, i);
173 switch (k)
174 {
175 case Z3_parameter_kind.Z3_PARAMETER_INT:
176 res[i] = new Parameter(k, Native.Z3_get_decl_int_parameter(Context.nCtx, NativeObject, i));
177 break;
178 case Z3_parameter_kind.Z3_PARAMETER_DOUBLE:
179 res[i] = new Parameter(k, Native.Z3_get_decl_double_parameter(Context.nCtx, NativeObject, i));
180 break;
181 case Z3_parameter_kind.Z3_PARAMETER_SYMBOL:
182 res[i] = new Parameter(k, Symbol.Create(Context, Native.Z3_get_decl_symbol_parameter(Context.nCtx, NativeObject, i)));
183 break;
184 case Z3_parameter_kind.Z3_PARAMETER_SORT:
185 res[i] = new Parameter(k, Sort.Create(Context, Native.Z3_get_decl_sort_parameter(Context.nCtx, NativeObject, i)));
186 break;
187 case Z3_parameter_kind.Z3_PARAMETER_AST:
188 res[i] = new Parameter(k, new AST(Context, Native.Z3_get_decl_ast_parameter(Context.nCtx, NativeObject, i)));
189 break;
190 case Z3_parameter_kind.Z3_PARAMETER_FUNC_DECL:
191 res[i] = new Parameter(k, new FuncDecl(Context, Native.Z3_get_decl_func_decl_parameter(Context.nCtx, NativeObject, i)));
192 break;
193 case Z3_parameter_kind.Z3_PARAMETER_RATIONAL:
194 res[i] = new Parameter(k, Native.Z3_get_decl_rational_parameter(Context.nCtx, NativeObject, i));
195 break;
196 default:
197 throw new Z3Exception("Unknown function declaration parameter kind encountered");
198 }
199 }
200 return res;
201 }
202 }
203
207 public class Parameter
208 {
209 readonly private Z3_parameter_kind kind;
210 readonly private int i;
211 readonly private double d;
212 readonly private Symbol sym;
213 readonly private Sort srt;
214 readonly private AST ast;
215 readonly private FuncDecl fd;
216 readonly private string r;
217
219 public int Int { get { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_INT) throw new Z3Exception("parameter is not an int"); return i; } }
221 public double Double { get { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_DOUBLE) throw new Z3Exception("parameter is not a double "); return d; } }
223 public Symbol Symbol { get { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_SYMBOL) throw new Z3Exception("parameter is not a Symbol"); return sym; } }
225 public Sort Sort { get { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_SORT) throw new Z3Exception("parameter is not a Sort"); return srt; } }
227 public AST AST { get { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_AST) throw new Z3Exception("parameter is not an AST"); return ast; } }
229 public FuncDecl FuncDecl { get { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_FUNC_DECL) throw new Z3Exception("parameter is not a function declaration"); return fd; } }
231 public string Rational { get { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_RATIONAL) throw new Z3Exception("parameter is not a rational string"); return r; } }
232
236 public Z3_parameter_kind ParameterKind { get { return kind; } }
237
238 #region Internal
239 internal Parameter(Z3_parameter_kind k, int i)
240 {
241 this.kind = k;
242 this.i = i;
243 }
244
245 internal Parameter(Z3_parameter_kind k, double d)
246 {
247 this.kind = k;
248 this.d = d;
249 }
250
251 internal Parameter(Z3_parameter_kind k, Symbol s)
252 {
253 this.kind = k;
254 this.sym = s;
255 }
256
257 internal Parameter(Z3_parameter_kind k, Sort s)
258 {
259 this.kind = k;
260 this.srt = s;
261 }
262
263 internal Parameter(Z3_parameter_kind k, AST a)
264 {
265 this.kind = k;
266 this.ast = a;
267 }
268
269 internal Parameter(Z3_parameter_kind k, FuncDecl fd)
270 {
271 this.kind = k;
272 this.fd = fd;
273 }
274
275 internal Parameter(Z3_parameter_kind k, string r)
276 {
277 this.kind = k;
278 this.r = r;
279 }
280 #endregion
281 }
282
283 #region Internal
284 internal FuncDecl(Context ctx, IntPtr obj)
285 : base(ctx, obj)
286 {
287 Debug.Assert(ctx != null);
288 }
289
290 internal FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range)
291 : base(ctx, Native.Z3_mk_func_decl(ctx.nCtx, name.NativeObject, AST.ArrayLength(domain), AST.ArrayToNative(domain), range.NativeObject))
292 {
293 Debug.Assert(ctx != null);
294 Debug.Assert(name != null);
295 Debug.Assert(range != null);
296 }
297
298 internal FuncDecl(Context ctx, string prefix, Sort[] domain, Sort range)
299 : base(ctx, Native.Z3_mk_fresh_func_decl(ctx.nCtx, prefix, AST.ArrayLength(domain), AST.ArrayToNative(domain), range.NativeObject))
300 {
301 Debug.Assert(ctx != null);
302 Debug.Assert(range != null);
303 }
304
305 internal FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range, bool is_rec)
306 : base(ctx, Native.Z3_mk_rec_func_decl(ctx.nCtx, name.NativeObject, AST.ArrayLength(domain), AST.ArrayToNative(domain), range.NativeObject))
307 {
308 Debug.Assert(ctx != null);
309 Debug.Assert(name != null);
310 Debug.Assert(range != null);
311 }
312
313
314#if DEBUG
315 internal override void CheckNativeObject(IntPtr obj)
316 {
317 if (Native.Z3_get_ast_kind(Context.nCtx, obj) != (uint)Z3_ast_kind.Z3_FUNC_DECL_AST)
318 throw new Z3Exception("Underlying object is not a function declaration");
319 base.CheckNativeObject(obj);
320 }
321#endif
322 #endregion
323
329 new public FuncDecl Translate(Context ctx)
330 {
331 return (FuncDecl) base.Translate(ctx);
332 }
333
334
340 public Expr this[params Expr[] args]
341 {
342 get
343 {
344 Debug.Assert(args == null || args.All(a => a != null));
345
346 return Apply(args);
347 }
348 }
349
355 public Expr Apply(params Expr[] args)
356 {
357 Debug.Assert(args == null || args.All(a => a != null));
358
359 Context.CheckContextMatch<Expr>(args);
360 return Expr.Create(Context, this, args);
361 }
362 }
363}
The abstract syntax tree (AST) class.
Definition: AST.cs:31
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Expressions are terms.
Definition: Expr.cs:31
Function declarations can have Parameters associated with them.
Definition: FuncDecl.cs:208
AST AST
The AST value of the parameter.
Definition: FuncDecl.cs:227
Symbol Symbol
The Symbol value of the parameter.
Definition: FuncDecl.cs:223
double Double
The double value of the parameter.
Definition: FuncDecl.cs:221
Sort Sort
The Sort value of the parameter.
Definition: FuncDecl.cs:225
string Rational
The rational string value of the parameter.
Definition: FuncDecl.cs:231
Z3_parameter_kind ParameterKind
The kind of the parameter.
Definition: FuncDecl.cs:236
int Int
The int value of the parameter.
Definition: FuncDecl.cs:219
FuncDecl FuncDecl
The FunctionDeclaration value of the parameter.
Definition: FuncDecl.cs:229
Function declarations.
Definition: FuncDecl.cs:31
override bool Equals(object o)
Object comparison.
Definition: FuncDecl.cs:57
Parameter[] Parameters
The parameters of the function declaration
Definition: FuncDecl.cs:164
Sort Range
The range of the function declaration
Definition: FuncDecl.cs:126
uint Arity
The arity of the function declaration
Definition: FuncDecl.cs:92
Expr this[params Expr[] args
Create expression that applies function to arguments.
Definition: FuncDecl.cs:341
Expr Apply(params Expr[] args)
Create expression that applies function to arguments.
Definition: FuncDecl.cs:355
uint DomainSize
The size of the domain of the function declaration Arity
Definition: FuncDecl.cs:101
override int GetHashCode()
A hash code.
Definition: FuncDecl.cs:67
static bool operator==(FuncDecl a, FuncDecl b)
Comparison operator.
Definition: FuncDecl.cs:36
static bool operator!=(FuncDecl a, FuncDecl b)
Comparison operator.
Definition: FuncDecl.cs:49
override string ToString()
A string representations of the function declaration.
Definition: FuncDecl.cs:75
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:137
Sort[] Domain
The domain of the function declaration
Definition: FuncDecl.cs:109
uint NumParameters
The number of parameters of the function declaration
Definition: FuncDecl.cs:156
Symbol Name
The name of the function declaration
Definition: FuncDecl.cs:145
new uint Id
Returns a unique identifier for the function declaration.
Definition: FuncDecl.cs:84
new FuncDecl Translate(Context ctx)
Translates (copies) the function declaration to the Context ctx .
Definition: FuncDecl.cs:329
The Sort class implements type information for ASTs.
Definition: Sort.cs:29
Symbols are used to name several term and type constructors.
Definition: Symbol.cs:30
The exception base class for error reporting from Z3
Definition: Z3Exception.cs:32
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3725
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
Definition: z3_api.h:180
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:1000
Z3_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a constant or function.
Z3_func_decl Z3_API Z3_mk_fresh_func_decl(Z3_context c, Z3_string prefix, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a fresh constant or function.
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:136
Z3_func_decl Z3_API Z3_mk_rec_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a recursive function.