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 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 
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 Expr getBody()
143  {
144  return 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 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 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 }
com.microsoft.z3.Quantifier.getNoPatterns
Pattern[] getNoPatterns()
Definition: Quantifier.java:89
com.microsoft.z3.Native.getQuantifierNoPatternAst
static long getQuantifierNoPatternAst(long a0, long a1, int a2)
Definition: Native.java:3395
com.microsoft.z3.enumerations
Definition: Z3_ast_kind.java:5
com.microsoft.z3.Sort
Definition: Sort.java:26
com.microsoft.z3.Native.getQuantifierBoundSort
static long getQuantifierBoundSort(long a0, long a1, int a2)
Definition: Native.java:3422
com.microsoft.z3.Native.isQuantifierForall
static boolean isQuantifierForall(long a0, long a1)
Definition: Native.java:3332
com.microsoft
com.microsoft.z3.Quantifier.getNumPatterns
int getNumPatterns()
Definition: Quantifier.java:54
com.microsoft.z3.Quantifier.getBody
Expr getBody()
Definition: Quantifier.java:142
com.microsoft.z3.Quantifier.isExistential
boolean isExistential()
Definition: Quantifier.java:38
com.microsoft.z3.Native.getQuantifierPatternAst
static long getQuantifierPatternAst(long a0, long a1, int a2)
Definition: Native.java:3377
com.microsoft.z3.Quantifier.isUniversal
boolean isUniversal()
Definition: Quantifier.java:30
com.microsoft.z3.Quantifier
Definition: Quantifier.java:25
com.microsoft.z3.Native.getQuantifierBody
static long getQuantifierBody(long a0, long a1)
Definition: Native.java:3431
com.microsoft.z3.Symbol
Definition: Symbol.java:25
com.microsoft.z3.Pattern
Definition: Pattern.java:24
com.microsoft.z3.Quantifier.getBoundVariableNames
Symbol[] getBoundVariableNames()
Definition: Quantifier.java:112
com.microsoft.z3.Native.getQuantifierNumBound
static int getQuantifierNumBound(long a0, long a1)
Definition: Native.java:3404
com.microsoft.z3.BoolExpr
Definition: BoolExpr.java:23
com.microsoft.z3.Quantifier.of
static Quantifier of(Context ctx, boolean isForall, Expr[] bound, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Quantifier.java:215
com.microsoft.z3.Quantifier.translate
Quantifier translate(Context ctx)
Definition: Quantifier.java:156
com.microsoft.z3.Quantifier.getBoundVariableSorts
Sort[] getBoundVariableSorts()
Definition: Quantifier.java:127
com.microsoft.z3.Native
Definition: Native.java:4
com.microsoft.z3.Native.getQuantifierNumPatterns
static int getQuantifierNumPatterns(long a0, long a1)
Definition: Native.java:3368
com.microsoft.z3
Definition: AlgebraicNum.java:18
com.microsoft.z3.Quantifier.of
static Quantifier of(Context ctx, boolean isForall, Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Quantifier.java:169
com.microsoft.z3.enumerations.Z3_ast_kind
Definition: Z3_ast_kind.java:13
com.microsoft.z3.Native.getQuantifierNumNoPatterns
static int getQuantifierNumNoPatterns(long a0, long a1)
Definition: Native.java:3386
com.microsoft.z3.Expr
Definition: Expr.java:30
com.microsoft.z3.Z3Exception
Definition: Z3Exception.java:25
com.microsoft.z3.AST
Definition: AST.java:25
com.microsoft.z3.Native.mkQuantifierConst
static long mkQuantifierConst(long a0, boolean a1, int a2, int a3, long[] a4, int a5, long[] a6, long a7)
Definition: Native.java:2594
com.microsoft.z3.Native.getQuantifierWeight
static int getQuantifierWeight(long a0, long a1)
Definition: Native.java:3359
com
com.microsoft.z3.Native.mkQuantifier
static long mkQuantifier(long a0, boolean a1, int a2, int a3, long[] a4, int a5, long[] a6, long[] a7, long a8)
Definition: Native.java:2558
com.microsoft.z3.Context
Definition: Context.java:35
com.microsoft.z3.Native.mkQuantifierEx
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:2567
com.microsoft.z3.Native.mkQuantifierConstEx
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:2603
Z3_ast_kind
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
Definition: z3_api.h:177
com.microsoft.z3.Quantifier.getWeight
int getWeight()
Definition: Quantifier.java:46
com.microsoft.z3.Quantifier.getNumBound
int getNumBound()
Definition: Quantifier.java:102
com.microsoft.z3.Quantifier.getPatterns
Pattern[] getPatterns()
Definition: Quantifier.java:65
com.microsoft.z3.Native.getQuantifierBoundName
static long getQuantifierBoundName(long a0, long a1, int a2)
Definition: Native.java:3413
com.microsoft.z3.Quantifier.getNumNoPatterns
int getNumNoPatterns()
Definition: Quantifier.java:78
com.microsoft.z3.Native.isQuantifierExists
static boolean isQuantifierExists(long a0, long a1)
Definition: Native.java:3341