Public Member Functions | |
int | getSortSize () throws Z3Exception |
![]() | |
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 |
![]() | |
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 |
![]() | |
void | dispose () throws Z3Exception |
![]() | |
void | dispose () throws Z3Exception |
Additional Inherited Members | |
![]() | |
Expr (Context ctx) | |
Expr (Context ctx, long obj) throws Z3Exception | |
![]() | |
void | finalize () throws Z3Exception |
Bit-vector expressions
Definition at line 23 of file BitVecExpr.java.
|
inline |
The size of the sort of a bit-vector term.
Z3Exception |
Definition at line 30 of file BitVecExpr.java.