Z3
Quantifier.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
21 
25 public 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 !isUniversal();
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 
65  public Pattern[] getPatterns()
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 
142  public BoolExpr getBody()
143  {
144  return new BoolExpr(getContext(), Native.getQuantifierBody(getContext()
145  .nCtx(), getNativeObject()));
146  }
147 
156  public static Quantifier of(
157  Context ctx, boolean isForall, Sort[] sorts, Symbol[] names,
158  Expr body, int weight, Pattern[] patterns, Expr[] noPatterns,
159  Symbol quantifierID, Symbol skolemID) {
160  ctx.checkContextMatch(patterns);
161  ctx.checkContextMatch(noPatterns);
162  ctx.checkContextMatch(sorts);
163  ctx.checkContextMatch(names);
164  ctx.checkContextMatch(body);
165 
166  if (sorts.length != names.length) {
167  throw new Z3Exception(
168  "Number of sorts does not match number of names");
169  }
170 
171  long nativeObj;
172  if (noPatterns == null && quantifierID == null && skolemID == null) {
173  nativeObj = Native.mkQuantifier(ctx.nCtx(), (isForall), weight, AST.arrayLength(patterns), AST
174  .arrayToNative(patterns), AST.arrayLength(sorts), AST
175  .arrayToNative(sorts), Symbol.arrayToNative(names), body
176  .getNativeObject());
177  } else {
178  nativeObj = Native.mkQuantifierEx(ctx.nCtx(),
179  (isForall), weight, AST.getNativeObject(quantifierID),
180  AST.getNativeObject(skolemID),
181  AST.arrayLength(patterns), AST.arrayToNative(patterns),
182  AST.arrayLength(noPatterns), AST.arrayToNative(noPatterns),
183  AST.arrayLength(sorts), AST.arrayToNative(sorts),
184  Symbol.arrayToNative(names),
185  body.getNativeObject());
186  }
187  return new Quantifier(ctx, nativeObj);
188  }
189 
190 
202  public static Quantifier of(Context ctx, boolean isForall, Expr[] bound, Expr body,
203  int weight, Pattern[] patterns, Expr[] noPatterns,
204  Symbol quantifierID, Symbol skolemID) {
205  ctx.checkContextMatch(noPatterns);
206  ctx.checkContextMatch(patterns);
207  ctx.checkContextMatch(body);
208 
209  long nativeObj;
210  if (noPatterns == null && quantifierID == null && skolemID == null) {
211  nativeObj = Native.mkQuantifierConst(ctx.nCtx(),
212  isForall, weight, AST.arrayLength(bound),
213  AST.arrayToNative(bound), AST.arrayLength(patterns),
214  AST.arrayToNative(patterns), body.getNativeObject());
215  } else {
216  nativeObj = Native.mkQuantifierConstEx(ctx.nCtx(),
217  isForall, weight,
218  AST.getNativeObject(quantifierID),
219  AST.getNativeObject(skolemID), AST.arrayLength(bound),
220  AST.arrayToNative(bound), AST.arrayLength(patterns),
221  AST.arrayToNative(patterns), AST.arrayLength(noPatterns),
222  AST.arrayToNative(noPatterns), body.getNativeObject());
223  }
224  return new Quantifier(ctx, nativeObj);
225  }
226 
227  Quantifier(Context ctx, long obj)
228  {
229  super(ctx, obj);
230  }
231 
232  @Override
233  void checkNativeObject(long obj) {
234  if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST
235  .toInt()) {
236  throw new Z3Exception("Underlying object is not a quantifier");
237  }
238  super.checkNativeObject(obj);
239  }
240 }
static long getQuantifierPatternAst(long a0, long a1, int a2)
Definition: Native.java:2987
static int getQuantifierNumPatterns(long a0, long a1)
Definition: Native.java:2978
static long getQuantifierBoundName(long a0, long a1, int a2)
Definition: Native.java:3023
static Quantifier of(Context ctx, boolean isForall, Expr[] bound, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
static Quantifier of(Context ctx, boolean isForall, Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
static long getQuantifierBoundSort(long a0, long a1, int a2)
Definition: Native.java:3032
static long getQuantifierBody(long a0, long a1)
Definition: Native.java:3041
static long mkQuantifier(long a0, boolean a1, int a2, int a3, long[] a4, int a5, long[] a6, long[] a7, long a8)
Definition: Native.java:2231
static int getQuantifierNumNoPatterns(long a0, long a1)
Definition: Native.java:2996
static long mkQuantifierConst(long a0, boolean a1, int a2, int a3, long[] a4, int a5, long[] a6, long a7)
Definition: Native.java:2267
static long getQuantifierNoPatternAst(long a0, long a1, int a2)
Definition: Native.java:3005
static int getQuantifierNumBound(long a0, long a1)
Definition: Native.java:3014
static int getQuantifierWeight(long a0, long a1)
Definition: Native.java:2969
static long mkQuantifierConstEx(long a0, boolean a1, int a2, long a3, long a4, int a5, long[] a6, int a7, long[] a8, int a9, long[] a10, long a11)
Definition: Native.java:2276
static int getAstKind(long a0, long a1)
Definition: Native.java:2762
static long mkQuantifierEx(long a0, boolean a1, int a2, long a3, long a4, int a5, long[] a6, int a7, long[] a8, int a9, long[] a10, long[] a11, long a12)
Definition: Native.java:2240
static boolean isQuantifierForall(long a0, long a1)
Definition: Native.java:2960