|
Z3
|
|
|
Z3
|
|
Inheritance diagram for DatatypeExpr:Additional Inherited Members | |
| Public Member Functions inherited from Expr | |
| Expr | simplify () |
| Expr | simplify (Params p) |
| FuncDecl | getFuncDecl () |
| Z3_lbool | getBoolValue () |
| int | getNumArgs () |
| Expr [] | getArgs () |
| Expr | update (Expr[] args) |
| Expr | substitute (Expr[] from, Expr[] to) |
| Expr | substitute (Expr from, Expr to) |
| Expr | substituteVars (Expr[] to) |
| Expr | translate (Context ctx) |
| String | toString () |
| boolean | isNumeral () |
| boolean | isWellSorted () |
| Sort | 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 | 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 | isProofPullQuantStar () |
| 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 | isProofNNFStar () |
| boolean | isProofCNFStar () |
| 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 () |
| Public Member Functions inherited from AST | |
| boolean | equals (Object o) |
| int | compareTo (AST other) |
| int | hashCode () |
| int | getId () |
| AST | translate (Context ctx) |
| Z3_ast_kind | getASTKind () |
| boolean | isExpr () |
| boolean | isApp () |
| boolean | isVar () |
| boolean | isQuantifier () |
| boolean | isSort () |
| boolean | isFuncDecl () |
| String | toString () |
| String | getSExpr () |
| Protected Member Functions inherited from Expr | |
| Expr (Context ctx, long obj) | |
Datatype expressions
Definition at line 23 of file DatatypeExpr.java.
1.8.15
