Z3 |

Public Member Functions | Static Public Member Functions
Quantifier Class Reference
Inheritance diagram for Quantifier:

## Public Member Functions
boolean | isUniversal ()
boolean | isExistential ()
int | getWeight ()
int | getNumPatterns ()
Pattern[] | getPatterns ()
int | getNumNoPatterns ()
Pattern[] | getNoPatterns ()
int | getNumBound ()
Symbol[] | getBoundVariableNames ()
Sort[] | getBoundVariableSorts ()
BoolExpr | getBody ()
Quantifier | translate (Context ctx)
Public Member Functions inherited from Expr< BoolSort >
Expr< R > | simplify ()
Expr< R > | simplify (Params p)
FuncDecl< R > | getFuncDecl ()
Z3_lbool | getBoolValue ()
int | getNumArgs ()
Expr<?>[] | getArgs ()
Expr< R > | update (Expr<?>[] args)
Expr< R > | substitute (Expr<?>[] from, Expr<?>[] to)
Expr< R > | substitute (Expr<?> from, Expr<?> to)
Expr< R > | substituteVars (Expr<?>[] to)
Expr< R > | translate (Context ctx)
String | toString ()
boolean | isNumeral ()
boolean | isWellSorted ()
R | getSort ()
boolean | isConst ()
boolean | isIntNum ()
boolean | isRatNum ()
boolean | isAlgebraicNumber ()
boolean | isBool ()
boolean | isTrue ()
boolean | isFalse ()
boolean | isEq ()
boolean | isDistinct ()
boolean | isITE ()
boolean | isAnd ()
boolean | isOr ()
boolean | isIff ()
boolean | isXor ()
boolean | isNot ()
boolean | isImplies ()
boolean | isInt ()
boolean | isReal ()
boolean | isArithmeticNumeral ()
boolean | isLE ()
boolean | isGE ()
boolean | isLT ()
boolean | isGT ()
boolean | isAdd ()
boolean | isSub ()
boolean | isUMinus ()
boolean | isMul ()
boolean | isDiv ()
boolean | isIDiv ()
boolean | isRemainder ()
boolean | isModulus ()
boolean | isIntToReal ()
boolean | isRealToInt ()
boolean | isRealIsInt ()
boolean | isArray ()
boolean | isStore ()
boolean | isSelect ()
boolean | isConstantArray ()
boolean | isDefaultArray ()
boolean | isArrayMap ()
boolean | isAsArray ()
boolean | isSetUnion ()
boolean | isSetIntersect ()
boolean | isSetDifference ()
boolean | isSetComplement ()
boolean | isSetSubset ()
boolean | isBV ()
boolean | isBVNumeral ()
boolean | isBVBitOne ()
boolean | isBVBitZero ()
boolean | isBVUMinus ()
boolean | isBVAdd ()
boolean | isBVSub ()
boolean | isBVMul ()
boolean | isBVSDiv ()
boolean | isBVUDiv ()
boolean | isBVSRem ()
boolean | isBVURem ()
boolean | isBVSMod ()
boolean | isBVULE ()
boolean | isBVSLE ()
boolean | isBVUGE ()
boolean | isBVSGE ()
boolean | isBVULT ()
boolean | isBVSLT ()
boolean | isBVUGT ()
boolean | isBVSGT ()
boolean | isBVAND ()
boolean | isBVOR ()
boolean | isBVNOT ()
boolean | isBVXOR ()
boolean | isBVNAND ()
boolean | isBVNOR ()
boolean | isBVXNOR ()
boolean | isBVConcat ()
boolean | isBVSignExtension ()
boolean | isBVZeroExtension ()
boolean | isBVExtract ()
boolean | isBVRepeat ()
boolean | isBVReduceOR ()
boolean | isBVReduceAND ()
boolean | isBVComp ()
boolean | isBVShiftLeft ()
boolean | isBVShiftRightLogical ()
boolean | isBVShiftRightArithmetic ()
boolean | isBVRotateLeft ()
boolean | isBVRotateRight ()
boolean | isBVRotateLeftExtended ()
boolean | isBVRotateRightExtended ()
boolean | isIntToBV ()
boolean | isBVToInt ()
boolean | isBVCarry ()
boolean | isBVXOR3 ()
boolean | isLabel ()
boolean | isLabelLit ()
boolean | isString ()
String | getString ()
boolean | isConcat ()
boolean | isOEQ ()
boolean | isProofTrue ()
boolean | isProofAsserted ()
boolean | isProofGoal ()
boolean | isProofModusPonens ()
boolean | isProofReflexivity ()
boolean | isProofSymmetry ()
boolean | isProofTransitivity ()
boolean | isProofTransitivityStar ()
boolean | isProofMonotonicity ()
boolean | isProofQuantIntro ()
boolean | isProofDistributivity ()
boolean | isProofAndElimination ()
boolean | isProofOrElimination ()
boolean | isProofRewrite ()
boolean | isProofRewriteStar ()
boolean | isProofPullQuant ()
boolean | isProofPushQuant ()
boolean | isProofElimUnusedVars ()
boolean | isProofDER ()
boolean | isProofQuantInst ()
boolean | isProofHypothesis ()
boolean | isProofLemma ()
boolean | isProofUnitResolution ()
boolean | isProofIFFTrue ()
boolean | isProofIFFFalse ()
boolean | isProofCommutativity ()
boolean | isProofDefAxiom ()
boolean | isProofDefIntro ()
boolean | isProofApplyDef ()
boolean | isProofIFFOEQ ()
boolean | isProofNNFPos ()
boolean | isProofNNFNeg ()
boolean | isProofSkolemize ()
boolean | isProofModusPonensOEQ ()
boolean | isProofTheoryLemma ()
boolean | isRelation ()
boolean | isRelationStore ()
boolean | isEmptyRelation ()
boolean | isIsEmptyRelation ()
boolean | isRelationalJoin ()
boolean | isRelationUnion ()
boolean | isRelationWiden ()
boolean | isRelationProject ()
boolean | isRelationFilter ()
boolean | isRelationNegationFilter ()
boolean | isRelationRename ()
boolean | isRelationComplement ()
boolean | isRelationSelect ()
boolean | isRelationClone ()
boolean | isFiniteDomain ()
boolean | isFiniteDomainLT ()
int | getIndex ()

