Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules Pages
FuncDecl.cs
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6  FuncDecl.cs
7 
8 Abstract:
9 
10  Z3 Managed API: Function Declarations
11 
12 Author:
13 
14  Christoph Wintersteiger (cwinter) 2012-03-16
15 
16 Notes:
17 
18 --*/
19 
20 using System;
21 using System.Diagnostics.Contracts;
22 
23 namespace Microsoft.Z3
24 {
28  [ContractVerification(true)]
29  public class FuncDecl : AST
30  {
35  public static bool operator ==(FuncDecl a, FuncDecl b)
36  {
37  return Object.ReferenceEquals(a, b) ||
38  (!Object.ReferenceEquals(a, null) &&
39  !Object.ReferenceEquals(b, null) &&
40  a.Context.nCtx == b.Context.nCtx &&
41  Native.Z3_is_eq_func_decl(a.Context.nCtx, a.NativeObject, b.NativeObject) != 0);
42  }
43 
48  public static bool operator !=(FuncDecl a, FuncDecl b)
49  {
50  return !(a == b);
51  }
52 
56  public override bool Equals(object o)
57  {
58  FuncDecl casted = o as FuncDecl;
59  if (casted == null) return false;
60  return this == casted;
61  }
62 
66  public override int GetHashCode()
67  {
68  return base.GetHashCode();
69  }
70 
74  public override string ToString()
75  {
76  return Native.Z3_func_decl_to_string(Context.nCtx, NativeObject);
77  }
78 
82  new public uint Id
83  {
84  get { return Native.Z3_get_func_decl_id(Context.nCtx, NativeObject); }
85  }
86 
90  public uint Arity
91  {
92  get { return Native.Z3_get_arity(Context.nCtx, NativeObject); }
93  }
94 
99  public uint DomainSize
100  {
101  get { return Native.Z3_get_domain_size(Context.nCtx, NativeObject); }
102  }
103 
107  public Sort[] Domain
108  {
109  get
110  {
111  Contract.Ensures(Contract.Result<Sort[]>() != null);
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  Contract.Ensures(Contract.Result<Sort>() != null);
130  return Sort.Create(Context, Native.Z3_get_range(Context.nCtx, NativeObject));
131  }
132  }
133 
137  public Z3_decl_kind DeclKind
138  {
139  get { return (Z3_decl_kind)Native.Z3_get_decl_kind(Context.nCtx, NativeObject); }
140  }
141 
145  public Symbol Name
146  {
147  get
148  {
149  Contract.Ensures(Contract.Result<Symbol>() != null);
150  return Symbol.Create(Context, Native.Z3_get_decl_name(Context.nCtx, NativeObject));
151  }
152  }
153 
157  public uint NumParameters
158  {
159  get { return Native.Z3_get_decl_num_parameters(Context.nCtx, NativeObject); }
160  }
161 
165  public Parameter[] Parameters
166  {
167  get
168  {
169  Contract.Ensures(Contract.Result<Parameter[]>() != null);
170 
171  uint num = NumParameters;
172  Parameter[] res = new Parameter[num];
173  for (uint i = 0; i < num; i++)
174  {
176  switch (k)
177  {
178  case Z3_parameter_kind.Z3_PARAMETER_INT:
179  res[i] = new Parameter(k, Native.Z3_get_decl_int_parameter(Context.nCtx, NativeObject, i));
180  break;
181  case Z3_parameter_kind.Z3_PARAMETER_DOUBLE:
182  res[i] = new Parameter(k, Native.Z3_get_decl_double_parameter(Context.nCtx, NativeObject, i));
183  break;
184  case Z3_parameter_kind.Z3_PARAMETER_SYMBOL:
185  res[i] = new Parameter(k, Symbol.Create(Context, Native.Z3_get_decl_symbol_parameter(Context.nCtx, NativeObject, i)));
186  break;
187  case Z3_parameter_kind.Z3_PARAMETER_SORT:
188  res[i] = new Parameter(k, Sort.Create(Context, Native.Z3_get_decl_sort_parameter(Context.nCtx, NativeObject, i)));
189  break;
190  case Z3_parameter_kind.Z3_PARAMETER_AST:
191  res[i] = new Parameter(k, new AST(Context, Native.Z3_get_decl_ast_parameter(Context.nCtx, NativeObject, i)));
192  break;
193  case Z3_parameter_kind.Z3_PARAMETER_FUNC_DECL:
194  res[i] = new Parameter(k, new FuncDecl(Context, Native.Z3_get_decl_func_decl_parameter(Context.nCtx, NativeObject, i)));
195  break;
196  case Z3_parameter_kind.Z3_PARAMETER_RATIONAL:
197  res[i] = new Parameter(k, Native.Z3_get_decl_rational_parameter(Context.nCtx, NativeObject, i));
198  break;
199  default:
200  throw new Z3Exception("Unknown function declaration parameter kind encountered");
201  }
202  }
203  return res;
204  }
205  }
206 
210  public class Parameter
211  {
212  readonly private Z3_parameter_kind kind;
213  readonly private int i;
214  readonly private double d;
215  readonly private Symbol sym;
216  readonly private Sort srt;
217  readonly private AST ast;
218  readonly private FuncDecl fd;
219  readonly private string r;
220 
222  public int Int { get { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_INT) throw new Z3Exception("parameter is not an int"); return i; } }
224  public double Double { get { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_DOUBLE) throw new Z3Exception("parameter is not a double "); return d; } }
226  public Symbol Symbol { get { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_SYMBOL) throw new Z3Exception("parameter is not a Symbol"); return sym; } }
228  public Sort Sort { get { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_SORT) throw new Z3Exception("parameter is not a Sort"); return srt; } }
230  public AST AST { get { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_AST) throw new Z3Exception("parameter is not an AST"); return ast; } }
232  public FuncDecl FuncDecl { get { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_FUNC_DECL) throw new Z3Exception("parameter is not a function declaration"); return fd; } }
234  public string Rational { get { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_RATIONAL) throw new Z3Exception("parameter is not a rational string"); return r; } }
235 
239  public Z3_parameter_kind ParameterKind { get { return kind; } }
240 
241  #region Internal
242  internal Parameter(Z3_parameter_kind k, int i)
243  {
244  this.kind = k;
245  this.i = i;
246  }
247 
248  internal Parameter(Z3_parameter_kind k, double d)
249  {
250  this.kind = k;
251  this.d = d;
252  }
253 
254  internal Parameter(Z3_parameter_kind k, Symbol s)
255  {
256  this.kind = k;
257  this.sym = s;
258  }
259 
260  internal Parameter(Z3_parameter_kind k, Sort s)
261  {
262  this.kind = k;
263  this.srt = s;
264  }
265 
266  internal Parameter(Z3_parameter_kind k, AST a)
267  {
268  this.kind = k;
269  this.ast = a;
270  }
271 
272  internal Parameter(Z3_parameter_kind k, FuncDecl fd)
273  {
274  this.kind = k;
275  this.fd = fd;
276  }
277 
278  internal Parameter(Z3_parameter_kind k, string r)
279  {
280  this.kind = k;
281  this.r = r;
282  }
283  #endregion
284  }
285 
286  #region Internal
287  internal FuncDecl(Context ctx, IntPtr obj)
288  : base(ctx, obj)
289  {
290  Contract.Requires(ctx != null);
291  }
292 
293  internal FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range)
294  : base(ctx, Native.Z3_mk_func_decl(ctx.nCtx, name.NativeObject, AST.ArrayLength(domain), AST.ArrayToNative(domain), range.NativeObject))
295  {
296  Contract.Requires(ctx != null);
297  Contract.Requires(name != null);
298  Contract.Requires(range != null);
299  }
300 
301  internal FuncDecl(Context ctx, string prefix, Sort[] domain, Sort range)
302  : base(ctx, Native.Z3_mk_fresh_func_decl(ctx.nCtx, prefix, AST.ArrayLength(domain), AST.ArrayToNative(domain), range.NativeObject))
303  {
304  Contract.Requires(ctx != null);
305  Contract.Requires(range != null);
306  }
307 
308 #if DEBUG
309  internal override void CheckNativeObject(IntPtr obj)
310  {
311  if (Native.Z3_get_ast_kind(Context.nCtx, obj) != (uint)Z3_ast_kind.Z3_FUNC_DECL_AST)
312  throw new Z3Exception("Underlying object is not a function declaration");
313  base.CheckNativeObject(obj);
314  }
315 #endif
316  #endregion
317 
323  public Expr this[params Expr[] args]
324  {
325  get
326  {
327  Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
328 
329  return Apply(args);
330  }
331  }
332 
338  public Expr Apply(params Expr[] args)
339  {
340  Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
341 
342  Context.CheckContextMatch(args);
343  return Expr.Create(Context, this, args);
344  }
345 
346  }
347 }
static IntPtr Z3_get_decl_symbol_parameter(Z3_context a0, Z3_func_decl a1, uint a2)
Definition: Native.cs:3166
static IntPtr Z3_get_decl_name(Z3_context a0, Z3_func_decl a1)
Definition: Native.cs:3086
static Z3_sort Z3_get_decl_sort_parameter(Z3_context a0, Z3_func_decl a1, uint a2)
Definition: Native.cs:3174
static int Z3_is_eq_func_decl(Z3_context a0, Z3_func_decl a1, Z3_func_decl a2)
Definition: Native.cs:3070
static uint Z3_get_decl_num_parameters(Z3_context a0, Z3_func_decl a1)
Definition: Native.cs:3134
static int Z3_get_decl_int_parameter(Z3_context a0, Z3_func_decl a1, uint a2)
Definition: Native.cs:3150
override bool Equals(object o)
Object comparison.
Definition: FuncDecl.cs:56
Z3_decl_kind
Z3_decl_kind
Definition: Enumerations.cs:59
static uint Z3_get_domain_size(Z3_context a0, Z3_func_decl a1)
Definition: Native.cs:3102
def Int
Definition: z3py.py:2717
static string Z3_func_decl_to_string(Z3_context a0, Z3_func_decl a1)
Definition: Native.cs:3856
Expressions are terms.
Definition: Expr.cs:29
static uint Z3_get_decl_kind(Z3_context a0, Z3_func_decl a1)
Definition: Native.cs:3094
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
Definition: z3_api.h:212
override int GetHashCode()
A hash code.
Definition: FuncDecl.cs:66
static uint Z3_get_func_decl_id(Z3_context a0, Z3_func_decl a1)
Definition: Native.cs:3078
Function declarations can have Parameters associated with them.
Definition: FuncDecl.cs:210
static string Z3_get_decl_rational_parameter(Z3_context a0, Z3_func_decl a1, uint a2)
Definition: Native.cs:3198
Expr Apply(params Expr[] args)
Create expression that applies function to arguments.
Definition: FuncDecl.cs:338
static uint Z3_get_decl_parameter_kind(Z3_context a0, Z3_func_decl a1, uint a2)
Definition: Native.cs:3142
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:171
static double Z3_get_decl_double_parameter(Z3_context a0, Z3_func_decl a1, uint a2)
Definition: Native.cs:3158
Z3_func_decl Z3_API Z3_mk_fresh_func_decl(__in Z3_context c, __in Z3_string prefix, __in unsigned domain_size, __in_ecount(domain_size) Z3_sort const domain[], __in Z3_sort range)
Declare a fresh constant or function.
The main interaction with Z3 happens via the Context.
Definition: Context.cs:31
The Sort class implements type information for ASTs.
Definition: Sort.cs:29
The exception base class for error reporting from Z3
Definition: Z3Exception.cs:27
static Z3_func_decl Z3_get_decl_func_decl_parameter(Z3_context a0, Z3_func_decl a1, uint a2)
Definition: Native.cs:3190
The abstract syntax tree (AST) class.
Definition: AST.cs:31
static Z3_sort Z3_get_range(Z3_context a0, Z3_func_decl a1)
Definition: Native.cs:3126
Z3_func_decl Z3_API Z3_mk_func_decl(__in Z3_context c, __in Z3_symbol s, __in unsigned domain_size, __in_ecount(domain_size) Z3_sort const domain[], __in Z3_sort range)
Declare a constant or function.
static Z3_sort Z3_get_domain(Z3_context a0, Z3_func_decl a1, uint a2)
Definition: Native.cs:3118
Symbols are used to name several term and type constructors.
Definition: Symbol.cs:30
Function declarations.
Definition: FuncDecl.cs:29
override string ToString()
A string representations of the function declaration.
Definition: FuncDecl.cs:74
Z3_parameter_kind
Z3_parameter_kind
Definition: Enumerations.cs:23
static uint Z3_get_arity(Z3_context a0, Z3_func_decl a1)
Definition: Native.cs:3110
static Z3_ast Z3_get_decl_ast_parameter(Z3_context a0, Z3_func_decl a1, uint a2)
Definition: Native.cs:3182