Z3 |

SeqExpr< R extends Sort > Class Template Reference
Inheritance diagram for SeqExpr< R extends Sort >:

## Additional Inherited Members
Public Member Functions inherited from Expr< SeqSort< R > >
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 ()
Protected Member Functions inherited from Expr< SeqSort< R > >
| Expr (Context ctx, long obj)

## Detailed Description

Seq expressions

Definition at line 23 of file SeqExpr.java.