## Static Public Member Functions
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 Quantifier | of (Context ctx, boolean isForall, Expr<?>[] bound, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)

## Additional Inherited Members
Protected Member Functions inherited from Expr< BoolSort >
| Expr (Context ctx, long obj)

## Detailed Description

Quantifier expressions.

Definition at line 25 of file Quantifier.java.

## Member Function Documentation

## ◆ getBody()

BoolExpr getBody | ( |  | ) |
| inline

The body of the quantifier.

Exceptions

  Z3Exception |

Definition at line 142 of file Quantifier.java.

143 {
144 return (BoolExpr) Expr.create(getContext(), Native.getQuantifierBody(getContext()
145 .nCtx(), getNativeObject()));
146 }
com.microsoft.z3.Expr< BoolSort >::Expr
Expr(Context ctx, long obj)
Definition: Expr.java:2119

## ◆ getBoundVariableNames()

Symbol[] getBoundVariableNames | ( |  | ) |
| inline

The symbols for the bound variables.

Exceptions

  Z3Exception |

Definition at line 112 of file Quantifier.java.

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 }
com.microsoft.z3.Quantifier.getNumBound
int getNumBound()
Definition: Quantifier.java:102

## ◆ getBoundVariableSorts()

Sort[] getBoundVariableSorts | ( |  | ) |
| inline

The sorts of the bound variables.

Exceptions

  Z3Exception |

Definition at line 127 of file Quantifier.java.

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 }

## ◆ getNoPatterns()

Pattern[] getNoPatterns | ( |  | ) |
| inline

The no-patterns.

Exceptions

  Z3Exception |

Definition at line 89 of file Quantifier.java.

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 }
com.microsoft.z3.Quantifier.getNumNoPatterns
int getNumNoPatterns()
Definition: Quantifier.java:78

## ◆ getNumBound()

int getNumBound | ( |  | ) |
| inline

The number of bound variables.

