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 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)]
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)]
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
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 }