Z3
Protected Member Functions
BoolExpr Class Reference
+ Inheritance diagram for BoolExpr:

Protected Member Functions

 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
 

Additional Inherited Members

- 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
 

Detailed Description

Boolean expressions

Definition at line 23 of file BoolExpr.java.

Constructor & Destructor Documentation

BoolExpr ( Context  ctx)
inlineprotected

Constructor for BoolExpr

Definition at line 28 of file BoolExpr.java.

Referenced by Quantifier.getBody().

29  {
30  super(ctx);
31  }