Z3
Quantifier.java
Go to the documentation of this file.
1
18package com.microsoft.z3;
19
20import com.microsoft.z3.enumerations.Z3_ast_kind;
21
25public class Quantifier extends BoolExpr
26{
30 public boolean isUniversal()
31 {
32 return Native.isQuantifierForall(getContext().nCtx(), getNativeObject());
33 }
34
38 public boolean isExistential()
39 {
40 return Native.isQuantifierExists(getContext().nCtx(), getNativeObject());
41 }
42
46 public int getWeight()
47 {
48 return Native.getQuantifierWeight(getContext().nCtx(), getNativeObject());
49 }
50
54 public int getNumPatterns()
55 {
56 return Native
57 .getQuantifierNumPatterns(getContext().nCtx(), getNativeObject());
58 }
59
66 {
67 int n = getNumPatterns();
68 Pattern[] res = new Pattern[n];
69 for (int i = 0; i < n; i++)
70 res[i] = new Pattern(getContext(), Native.getQuantifierPatternAst(
71 getContext().nCtx(), getNativeObject(), i));
72 return res;
73 }
74
78 public int getNumNoPatterns()
79 {
80 return Native.getQuantifierNumNoPatterns(getContext().nCtx(),
81 getNativeObject());
82 }
83
90 {
91 int n = getNumNoPatterns();
92 Pattern[] res = new Pattern[n];
93 for (int i = 0; i < n; i++)
94 res[i] = new Pattern(getContext(), Native.getQuantifierNoPatternAst(
95 getContext().nCtx(), getNativeObject(), i));
96 return res;
97 }
98
102 public int getNumBound()
103 {
104 return Native.getQuantifierNumBound(getContext().nCtx(), getNativeObject());
105 }
106
113 {
114 int n = getNumBound();
115 Symbol[] res = new Symbol[n];
116 for (int i = 0; i < n; i++)
117 res[i] = Symbol.create(getContext(), Native.getQuantifierBoundName(
118 getContext().nCtx(), getNativeObject(), i));
119 return res;
120 }
121
128 {
129 int n = getNumBound();
130 Sort[] res = new Sort[n];
131 for (int i = 0; i < n; i++)
132 res[i] = Sort.create(getContext(), Native.getQuantifierBoundSort(
133 getContext().nCtx(), getNativeObject(), i));
134 return res;
135 }
136
143 {
144 return (BoolExpr) Expr.create(getContext(), Native.getQuantifierBody(getContext()
145 .nCtx(), getNativeObject()));
146 }
147
157 {
158 return (Quantifier) super.translate(ctx);
159 }
160
169 public static Quantifier of(
170 Context ctx, boolean isForall, Sort[] sorts, Symbol[] names,
171 Expr<BoolSort> body, int weight, Pattern[] patterns, Expr<?>[] noPatterns,
172 Symbol quantifierID, Symbol skolemID) {
173 ctx.checkContextMatch(patterns);
174 ctx.checkContextMatch(noPatterns);
175 ctx.checkContextMatch(sorts);
176 ctx.checkContextMatch(names);
177 ctx.checkContextMatch(body);
178
179 if (sorts.length != names.length) {
180 throw new Z3Exception(
181 "Number of sorts does not match number of names");
182 }
183
184 long nativeObj;
185 if (noPatterns == null && quantifierID == null && skolemID == null) {
186 nativeObj = Native.mkQuantifier(ctx.nCtx(), (isForall), weight, AST.arrayLength(patterns), AST
187 .arrayToNative(patterns), AST.arrayLength(sorts), AST
188 .arrayToNative(sorts), Symbol.arrayToNative(names), body
189 .getNativeObject());
190 } else {
191 nativeObj = Native.mkQuantifierEx(ctx.nCtx(),
192 (isForall), weight, AST.getNativeObject(quantifierID),
193 AST.getNativeObject(skolemID),
194 AST.arrayLength(patterns), AST.arrayToNative(patterns),
195 AST.arrayLength(noPatterns), AST.arrayToNative(noPatterns),
196 AST.arrayLength(sorts), AST.arrayToNative(sorts),
197 Symbol.arrayToNative(names),
198 body.getNativeObject());
199 }
200 return new Quantifier(ctx, nativeObj);
201 }
202
203
215 public static Quantifier of(Context ctx, boolean isForall, Expr<?>[] bound, Expr<BoolSort> body,
216 int weight, Pattern[] patterns, Expr<?>[] noPatterns,
217 Symbol quantifierID, Symbol skolemID) {
218 ctx.checkContextMatch(noPatterns);
219 ctx.checkContextMatch(patterns);
220 ctx.checkContextMatch(body);
221
222 long nativeObj;
223 if (noPatterns == null && quantifierID == null && skolemID == null) {
224 nativeObj = Native.mkQuantifierConst(ctx.nCtx(),
225 isForall, weight, AST.arrayLength(bound),
226 AST.arrayToNative(bound), AST.arrayLength(patterns),
227 AST.arrayToNative(patterns), body.getNativeObject());
228 } else {
229 nativeObj = Native.mkQuantifierConstEx(ctx.nCtx(),
230 isForall, weight,
231 AST.getNativeObject(quantifierID),
232 AST.getNativeObject(skolemID), AST.arrayLength(bound),
233 AST.arrayToNative(bound), AST.arrayLength(patterns),
234 AST.arrayToNative(patterns), AST.arrayLength(noPatterns),
235 AST.arrayToNative(noPatterns), body.getNativeObject());
236 }
237 return new Quantifier(ctx, nativeObj);
238 }
239
240 Quantifier(Context ctx, long obj)
241 {
242 super(ctx, obj);
243 }
244
245 @Override
246 void checkNativeObject(long obj) {
247 if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST
248 .toInt()) {
249 throw new Z3Exception("Underlying object is not a quantifier");
250 }
251 super.checkNativeObject(obj);
252 }
253}
static Quantifier of(Context ctx, boolean isForall, Expr<?>[] bound, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
Quantifier translate(Context ctx)
static Quantifier of(Context ctx, boolean isForall, Sort[] sorts, Symbol[] names, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
static long[] arrayToNative(Z3Object[] a)
Definition: Z3Object.java:73
static int arrayLength(Z3Object[] a)
Definition: Z3Object.java:83
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
Definition: z3_api.h:180