00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
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 }