Z3
- i -
Id :
AST
,
FuncDecl
,
Sort
Inconsistent :
Goal
Index :
Expr
Int :
BitVecNum
,
FiniteDomainNum
,
FuncDecl.Parameter
,
IntNum
,
IntSymbol
Int64 :
BitVecNum
,
FiniteDomainNum
,
IntNum
IntSort :
Context
IsAdd :
Expr
IsAlgebraicNumber :
Expr
IsAnd :
Expr
IsApp :
AST
IsArithmeticNumeral :
Expr
IsArray :
Expr
IsArrayMap :
Expr
IsAsArray :
Expr
IsBool :
Expr
IsBV :
Expr
IsBVAdd :
Expr
IsBVAND :
Expr
IsBVBitOne :
Expr
IsBVBitZero :
Expr
IsBVCarry :
Expr
IsBVComp :
Expr
IsBVConcat :
Expr
IsBVExtract :
Expr
IsBVMul :
Expr
IsBVNAND :
Expr
IsBVNOR :
Expr
IsBVNOT :
Expr
IsBVNumeral :
Expr
IsBVOR :
Expr
IsBVReduceAND :
Expr
IsBVReduceOR :
Expr
IsBVRepeat :
Expr
IsBVRotateLeft :
Expr
IsBVRotateLeftExtended :
Expr
IsBVRotateRight :
Expr
IsBVRotateRightExtended :
Expr
IsBVSDiv :
Expr
IsBVSGE :
Expr
IsBVSGT :
Expr
IsBVShiftLeft :
Expr
IsBVShiftRightArithmetic :
Expr
IsBVShiftRightLogical :
Expr
IsBVSignExtension :
Expr
IsBVSLE :
Expr
IsBVSLT :
Expr
IsBVSMod :
Expr
IsBVSRem :
Expr
IsBVSub :
Expr
IsBVToInt :
Expr
IsBVUDiv :
Expr
IsBVUGE :
Expr
IsBVUGT :
Expr
IsBVULE :
Expr
IsBVULT :
Expr
IsBVUMinus :
Expr
IsBVURem :
Expr
IsBVXNOR :
Expr
IsBVXOR :
Expr
IsBVXOR3 :
Expr
IsBVZeroExtension :
Expr
IsConsDecl :
ListSort
IsConst :
Expr
IsConstantArray :
Expr
IsDecidedSat :
Goal
IsDecidedUnsat :
Goal
IsDefaultArray :
Expr
IsDistinct :
Expr
IsDiv :
Expr
IsDouble :
Statistics.Entry
IsEmptyRelation :
Expr
IsEq :
Expr
IsExistential :
Quantifier
IsExpr :
AST
IsFalse :
Expr
IsFiniteDomain :
Expr
IsFiniteDomainLT :
Expr
IsFP :
Expr
IsFPAbs :
Expr
IsFPAdd :
Expr
IsFPDiv :
Expr
IsFPEq :
Expr
IsFPFMA :
Expr
IsFPFP :
Expr
IsFPGe :
Expr
IsFPGt :
Expr
IsFPisInf :
Expr
IsFPisNaN :
Expr
IsFPisNegative :
Expr
IsFPisNormal :
Expr
IsFPisPositive :
Expr
IsFPisSubnormal :
Expr
IsFPisZero :
Expr
IsFPLe :
Expr
IsFPLt :
Expr
IsFPMax :
Expr
IsFPMin :
Expr
IsFPMinusInfinity :
Expr
IsFPMinusZero :
Expr
IsFPMul :
Expr
IsFPNaN :
Expr
IsFPNeg :
Expr
IsFPNumeral :
Expr
IsFPPlusInfinity :
Expr
IsFPPlusZero :
Expr
IsFPRem :
Expr
IsFPRM :
Expr
IsFPRMExpr :
Expr
IsFPRMExprRNA :
Expr
IsFPRMExprRNE :
Expr
IsFPRMExprRTN :
Expr
IsFPRMExprRTP :
Expr
IsFPRMExprRTZ :
Expr
IsFPRMNumeral :
Expr
IsFPRMRoundNearestTiesToAway :
Expr
IsFPRMRoundNearestTiesToEven :
Expr
IsFPRMRoundTowardNegative :
Expr
IsFPRMRoundTowardPositive :
Expr
IsFPRMRoundTowardZero :
Expr
IsFPRoundToIntegral :
Expr
IsFPSqrt :
Expr
IsFPSub :
Expr
IsFPToFp :
Expr
IsFPToFpUnsigned :
Expr
IsFPToIEEEBV :
Expr
IsFPToReal :
Expr
IsFPToSBV :
Expr
IsFPToUBV :
Expr
IsFuncDecl :
AST
IsGarbage :
Goal
IsGE :
Expr
IsGT :
Expr
IsIDiv :
Expr
IsIff :
Expr
IsImplies :
Expr
IsInt :
Expr
IsInterpolant :
Expr
IsIntNum :
Expr
IsIntToBV :
Expr
IsIntToReal :
Expr
IsIsEmptyRelation :
Expr
IsITE :
Expr
IsLabel :
Expr
IsLabelLit :
Expr
IsLE :
Expr
IsLT :
Expr
IsModulus :
Expr
IsMul :
Expr
IsNilDecl :
ListSort
IsNot :
Expr
IsNumeral :
Expr
IsOEQ :
Expr
IsOr :
Expr
IsOverApproximation :
Goal
IsPrecise :
Goal
IsProofAndElimination :
Expr
IsProofApplyDef :
Expr
IsProofAsserted :
Expr
IsProofCNFStar :
Expr
IsProofCommutativity :
Expr
IsProofDefAxiom :
Expr
IsProofDefIntro :
Expr
IsProofDER :
Expr
IsProofDistributivity :
Expr
IsProofElimUnusedVars :
Expr
IsProofGoal :
Expr
IsProofHypothesis :
Expr
IsProofIFFFalse :
Expr
IsProofIFFOEQ :
Expr
IsProofIFFTrue :
Expr
IsProofLemma :
Expr
IsProofModusPonens :
Expr
IsProofModusPonensOEQ :
Expr
IsProofMonotonicity :
Expr
IsProofNNFNeg :
Expr
IsProofNNFPos :
Expr
IsProofNNFStar :
Expr
IsProofOrElimination :
Expr
IsProofPullQuant :
Expr
IsProofPullQuantStar :
Expr
IsProofPushQuant :
Expr
IsProofQuantInst :
Expr
IsProofQuantIntro :
Expr
IsProofReflexivity :
Expr
IsProofRewrite :
Expr
IsProofRewriteStar :
Expr
IsProofSkolemize :
Expr
IsProofSymmetry :
Expr
IsProofTheoryLemma :
Expr
IsProofTransitivity :
Expr
IsProofTransitivityStar :
Expr
IsProofTrue :
Expr
IsProofUnitResolution :
Expr
IsQuantifier :
AST
IsRatNum :
Expr
IsReal :
Expr
IsRealIsInt :
Expr
IsRealToInt :
Expr
IsRelation :
Expr
IsRelationalJoin :
Expr
IsRelationClone :
Expr
IsRelationComplement :
Expr
IsRelationFilter :
Expr
IsRelationNegationFilter :
Expr
IsRelationProject :
Expr
IsRelationRename :
Expr
IsRelationSelect :
Expr
IsRelationStore :
Expr
IsRelationUnion :
Expr
IsRelationWiden :
Expr
IsRemainder :
Expr
isRNA :
FPRMNum
isRNE :
FPRMNum
isRoundNearestTiesToAway :
FPRMNum
isRoundNearestTiesToEven :
FPRMNum
isRoundTowardNegative :
FPRMNum
isRoundTowardPositive :
FPRMNum
isRoundTowardZero :
FPRMNum
isRTN :
FPRMNum
isRTP :
FPRMNum
isRTZ :
FPRMNum
IsSelect :
Expr
IsSetComplement :
Expr
IsSetDifference :
Expr
IsSetIntersect :
Expr
IsSetSubset :
Expr
IsSetUnion :
Expr
IsSort :
AST
IsStore :
Expr
IsSub :
Expr
IsTrue :
Expr
IsUInt :
Statistics.Entry
IsUMinus :
Expr
IsUnderApproximation :
Goal
IsUniversal :
Quantifier
IsVar :
AST
IsWellSorted :
Expr
IsXor :
Expr
Generated on Sat Nov 12 2016 23:19:11 for Z3 by
1.8.12