Definition at line 102 of file Quantifier.java.

103 {
104 return Native.getQuantifierNumBound(getContext().nCtx(), getNativeObject());
105 }

Referenced by Quantifier.getBoundVariableNames(), and Quantifier.getBoundVariableSorts().

## ◆ getNumNoPatterns()

int getNumNoPatterns | ( |  | ) |
| inline

The number of no-patterns.

Definition at line 78 of file Quantifier.java.

79 {
80 return Native.getQuantifierNumNoPatterns(getContext().nCtx(),
81 getNativeObject());
82 }

Referenced by Quantifier.getNoPatterns().

## ◆ getNumPatterns()

int getNumPatterns | ( |  | ) |
| inline

The number of patterns.

Definition at line 54 of file Quantifier.java.

55 {
56 return Native
57 .getQuantifierNumPatterns(getContext().nCtx(), getNativeObject());
58 }

Referenced by Quantifier.getPatterns().

## ◆ getPatterns()

Pattern[] getPatterns | ( |  | ) |
| inline

The patterns.

Exceptions

  Z3Exception |

Definition at line 65 of file Quantifier.java.

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 }
com.microsoft.z3.Quantifier.getNumPatterns
int getNumPatterns()
Definition: Quantifier.java:54

## ◆ getWeight()

int getWeight | ( |  | ) |
| inline

The weight of the quantifier.

Definition at line 46 of file Quantifier.java.

47 {
48 return Native.getQuantifierWeight(getContext().nCtx(), getNativeObject());
49 }

## ◆ isExistential()

boolean isExistential | ( |  | ) |
| inline

Indicates whether the quantifier is existential.

Definition at line 38 of file Quantifier.java.

39 {
40 return Native.isQuantifierExists(getContext().nCtx(), getNativeObject());
41 }

## ◆ isUniversal()

boolean isUniversal | ( |  | ) |
| inline

Indicates whether the quantifier is universal.

Definition at line 30 of file Quantifier.java.

31 {
32 return Native.isQuantifierForall(getContext().nCtx(), getNativeObject());
33 }

## ◆ of() [1/2]

static Quantifier of | ( | Context | ctx,
|  | boolean | isForall,
|  | Expr<?>[] | bound,
|  | Expr< BoolSort > | body,
|  | int | weight,
|  | Pattern[] | patterns,
|  | Expr<?>[] | noPatterns,
|  | Symbol | quantifierID,
|  | Symbol | skolemID
| ) |  |
| inline static

Parameters

  ctx | Context to create the quantifier on.
  isForall | Quantifier type.
  bound | Bound variables.
  body | Body of the quantifier.
  weight | Weight.
  patterns | Nullable array of patterns.
  noPatterns | Nullable array of noPatterns.
  quantifierID | Nullable quantifier identifier.
  skolemID | Nullable skolem identifier.

Definition at line 215 of file Quantifier.java.

217 {
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 }

## ◆ of() [2/2]

static Quantifier of | ( | Context | ctx,
|  | boolean | isForall,
|  | Sort[] | sorts,
|  | Symbol[] | names,
|  | Expr< BoolSort > | body,
|  | int | weight,
|  | Pattern[] | patterns,
|  | Expr<?>[] | noPatterns,
|  | Symbol | quantifierID,
|  | Symbol | skolemID
| ) |  |
| inline static

Create a quantified expression.

Parameters

  patterns | Nullable patterns
  noPatterns | Nullable noPatterns
  quantifierID | Nullable quantifierID
  skolemID | Nullable skolemID

Definition at line 169 of file Quantifier.java.

172 {
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 }

Referenced by Context.mkExists(), and Context.mkForall().

## ◆ translate()

Quantifier translate | ( | Context | ctx | ) |
| inline

Translates (copies) the quantifier to the Context `ctx`.

Parameters

  ctx | A context

Returns
  A copy of the quantifier which is associated with `ctx`

Exceptions

  Z3Exception | on error

Definition at line 156 of file Quantifier.java.

157 {
158 return (Quantifier) super.translate(ctx);
159 }

Referenced by AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), Solver.__copy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), Solver.__deepcopy__(), and Quantifier.translate().