Z3
src/api/dotnet/FuncDecl.cs
Go to the documentation of this file.
00001 /*++
00002 Copyright (c) 2012 Microsoft Corporation
00003 
00004 Module Name:
00005 
00006     FuncDecl.cs
00007 
00008 Abstract:
00009 
00010     Z3 Managed API: Function Declarations
00011 
00012 Author:
00013 
00014     Christoph Wintersteiger (cwinter) 2012-03-16
00015 
00016 Notes:
00017     
00018 --*/
00019 
00020 using System;
00021 using System.Diagnostics.Contracts;
00022 
00023 namespace Microsoft.Z3
00024 {
00028     [ContractVerification(true)]
00029     public class FuncDecl : AST
00030     {
00035         public static bool operator ==(FuncDecl a, FuncDecl b)
00036         {
00037             return Object.ReferenceEquals(a, b) ||
00038                    (!Object.ReferenceEquals(a, null) &&
00039                     !Object.ReferenceEquals(b, null) &&
00040                     a.Context.nCtx == b.Context.nCtx &&
00041                     Native.Z3_is_eq_func_decl(a.Context.nCtx, a.NativeObject, b.NativeObject) != 0);
00042         }
00043 
00048         public static bool operator !=(FuncDecl a, FuncDecl b)
00049         {
00050             return !(a == b);
00051         }
00052 
00056         public override bool Equals(object o)
00057         {
00058             FuncDecl casted = o as FuncDecl;
00059             if (casted == null) return false;
00060             return this == casted;
00061         }
00062 
00066         public override int GetHashCode()
00067         {
00068             return base.GetHashCode();
00069         }
00070 
00074         public override string ToString()
00075         {
00076             return Native.Z3_func_decl_to_string(Context.nCtx, NativeObject);
00077         }
00078 
00082         new public uint Id
00083         {
00084             get { return Native.Z3_get_func_decl_id(Context.nCtx, NativeObject); }
00085         }
00086 
00090         public uint Arity
00091         {
00092             get { return Native.Z3_get_arity(Context.nCtx, NativeObject); }
00093         }
00094 
00099         public uint DomainSize
00100         {
00101             get { return Native.Z3_get_domain_size(Context.nCtx, NativeObject); }
00102         }
00103 
00107         public Sort[] Domain
00108         {
00109             get
00110             {
00111                 Contract.Ensures(Contract.Result<Sort[]>() != null);
00112 
00113                 uint n = DomainSize;
00114 
00115                 Sort[] res = new Sort[n];
00116                 for (uint i = 0; i < n; i++)
00117                     res[i] = Sort.Create(Context, Native.Z3_get_domain(Context.nCtx, NativeObject, i));
00118                 return res;
00119             }
00120         }
00121 
00125         public Sort Range
00126         {
00127             get
00128             {
00129                 Contract.Ensures(Contract.Result<Sort>() != null);
00130                 return Sort.Create(Context, Native.Z3_get_range(Context.nCtx, NativeObject));
00131             }
00132         }
00133 
00137         public Z3_decl_kind DeclKind
00138         {
00139             get { return (Z3_decl_kind)Native.Z3_get_decl_kind(Context.nCtx, NativeObject); }
00140         }
00141 
00145         public Symbol Name
00146         {
00147             get
00148             {
00149                 Contract.Ensures(Contract.Result<Symbol>() != null);
00150                 return Symbol.Create(Context, Native.Z3_get_decl_name(Context.nCtx, NativeObject));
00151             }
00152         }
00153 
00157         public uint NumParameters
00158         {
00159             get { return Native.Z3_get_decl_num_parameters(Context.nCtx, NativeObject); }
00160         }
00161 
00165         public Parameter[] Parameters
00166         {
00167             get
00168             {
00169                 Contract.Ensures(Contract.Result<Parameter[]>() != null);
00170 
00171                 uint num = NumParameters;
00172                 Parameter[] res = new Parameter[num];
00173                 for (uint i = 0; i < num; i++)
00174                 {
00175                     Z3_parameter_kind k = (Z3_parameter_kind)Native.Z3_get_decl_parameter_kind(Context.nCtx, NativeObject, i);
00176                     switch (k)
00177                     {
00178                         case Z3_parameter_kind.Z3_PARAMETER_INT:
00179                             res[i] = new Parameter(k, Native.Z3_get_decl_int_parameter(Context.nCtx, NativeObject, i));
00180                             break;
00181                         case Z3_parameter_kind.Z3_PARAMETER_DOUBLE:
00182                             res[i] = new Parameter(k, Native.Z3_get_decl_double_parameter(Context.nCtx, NativeObject, i));
00183                             break;
00184                         case Z3_parameter_kind.Z3_PARAMETER_SYMBOL:
00185                             res[i] = new Parameter(k, Symbol.Create(Context, Native.Z3_get_decl_symbol_parameter(Context.nCtx, NativeObject, i)));
00186                             break;
00187                         case Z3_parameter_kind.Z3_PARAMETER_SORT:
00188                             res[i] = new Parameter(k, Sort.Create(Context, Native.Z3_get_decl_sort_parameter(Context.nCtx, NativeObject, i)));
00189                             break;
00190                         case Z3_parameter_kind.Z3_PARAMETER_AST:
00191                             res[i] = new Parameter(k, new AST(Context, Native.Z3_get_decl_ast_parameter(Context.nCtx, NativeObject, i)));
00192                             break;
00193                         case Z3_parameter_kind.Z3_PARAMETER_FUNC_DECL:
00194                             res[i] = new Parameter(k, new FuncDecl(Context, Native.Z3_get_decl_func_decl_parameter(Context.nCtx, NativeObject, i)));
00195                             break;
00196                         case Z3_parameter_kind.Z3_PARAMETER_RATIONAL:
00197                             res[i] = new Parameter(k, Native.Z3_get_decl_rational_parameter(Context.nCtx, NativeObject, i));
00198                             break;
00199                         default:
00200                             throw new Z3Exception("Unknown function declaration parameter kind encountered");
00201                     }
00202                 }
00203                 return res;
00204             }
00205         }
00206 
00210         public class Parameter
00211         {
00212             readonly private Z3_parameter_kind kind;
00213             readonly private int i;
00214             readonly private double d;
00215             readonly private Symbol sym;
00216             readonly private Sort srt;
00217             readonly private AST ast;
00218             readonly private FuncDecl fd;
00219             readonly private string r;
00220 
00222             public int Int { get { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_INT) throw new Z3Exception("parameter is not an int"); return i; } }
00224             public double Double { get { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_DOUBLE) throw new Z3Exception("parameter is not a double "); return d; } }
00226             public Symbol Symbol { get { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_SYMBOL) throw new Z3Exception("parameter is not a Symbol"); return sym; } }
00228             public Sort Sort { get { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_SORT) throw new Z3Exception("parameter is not a Sort"); return srt; } }
00230             public AST AST { get { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_AST) throw new Z3Exception("parameter is not an AST"); return ast; } }
00232             public FuncDecl FuncDecl { get { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_FUNC_DECL) throw new Z3Exception("parameter is not a function declaration"); return fd; } }
00234             public string Rational { get { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_RATIONAL) throw new Z3Exception("parameter is not a rational string"); return r; } }
00235 
00239             public Z3_parameter_kind ParameterKind { get { return kind; } }
00240 
00241             #region Internal
00242             internal Parameter(Z3_parameter_kind k, int i)
00243             {
00244                 this.kind = k;
00245                 this.i = i;
00246             }
00247 
00248             internal Parameter(Z3_parameter_kind k, double d)
00249             {
00250                 this.kind = k;
00251                 this.d = d;
00252             }
00253 
00254             internal Parameter(Z3_parameter_kind k, Symbol s)
00255             {
00256                 this.kind = k;
00257                 this.sym = s;
00258             }
00259 
00260             internal Parameter(Z3_parameter_kind k, Sort s)
00261             {
00262                 this.kind = k;
00263                 this.srt = s;
00264             }
00265 
00266             internal Parameter(Z3_parameter_kind k, AST a)
00267             {
00268                 this.kind = k;
00269                 this.ast = a;
00270             }
00271 
00272             internal Parameter(Z3_parameter_kind k, FuncDecl fd)
00273             {
00274                 this.kind = k;
00275                 this.fd = fd;
00276             }
00277 
00278             internal Parameter(Z3_parameter_kind k, string r)
00279             {
00280                 this.kind = k;
00281                 this.r = r;
00282             }
00283             #endregion
00284         }
00285 
00286         #region Internal
00287         internal FuncDecl(Context ctx, IntPtr obj)
00288             : base(ctx, obj)
00289         {
00290             Contract.Requires(ctx != null);
00291         }
00292 
00293         internal FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range)
00294             : base(ctx, Native.Z3_mk_func_decl(ctx.nCtx, name.NativeObject, AST.ArrayLength(domain), AST.ArrayToNative(domain), range.NativeObject))
00295         {
00296             Contract.Requires(ctx != null);
00297             Contract.Requires(name != null);
00298             Contract.Requires(range != null);
00299         }
00300 
00301         internal FuncDecl(Context ctx, string prefix, Sort[] domain, Sort range)
00302             : base(ctx, Native.Z3_mk_fresh_func_decl(ctx.nCtx, prefix, AST.ArrayLength(domain), AST.ArrayToNative(domain), range.NativeObject))
00303         {
00304             Contract.Requires(ctx != null);
00305             Contract.Requires(range != null);
00306         }
00307 
00308 #if DEBUG
00309         internal override void CheckNativeObject(IntPtr obj)
00310         {
00311             if (Native.Z3_get_ast_kind(Context.nCtx, obj) != (uint)Z3_ast_kind.Z3_FUNC_DECL_AST)
00312                 throw new Z3Exception("Underlying object is not a function declaration");
00313             base.CheckNativeObject(obj);
00314         }
00315 #endif
00316         #endregion
00317 
00323         public Expr this[params Expr[] args]
00324         {
00325             get
00326             {
00327                 Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
00328 
00329                 return Apply(args);
00330             }
00331         }
00332 
00338         public Expr Apply(params Expr[] args)
00339         {
00340             Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
00341 
00342             Context.CheckContextMatch(args);
00343             return Expr.Create(Context, this, args);
00344         }
00345 
00346     }
00347 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines