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 
148  Quantifier(Context ctx, boolean isForall, Sort[] sorts, Symbol[] names,
149  Expr body, int weight, Pattern[] patterns, Expr[] noPatterns,
150  Symbol quantifierID, Symbol skolemID)
151  {
152  super(ctx, 0);
153 
154  getContext().checkContextMatch(patterns);
155  getContext().checkContextMatch(noPatterns);
156  getContext().checkContextMatch(sorts);
157  getContext().checkContextMatch(names);
158  getContext().checkContextMatch(body);
159 
160  if (sorts.length != names.length)
161  throw new Z3Exception(
162  "Number of sorts does not match number of names");
163 
164  if (noPatterns == null && quantifierID == null && skolemID == null)
165  {
166  setNativeObject(Native.mkQuantifier(ctx.nCtx(), (isForall) ? true
167  : false, weight, AST.arrayLength(patterns), AST
168  .arrayToNative(patterns), AST.arrayLength(sorts), AST
169  .arrayToNative(sorts), Symbol.arrayToNative(names), body
170  .getNativeObject()));
171  } else
172  {
173  setNativeObject(Native.mkQuantifierEx(ctx.nCtx(),
174  (isForall) ? true : false, weight, AST.getNativeObject(quantifierID),
175  AST.getNativeObject(skolemID),
176  AST.arrayLength(patterns), AST.arrayToNative(patterns),
177  AST.arrayLength(noPatterns), AST.arrayToNative(noPatterns),
178  AST.arrayLength(sorts), AST.arrayToNative(sorts),
179  Symbol.arrayToNative(names),
180  body.getNativeObject()));
181  }
182  }
183 
184  Quantifier(Context ctx, boolean isForall, Expr[] bound, Expr body,
185  int weight, Pattern[] patterns, Expr[] noPatterns,
186  Symbol quantifierID, Symbol skolemID)
187  {
188  super(ctx, 0);
189 
190  getContext().checkContextMatch(noPatterns);
191  getContext().checkContextMatch(patterns);
192  // Context().CheckContextMatch(bound);
193  getContext().checkContextMatch(body);
194 
195  if (noPatterns == null && quantifierID == null && skolemID == null)
196  {
197  setNativeObject(Native.mkQuantifierConst(ctx.nCtx(),
198  (isForall) ? true : false, weight, AST.arrayLength(bound),
199  AST.arrayToNative(bound), AST.arrayLength(patterns),
200  AST.arrayToNative(patterns), body.getNativeObject()));
201  } else
202  {
203  setNativeObject(Native.mkQuantifierConstEx(ctx.nCtx(),
204  (isForall) ? true : false, weight,
205  AST.getNativeObject(quantifierID),
206  AST.getNativeObject(skolemID), AST.arrayLength(bound),
207  AST.arrayToNative(bound), AST.arrayLength(patterns),
208  AST.arrayToNative(patterns), AST.arrayLength(noPatterns),
209  AST.arrayToNative(noPatterns), body.getNativeObject()));
210  }
211  }
212 
213  Quantifier(Context ctx, long obj)
214  {
215  super(ctx, obj);
216  }
217 
218  void checkNativeObject(long obj)
219  {
220  if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST
221  .toInt())
222  throw new Z3Exception("Underlying object is not a quantifier");
223  super.checkNativeObject(obj);
224  }
225 }
static long getQuantifierPatternAst(long a0, long a1, int a2)
Definition: Native.java:2720
static int getQuantifierNumPatterns(long a0, long a1)
Definition: Native.java:2711
static long getQuantifierBoundName(long a0, long a1, int a2)
Definition: Native.java:2756
static long getQuantifierBoundSort(long a0, long a1, int a2)
Definition: Native.java:2765
static long getQuantifierBody(long a0, long a1)
Definition: Native.java:2774
static long mkQuantifier(long a0, boolean a1, int a2, int a3, long[] a4, int a5, long[] a6, long[] a7, long a8)
Definition: Native.java:1973
static int getQuantifierNumNoPatterns(long a0, long a1)
Definition: Native.java:2729
static long mkQuantifierConst(long a0, boolean a1, int a2, int a3, long[] a4, int a5, long[] a6, long a7)
Definition: Native.java:2009
static long getQuantifierNoPatternAst(long a0, long a1, int a2)
Definition: Native.java:2738
static int getQuantifierNumBound(long a0, long a1)
Definition: Native.java:2747
static int getQuantifierWeight(long a0, long a1)
Definition: Native.java:2702
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:2018
static int getAstKind(long a0, long a1)
Definition: Native.java:2495
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:1982
static boolean isQuantifierForall(long a0, long a1)
Definition: Native.java:2693