00001
00018 package com.microsoft.z3;
00019
00020 import com.microsoft.z3.enumerations.Z3_ast_kind;
00021
00025 public class Quantifier extends BoolExpr
00026 {
00030 public boolean isUniversal() throws Z3Exception
00031 {
00032 return Native.isQuantifierForall(getContext().nCtx(), getNativeObject());
00033 }
00034
00038 public boolean isExistential() throws Z3Exception
00039 {
00040 return !isUniversal();
00041 }
00042
00046 public int getWeight() throws Z3Exception
00047 {
00048 return Native.getQuantifierWeight(getContext().nCtx(), getNativeObject());
00049 }
00050
00054 public int getNumPatterns() throws Z3Exception
00055 {
00056 return Native
00057 .getQuantifierNumPatterns(getContext().nCtx(), getNativeObject());
00058 }
00059
00065 public Pattern[] getPatterns() throws Z3Exception
00066 {
00067 int n = getNumPatterns();
00068 Pattern[] res = new Pattern[n];
00069 for (int i = 0; i < n; i++)
00070 res[i] = new Pattern(getContext(), Native.getQuantifierPatternAst(
00071 getContext().nCtx(), getNativeObject(), i));
00072 return res;
00073 }
00074
00078 public int getNumNoPatterns() throws Z3Exception
00079 {
00080 return Native.getQuantifierNumNoPatterns(getContext().nCtx(),
00081 getNativeObject());
00082 }
00083
00089 public Pattern[] getNoPatterns() throws Z3Exception
00090 {
00091 int n = getNumNoPatterns();
00092 Pattern[] res = new Pattern[n];
00093 for (int i = 0; i < n; i++)
00094 res[i] = new Pattern(getContext(), Native.getQuantifierNoPatternAst(
00095 getContext().nCtx(), getNativeObject(), i));
00096 return res;
00097 }
00098
00102 public int getNumBound() throws Z3Exception
00103 {
00104 return Native.getQuantifierNumBound(getContext().nCtx(), getNativeObject());
00105 }
00106
00112 public Symbol[] getBoundVariableNames() throws Z3Exception
00113 {
00114 int n = getNumBound();
00115 Symbol[] res = new Symbol[n];
00116 for (int i = 0; i < n; i++)
00117 res[i] = Symbol.create(getContext(), Native.getQuantifierBoundName(
00118 getContext().nCtx(), getNativeObject(), i));
00119 return res;
00120 }
00121
00127 public Sort[] getBoundVariableSorts() throws Z3Exception
00128 {
00129 int n = getNumBound();
00130 Sort[] res = new Sort[n];
00131 for (int i = 0; i < n; i++)
00132 res[i] = Sort.create(getContext(), Native.getQuantifierBoundSort(
00133 getContext().nCtx(), getNativeObject(), i));
00134 return res;
00135 }
00136
00142 public BoolExpr getBody() throws Z3Exception
00143 {
00144 return new BoolExpr(getContext(), Native.getQuantifierBody(getContext()
00145 .nCtx(), getNativeObject()));
00146 }
00147
00148 Quantifier(Context ctx, boolean isForall, Sort[] sorts, Symbol[] names,
00149 Expr body, int weight, Pattern[] patterns, Expr[] noPatterns,
00150 Symbol quantifierID, Symbol skolemID) throws Z3Exception
00151 {
00152 super(ctx);
00153
00154 getContext().checkContextMatch(patterns);
00155 getContext().checkContextMatch(noPatterns);
00156 getContext().checkContextMatch(sorts);
00157 getContext().checkContextMatch(names);
00158 getContext().checkContextMatch(body);
00159
00160 if (sorts.length != names.length)
00161 throw new Z3Exception(
00162 "Number of sorts does not match number of names");
00163
00164 if (noPatterns == null && quantifierID == null && skolemID == null)
00165 {
00166 setNativeObject(Native.mkQuantifier(ctx.nCtx(), (isForall) ? true
00167 : false, weight, AST.arrayLength(patterns), AST
00168 .arrayToNative(patterns), AST.arrayLength(sorts), AST
00169 .arrayToNative(sorts), Symbol.arrayToNative(names), body
00170 .getNativeObject()));
00171 } else
00172 {
00173 setNativeObject(Native.mkQuantifierEx(ctx.nCtx(),
00174 (isForall) ? true : false, weight, AST.getNativeObject(quantifierID),
00175 AST.getNativeObject(skolemID),
00176 AST.arrayLength(patterns), AST.arrayToNative(patterns),
00177 AST.arrayLength(noPatterns), AST.arrayToNative(noPatterns),
00178 AST.arrayLength(sorts), AST.arrayToNative(sorts),
00179 Symbol.arrayToNative(names),
00180 body.getNativeObject()));
00181 }
00182 }
00183
00184 Quantifier(Context ctx, boolean isForall, Expr[] bound, Expr body,
00185 int weight, Pattern[] patterns, Expr[] noPatterns,
00186 Symbol quantifierID, Symbol skolemID) throws Z3Exception
00187 {
00188 super(ctx);
00189
00190 getContext().checkContextMatch(noPatterns);
00191 getContext().checkContextMatch(patterns);
00192
00193 getContext().checkContextMatch(body);
00194
00195 if (noPatterns == null && quantifierID == null && skolemID == null)
00196 {
00197 setNativeObject(Native.mkQuantifierConst(ctx.nCtx(),
00198 (isForall) ? true : false, weight, AST.arrayLength(bound),
00199 AST.arrayToNative(bound), AST.arrayLength(patterns),
00200 AST.arrayToNative(patterns), body.getNativeObject()));
00201 } else
00202 {
00203 setNativeObject(Native.mkQuantifierConstEx(ctx.nCtx(),
00204 (isForall) ? true : false, weight,
00205 AST.getNativeObject(quantifierID),
00206 AST.getNativeObject(skolemID), AST.arrayLength(bound),
00207 AST.arrayToNative(bound), AST.arrayLength(patterns),
00208 AST.arrayToNative(patterns), AST.arrayLength(noPatterns),
00209 AST.arrayToNative(noPatterns), body.getNativeObject()));
00210 }
00211 }
00212
00213 Quantifier(Context ctx, long obj) throws Z3Exception
00214 {
00215 super(ctx, obj);
00216 }
00217
00218 void checkNativeObject(long obj) throws Z3Exception
00219 {
00220 if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST
00221 .toInt())
00222 throw new Z3Exception("Underlying object is not a quantifier");
00223 super.checkNativeObject(obj);
00224 }
00225 }