Z3
src/api/dotnet/Quantifier.cs
Go to the documentation of this file.
00001 /*++
00002 Copyright (c) 2012 Microsoft Corporation
00003 
00004 Module Name:
00005 
00006     Quantifier.cs
00007 
00008 Abstract:
00009 
00010     Z3 Managed API: Quantifiers
00011 
00012 Author:
00013 
00014     Christoph Wintersteiger (cwinter) 2012-03-19
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 Quantifier : BoolExpr
00030     {
00034         public bool IsUniversal
00035         {
00036             get { return Native.Z3_is_quantifier_forall(Context.nCtx, NativeObject) != 0; }
00037         }
00038 
00042         public bool IsExistential
00043         {
00044             get { return !IsUniversal; }
00045         }
00046 
00050         public uint Weight
00051         {
00052             get { return Native.Z3_get_quantifier_weight(Context.nCtx, NativeObject); }
00053         }
00054 
00058         public uint NumPatterns
00059         {
00060             get { return Native.Z3_get_quantifier_num_patterns(Context.nCtx, NativeObject); }
00061         }
00062 
00066         public Pattern[] Patterns
00067         {
00068             get
00069             {
00070                 Contract.Ensures(Contract.Result<Pattern[]>() != null);
00071 
00072                 uint n = NumPatterns;
00073                 Pattern[] res = new Pattern[n];
00074                 for (uint i = 0; i < n; i++)
00075                     res[i] = new Pattern(Context, Native.Z3_get_quantifier_pattern_ast(Context.nCtx, NativeObject, i));
00076                 return res;
00077             }
00078         }
00079 
00083         public uint NumNoPatterns
00084         {
00085             get { return Native.Z3_get_quantifier_num_no_patterns(Context.nCtx, NativeObject); }
00086         }
00087 
00091         public Pattern[] NoPatterns
00092         {
00093             get
00094             {
00095                 Contract.Ensures(Contract.Result<Pattern[]>() != null);
00096 
00097                 uint n = NumNoPatterns;
00098                 Pattern[] res = new Pattern[n];
00099                 for (uint i = 0; i < n; i++)
00100                     res[i] = new Pattern(Context, Native.Z3_get_quantifier_no_pattern_ast(Context.nCtx, NativeObject, i));
00101                 return res;
00102             }
00103         }
00104 
00108         public uint NumBound
00109         {
00110             get { return Native.Z3_get_quantifier_num_bound(Context.nCtx, NativeObject); }
00111         }
00112 
00116         public Symbol[] BoundVariableNames
00117         {
00118             get
00119             {
00120                 Contract.Ensures(Contract.Result<Symbol[]>() != null);
00121 
00122                 uint n = NumBound;
00123                 Symbol[] res = new Symbol[n];
00124                 for (uint i = 0; i < n; i++)
00125                     res[i] = Symbol.Create(Context, Native.Z3_get_quantifier_bound_name(Context.nCtx, NativeObject, i));
00126                 return res;
00127             }
00128         }
00129 
00133         public Sort[] BoundVariableSorts
00134         {
00135             get
00136             {
00137                 Contract.Ensures(Contract.Result<Sort[]>() != null);
00138 
00139                 uint n = NumBound;
00140                 Sort[] res = new Sort[n];
00141                 for (uint i = 0; i < n; i++)
00142                     res[i] = Sort.Create(Context, Native.Z3_get_quantifier_bound_sort(Context.nCtx, NativeObject, i));
00143                 return res;
00144             }
00145         }
00146 
00150         public BoolExpr Body
00151         {
00152             get
00153             {
00154                 Contract.Ensures(Contract.Result<BoolExpr>() != null);
00155 
00156                 return new BoolExpr(Context, Native.Z3_get_quantifier_body(Context.nCtx, NativeObject));
00157             }
00158         }
00159 
00160         #region Internal
00161         [ContractVerification(false)] // F: Clousot ForAll decompilation gets confused below. Setting verification off until I fixed the bug
00162         internal Quantifier(Context ctx, bool isForall, Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
00163             : base(ctx)
00164         {
00165             Contract.Requires(ctx != null);
00166             Contract.Requires(sorts != null);
00167             Contract.Requires(names != null);
00168             Contract.Requires(body != null);
00169             Contract.Requires(sorts.Length == names.Length);
00170             Contract.Requires(Contract.ForAll(sorts, s => s != null));
00171             Contract.Requires(Contract.ForAll(names, n => n != null));
00172             Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
00173             Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
00174 
00175             Context.CheckContextMatch(patterns);
00176             Context.CheckContextMatch(noPatterns);
00177             Context.CheckContextMatch(sorts);
00178             Context.CheckContextMatch(names);
00179             Context.CheckContextMatch(body);
00180 
00181             if (sorts.Length != names.Length)
00182                 throw new Z3Exception("Number of sorts does not match number of names");
00183 
00184             if (noPatterns == null && quantifierID == null && skolemID == null)
00185             {
00186                 NativeObject = Native.Z3_mk_quantifier(ctx.nCtx, (isForall) ? 1 : 0, weight,
00187                                            AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
00188                                            AST.ArrayLength(sorts), AST.ArrayToNative(sorts),
00189                                            Symbol.ArrayToNative(names),
00190                                            body.NativeObject);
00191             }
00192             else
00193             {
00194                 NativeObject = Native.Z3_mk_quantifier_ex(ctx.nCtx, (isForall) ? 1 : 0, weight,
00195                                   AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID),
00196                                   AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
00197                                   AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns),
00198                                   AST.ArrayLength(sorts), AST.ArrayToNative(sorts),
00199                                   Symbol.ArrayToNative(names),
00200                                   body.NativeObject);
00201             }
00202         }
00203 
00204         [ContractVerification(false)] // F: Clousot ForAll decompilation gets confused below. Setting verification off until I fixed the bug
00205         internal Quantifier(Context ctx, bool isForall, Expr[] bound, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
00206             : base(ctx)
00207         {
00208             Contract.Requires(ctx != null);
00209             Contract.Requires(body != null);
00210 
00211             Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
00212             Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
00213             Contract.Requires(bound == null || Contract.ForAll(bound, n => n != null));
00214 
00215             Context.CheckContextMatch(noPatterns);
00216             Context.CheckContextMatch(patterns);
00217             //Context.CheckContextMatch(bound);
00218             Context.CheckContextMatch(body);
00219 
00220             if (noPatterns == null && quantifierID == null && skolemID == null)
00221             {
00222                 NativeObject = Native.Z3_mk_quantifier_const(ctx.nCtx, (isForall) ? 1 : 0, weight,
00223                                                  AST.ArrayLength(bound), AST.ArrayToNative(bound),
00224                                                  AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
00225                                                  body.NativeObject);
00226             }
00227             else
00228             {
00229                 NativeObject = Native.Z3_mk_quantifier_const_ex(ctx.nCtx, (isForall) ? 1 : 0, weight,
00230                                         AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID),
00231                                         AST.ArrayLength(bound), AST.ArrayToNative(bound),
00232                                         AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
00233                                         AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns),
00234                                         body.NativeObject);
00235             }
00236         }
00237 
00238 
00239         internal Quantifier(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
00240 
00241 #if DEBUG
00242         internal override void CheckNativeObject(IntPtr obj)
00243         {
00244             if ((Z3_ast_kind)Native.Z3_get_ast_kind(Context.nCtx, obj) != Z3_ast_kind.Z3_QUANTIFIER_AST)
00245                 throw new Z3Exception("Underlying object is not a quantifier");
00246             base.CheckNativeObject(obj);
00247         }
00248 #endif
00249         #endregion
00250     }
00251 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines