- i -

• id() : CVC3::Clause , CVC3::Context , MiniSat::Clause , MiniSat::Lit
• idExpr() : CVC3::ValidityChecker , CVC3::VCL
• iffAndDistrib() : CVC3::CoreTheoremProducer , CVC3::CoreProofRules
• iffCNFRule() : CVC3::SearchEngineRules , CVC3::SearchEngineTheoremProducer
• iffContrapositive() : CVC3::CommonProofRules , CVC3::CommonTheoremProducer
• iffExpr() : CVC3::Expr , CVC3::ValidityChecker , CVC3::VCL
• iffFalseElim() : CVC3::CommonProofRules , CVC3::CommonTheoremProducer
• iffMP() : CVC3::CommonProofRules , CVC3::Theory , CVC3::CommonTheoremProducer
• iffNotFalse() : CVC3::CommonProofRules , CVC3::CommonTheoremProducer
• iffOrDistrib() : CVC3::CoreProofRules , CVC3::CoreTheoremProducer
• iffToClauses() : CVC3::SearchEngineRules , CVC3::SearchEngineTheoremProducer
• IffToIte() : CVC3::CoreProofRules , CVC3::CoreTheoremProducer
• iffTrue() : CVC3::CommonProofRules , CVC3::CommonTheoremProducer
• iffTrueElim() : CVC3::CommonTheoremProducer , CVC3::CommonProofRules
• ifLiftRule() : CVC3::CNF_Rules , CVC3::CNF_TheoremProducer
• ifLiftUnaryRule() : CVC3::CoreProofRules , CVC3::CoreTheoremProducer
• impCNFRule() : CVC3::SearchEngineRules , CVC3::SearchEngineTheoremProducer
• impExpr() : CVC3::Expr
• implContrapositive() : CVC3::CommonProofRules , CVC3::CommonTheoremProducer
• impliesExpr() : CVC3::ValidityChecker , CVC3::VCL
• implIntro() : CVC3::CommonProofRules , CVC3::CommonTheoremProducer
• implIntro3() : CVC3::CommonProofRules , CVC3::CommonTheoremProducer
• implMP() : CVC3::CommonProofRules , CVC3::CommonTheoremProducer
• implyDiffLogicBothBounds() : CVC3::ArithProofRules , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld
• implyEqualities() : CVC3::ArithProofRules , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld
• implyNegatedInequality() : CVC3::ArithProofRules , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld
• implyNegatedInequalityDiffLogic() : CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld , CVC3::ArithProofRules , CVC3::ArithTheoremProducer
• implyWeakerInequality() : CVC3::ArithProofRules , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld
• implyWeakerInequalityDiffLogic() : CVC3::ArithProofRules , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld
• importExpr() : CVC3::ValidityChecker , CVC3::VCL
• importType() : CVC3::ValidityChecker , CVC3::VCL
• ImpToIte() : CVC3::CoreProofRules , CVC3::CoreTheoremProducer
• in_new_cl() : CVariable
• in_use() : CClause
• incIndent() : CVC3::ExprManager
• incomplete() : CVC3::TheoryCore , CVC3::ValidityChecker , CVC3::VCL
• inconsistent() : CVC3::Theory , CVC3::TheoryCore , CVC3::ValidityChecker , CVC3::VCL
• inconsistentThm() : CVC3::TheoryCore
• increase() : MiniSat::Heap< C >
• incRefcount() : CVC3::ExprValue
• inCycle() : CVC3::TheoryArithOld::DifferenceLogicGraph
• indent() : CVC3::Expr , CVC3::ExprManager , Obj
• index() : MiniSat::Lit
• Ineq() : CVC3::TheoryArith3::Ineq , CVC3::TheoryArithNew::Ineq , CVC3::TheoryArithOld::Ineq
• ineq() : CVC3::TheoryArith3::Ineq , CVC3::TheoryArithNew::Ineq , CVC3::TheoryArithOld::Ineq
• inequalityToFind() : CVC3::TheoryArithOld
• Inference() : MiniSat::Inference
• inHeap() : MiniSat::Heap< C >
• init() : Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey > , CVC3::VCL , MiniSat::vec< T > , CClause , CDatabase , CSolver , CVC3::RWTheoremValue
• init_num_clauses() : CDatabase
• init_num_literals() : CDatabase
• initialize() : LFSCObj , LFSCProofExpr , Obj
• initializeLabels() : CVC3::TheoryDatatype , CVC3::TheoryDatatypeLazy
• initParser() : CVC3::Parser
• initTimeLimit() : CVC3::TheoryCore
• inPush() : MiniSat::Solver
• inSearch() : MiniSat::Solver
• insert() : CVC3::CDMap< Key, Data, HashFcn > , CVC3::CDMapOrdered< Key, Data > , CVC3::ExprMap< Data > , CVC3::ExprHashMap< Data > , Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey > , Hash::hash_set< _Key, _HashFcn, _EqualKey > , Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey > , MiniSat::Heap< C >
• insertClause() : MiniSat::Solver
• insertLemma() : MiniSat::Solver
• inst() : CVC3::CompleteInstPreProcessor , recCompleteInster
• inst_helper() : recCompleteInster
• installExprValue() : CVC3::ExprManager
• installID() : CVC3::Theory
• instantiate() : CVC3::TheoryDatatype , CVC3::TheoryDatatypeLazy , CVC3::TheoryQuant
• insted() : CVC3::TheoryQuant
• instMacros() : CVC3::CompleteInstPreProcessor
• integerSplit() : CVC3::ArithProofRules , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld
• intEqIrrational() : CVC3::ArithProofRules , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld
• intEqualityRationalConstant() : CVC3::ArithProofRules , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld
• interchangeIndices() : CVC3::ArrayProofRules , CVC3::ArrayTheoremProducer
• intType() : CVC3::TheoryArith , CVC3::ValidityChecker , CVC3::VCL , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld
• intVarEqnConst() : CVC3::ArithProofRules , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld
• inUpdate() : CVC3::TheoryCore
• inUserAssumption() : CVC3::Expr
• invalidateSimpCache() : CVC3::ExprManager
• invertValue() : SAT::Var
• is_conflict() : CDatabase
• is_ht() : CLitPoolElement
• is_literal() : CLitPoolElement
• is_marked() : CVariable
• is_satisfied() : CDatabase
• isAbsAtomicFormula() : CVC3::Expr
• isAbsLiteral() : CVC3::Expr , CVC3::Theorem , CVC3::Theorem3
• isActive() : CVC3::ExprManager , CVC3::TheoremManager
• isAnd() : CVC3::Expr
• isApply() : CVC3::Expr , CVC3::ExprValue , CVC3::ExprApplyTmp , CVC3::ExprApply
• isAssump() : CVC3::Theorem , CVC3::Theorem3 , CVC3::TheoremValue
• isAssumption() : CVC3::SearchEngine , CVC3::SearchEngineFast , CVC3::SearchImplBase , CVC3::SearchSat
• isAtomic() : CVC3::Expr
• isAtomicArithFormula() : CVC3::TheoryArith
• isAtomicArithTerm() : CVC3::TheoryArith
• isAtomicFormula() : CVC3::Expr
• isBasic() : CVC3::TheoryArithNew
• isBasicKind() : CVC3::TheoryCore
• isBetter() : CVC3::DecisionEngine , CVC3::DecisionEngineCaching , CVC3::DecisionEngineDFS , CVC3::DecisionEngineMBTF
• isBool() : CVC3::Type
• isBoolConnective() : CVC3::Expr
• isBoolConst() : CVC3::Expr
• isBounded() : CVC3::TheoryArithOld
• isBoundVar() : CVC3::Expr
• isClause() : CVC3::SearchImplBase
• isClosure() : CVC3::Expr , CVC3::ExprValue , CVC3::ExprClosure
• isCNFVar() : CVC3::SearchImplBase
• isConflicting() : MiniSat::Solver
• isConsistent() : MiniSat::Solver
• isConstant() : CVC3::Expr
• isConstrained() : CVC3::TheoryArithOld
• isConstrainedAbove() : CVC3::TheoryArithOld
• isConstrainedBelow() : CVC3::TheoryArithOld
• isCurrent() : CVC3::Scope , CVC3::ContextObj
• isDefined() : CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo
• isEq() : CVC3::Expr
• isExists() : CVC3::Expr
• isFalse() : CVC3::Expr , SAT::Lit
• isFinite() : CVC3::Expr , CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational
• isFlagged() : CVC3::Theorem , CVC3::TheoremManager , CVC3::TheoremValue
• isForall() : CVC3::Expr
• isFormula() : LFSCObj
• isFunction() : CVC3::Type
• isGood() : CVC3::CompleteInstPreProcessor
• isGoodQuant() : CVC3::CompleteInstPreProcessor
• isGoodSplitter() : CVC3::SearchImplBase
• isIff() : CVC3::Expr
• isIgnoredRule() : LFSCConvert
• isImpl() : CVC3::Expr
• isImpliedAt() : MiniSat::Solver
• isImpliedLiteral() : CVC3::Expr
• isInitialized() : CVC3::Expr
• isIntAssumption() : CVC3::Expr
• isIntConst() : CVC3::ArithProofRules , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld
• isInteger() : CVC3::Rational , CVC3::TheoryArithNew , CVC3::TheoryArithNew::EpsRational , CVC3::TheoryArithOld , CVC3::TheoryArith3 , CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational
• isIntegerDerive() : CVC3::TheoryArith3 , CVC3::TheoryArithNew , CVC3::TheoryArithOld
• IsIntegerElim() : CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld , CVC3::ArithProofRules
• isIntegerThm() : CVC3::TheoryArith3 , CVC3::TheoryArithNew , CVC3::TheoryArithOld
• isInverted() : SAT::Lit
• isITE() : CVC3::Expr
• isJustified() : CVC3::Expr
• isKindRegistered() : CVC3::ExprManager
• isLambda() : CVC3::Expr
• isLeaf() : SAT::SatProofNode , CVC3::Theory
• isLeafIn() : CVC3::Theory
• isLinearTerm() : CVC3::TheoryBitvector
• isLiteral() : CVC3::Expr
• isLraMulC() : LFSCLraMulC , LFSCProof
• isMacro() : CVC3::CompleteInstPreProcessor
• isMultiTrig() : CVC3::Trigger
• isNeg() : CVC3::Trigger
• isNegative() : CVC3::Literal
• isNonlinearEq() : CVC3::TheoryArithOld
• isNonlinearSumTerm() : CVC3::TheoryArithOld
• isNot() : CVC3::Expr
• isNull() : CVC3::Op
• IsNull() : SatSolver::Lit
• isNull() : CVC3::Type , SAT::Clause , CVC3::Theorem3 , CVC3::Variable , SAT::Lit , SAT::Var , CVC3::Clause , CVC3::SmartCDO< T > , CVC3::Theorem , CVC3::Expr
• IsNull() : SatSolver::Clause
• isNull() : CVC3::Literal
• IsNull() : SatSolver::Var
• isNull() : CVC3::Proof
• isolate_var() : CVC3::BitvectorTheoremProducer , CVC3::BitvectorProofRules
• isolateVariable() : CVC3::TheoryArith3 , CVC3::TheoryArithNew , CVC3::TheoryArithOld
• isOr() : CVC3::Expr
• isPermSatisfied() : MiniSat::Solver
• isPos() : CVC3::Trigger
• isPositive() : SAT::Lit , CVC3::Literal
• isPowerEquality() : CVC3::TheoryArithOld
• isPowersEquality() : CVC3::TheoryArithOld
• isPropAtom() : CVC3::Expr
• isPropClause() : CVC3::SearchImplBase
• isPropLiteral() : CVC3::Expr
• isQuantifier() : CVC3::Expr
• isRational() : CVC3::ExprValue , CVC3::TheoryArithNew::EpsRational , CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational , CVC3::Expr , CVC3::ExprRational
• isRawList() : CVC3::Expr
• isReason() : MiniSat::Solver
• isRecord() : CVC3::TheoryRecords
• isRecordAccess() : CVC3::RecordsTheoremProducer , CVC3::TheoryRecords
• isRecordType() : CVC3::TheoryRecords , CVC3::RecordsTheoremProducer , CVC3::TheoryRecords , CVC3::RecordsTheoremProducer
• isRefl() : CVC3::Theorem
• isRegistered() : MiniSat::Solver
• isRegisteredAtom() : CVC3::Expr
• isRewrite() : CVC3::Theorem , CVC3::TheoremValue , CVC3::Theorem3 , CVC3::RWTheoremValue
• isRewriteNormal() : CVC3::Expr
• isSatisfied() : SAT::Clause
• isSelected() : CVC3::Expr
• isShield() : CVC3::CompleteInstPreProcessor
• isSimp() : CVC3::Trigger
• isSkolem() : CVC3::Expr
• isStale() : CVC3::TheoryArithOld , CVC3::TheoryArith3 , CVC3::TheoryArithOld , CVC3::TheoryArithNew
• isStoredPredicate() : CVC3::Expr
• isString() : CVC3::ExprString , CVC3::Expr , CVC3::ExprValue
• isSubst() : CVC3::Theorem , CVC3::TheoremValue
• isSubtype() : CVC3::Type
• isSuperSimp() : CVC3::Trigger
• isSymbol() : CVC3::ExprSymbol , CVC3::Expr , CVC3::ExprValue
• isSyntacticRational() : CVC3::TheoryArith
• isTerm() : CVC3::Expr
• isTermIn() : CVC3::TheoryBitvector
• isTheorem() : CVC3::Expr , CVC3::ExprValue
• isTrans2Like() : CVC3::TheoryQuant
• isTranslated() : CVC3::Expr
• isTransLike() : CVC3::TheoryQuant
• isTrivial() : LFSCProof
• IsTrivial() : LFSCLem
• isTrivial() : LFSCLraAxiom
• isTrivialBooleanAxiom() : LFSCConvert
• isTrivialTheoryAxiom() : LFSCConvert
• isTrue() : CVC3::Expr , SAT::Lit
• isTuple() : CVC3::TheoryRecords
• isTupleAccess() : CVC3::TheoryRecords , CVC3::RecordsTheoremProducer
• isTupleType() : CVC3::TheoryRecords
• isType() : CVC3::Expr
• isTypeKind() : CVC3::ExprManager
• isUnit() : SAT::Clause
• isUnsat() : CVC3::TheoryArithOld::DifferenceLogicGraph
• isUnsigned() : CVC3::Rational
• isUserAssumption() : CVC3::Expr
• isUserRegisteredAtom() : CVC3::Expr
• isValidType() : CVC3::Expr
• isVar() : CVC3::ExprSkolem , CVC3::ExprVar , CVC3::ExprBoundVar , SAT::Var , LFSCObj , CVC3::ExprValue , CVC3::Expr , SAT::Lit
• isWellFounded() : CVC3::Expr
• isXor() : CVC3::Expr
• ITE_generator() : CVC3::ExprTransform
• iteBVnegRule() : CVC3::BitvectorTheoremProducer , CVC3::BitvectorProofRules
• iteCNFRule() : CVC3::SearchEngineRules , CVC3::SearchEngineTheoremProducer
• iteExpr() : CVC3::VCL , CVC3::Expr , CVC3::ValidityChecker
• iteExtractRule() : CVC3::BitvectorProofRules , CVC3::BitvectorTheoremProducer
• iterator() : CVC3::Expr::iterator , CVC3::CDMap< Key, Data, HashFcn >::iterator , CVC3::Expr::iterator , CVC3::CDMap< Key, Data, HashFcn >::iterator , Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::iterator , CVC3::CDMapOrdered< Key, Data >::iterator , CVC3::ExprHashMap< Data >::iterator , CVC3::CDMapOrdered< Key, Data >::iterator , Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::iterator , CVC3::CDMap< Key, Data, HashFcn >::iterator , CVC3::ExprMap< Data >::iterator , CVC3::ExprHashMap< Data >::iterator , CVC3::CDMapOrdered< Key, Data >::iterator , Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::iterator , CVC3::Assumptions::iterator
• iterBKList() : CVC3::TheoryQuant
• iterFWList() : CVC3::TheoryQuant
• iteToClauses() : CVC3::SearchEngineTheoremProducer , CVC3::SearchEngineRules