Z3
Public Member Functions
Quantifier Class Reference
+ Inheritance diagram for Quantifier:

Public Member Functions

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

Additional Inherited Members

- Protected Member Functions inherited from BoolExpr
 BoolExpr (Context ctx)
 
- Protected Member Functions inherited from Expr
 Expr (Context ctx)
 
 Expr (Context ctx, long obj) throws Z3Exception
 
- Protected Member Functions inherited from Z3Object
void finalize () throws Z3Exception
 

Detailed Description

Quantifier expressions.

Definition at line 25 of file Quantifier.java.

Member Function Documentation

BoolExpr getBody ( ) throws Z3Exception
inline

The body of the quantifier.

Exceptions
Z3Exception

Definition at line 142 of file Quantifier.java.

143  {
144  return new BoolExpr(getContext(), Native.getQuantifierBody(getContext()
145  .nCtx(), getNativeObject()));
146  }
Symbol [] getBoundVariableNames ( ) throws Z3Exception
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  }
Sort [] getBoundVariableSorts ( ) throws Z3Exception
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  }
Pattern [] getNoPatterns ( ) throws Z3Exception
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  }
int getNumBound ( ) throws Z3Exception
inline

The number of bound variables.

Definition at line 102 of file Quantifier.java.

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

103  {
104  return Native.getQuantifierNumBound(getContext().nCtx(), getNativeObject());
105  }
int getNumNoPatterns ( ) throws Z3Exception
inline

The number of no-patterns.

Definition at line 78 of file Quantifier.java.

Referenced by Quantifier.getNoPatterns().

79  {
80  return Native.getQuantifierNumNoPatterns(getContext().nCtx(),
81  getNativeObject());
82  }
int getNumPatterns ( ) throws Z3Exception
inline

The number of patterns.

Definition at line 54 of file Quantifier.java.

Referenced by Quantifier.getPatterns().

55  {
56  return Native
57  .getQuantifierNumPatterns(getContext().nCtx(), getNativeObject());
58  }
Pattern [] getPatterns ( ) throws Z3Exception
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  }
int getWeight ( ) throws Z3Exception
inline

The weight of the quantifier.

Definition at line 46 of file Quantifier.java.

47  {
48  return Native.getQuantifierWeight(getContext().nCtx(), getNativeObject());
49  }
boolean isExistential ( ) throws Z3Exception
inline

Indicates whether the quantifier is existential.

Definition at line 38 of file Quantifier.java.

39  {
40  return !isUniversal();
41  }
boolean isUniversal ( ) throws Z3Exception
inline

Indicates whether the quantifier is universal.

Definition at line 30 of file Quantifier.java.

Referenced by Quantifier.isExistential().

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