- i -

• id() : CVC3::Clause , CVC3::Context , MiniSat::Lit , MiniSat::Clause
• idExpr() : CVC3::VCL , CVC3::ValidityChecker
• IF_DEBUG() : CVC3::Clause
• iffAndDistrib() : CVC3::CoreProofRules , CVC3::CoreTheoremProducer
• iffCNFRule() : CVC3::SearchEngineRules , CVC3::SearchEngineTheoremProducer
• iffContrapositive() : CVC3::CommonTheoremProducer , CVC3::CommonProofRules
• iffExpr() : CVC3::ValidityChecker , CVC3::VCL , CVC3::Expr
• iffFalseElim() : CVC3::CommonTheoremProducer , CVC3::CommonProofRules
• iffMP() : CVC3::CommonProofRules , CVC3::Theory , CVC3::CommonTheoremProducer
• iffNotFalse() : CVC3::CommonTheoremProducer , CVC3::CommonProofRules
• iffOrDistrib() : CVC3::CoreProofRules , CVC3::CoreTheoremProducer
• iffToClauses() : CVC3::SearchEngineRules , CVC3::SearchEngineTheoremProducer
• IffToIte() : CVC3::CoreTheoremProducer , CVC3::CoreProofRules
• iffTrue() : CVC3::CommonTheoremProducer , CVC3::CommonProofRules
• iffTrueElim() : CVC3::CommonTheoremProducer , CVC3::CommonProofRules
• ifLiftRule() : CVC3::CNF_TheoremProducer , CVC3::CNF_Rules
• 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::CommonTheoremProducer , CVC3::CommonProofRules
• 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::ArithProofRules , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld
• 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
• incIndent() : CVC3::ExprManager
• incomplete() : CVC3::ValidityChecker , CVC3::VCL , CVC3::TheoryCore
• inconsistent() : CVC3::ValidityChecker , CVC3::VCL , CVC3::Theory , CVC3::TheoryCore
• inconsistentThm() : CVC3::TheoryCore
• increase() : MiniSat::Heap< C >
• incRefcount() : CVC3::ExprValue
• inCycle() : CVC3::TheoryArithOld::DifferenceLogicGraph
• indent() : CVC3::Expr , CVC3::ExprManager
• index() : MiniSat::Lit
• Ineq() : CVC3::TheoryArith3::Ineq
• ineq() : CVC3::TheoryArith3::Ineq
• Ineq() : CVC3::TheoryArith3::Ineq , CVC3::TheoryArithNew::Ineq
• ineq() : CVC3::TheoryArithNew::Ineq
• Ineq() : CVC3::TheoryArithOld::Ineq
• 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 > , CVC3::RWTheoremValue , vec< T >
• initializeLabels() : CVC3::TheoryDatatypeLazy , CVC3::TheoryDatatype
• initParser() : CVC3::Parser
• initTimeLimit() : CVC3::TheoryCore
• inPush() : MiniSat::Solver
• inSearch() : MiniSat::Solver
• insert() : iterator , ExprMap< unsigned > , iterator , CDMap< Expr, bool > , iterator , hash_map< Expr, Theorem > , ExprHashMap< bool > , ExprMap< Polarity > , iterator , ExprMap< Polarity > , iterator , ExprMap< vector< dynTrig > , iterator , Hash::hash_set< _Key, _HashFcn, _EqualKey > , iterator , ExprMap< Expr > emptyEnv , Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey > , Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey > , CDMap< Expr, CDList< dynTrig > , iterator , ExprMap< CDList< Expr > , iterator iterOneBegin vector< pair< Expr, CDList< Expr > , ExprMap< ExprMap< vector< dynTrig > , iterator , ExprMap< set< Expr > , iterator , MiniSat::Heap< C > , hash_map< Expr, bool > , ExprMap< Expr > currentBinds , iterator , ExprMap< Expr > emptyEnv , iterator iterOneBegin vector< pair< Expr, CDList< Expr > , CDMap< Expr, Theorem > , iterator , ExprMap< Expr > currentBinds , iterator iterTwoBegin vector< pair< Expr, CDList< Expr > , iterator , ExprMap< ExprMap< vector< dynTrig > , ExprMap< Rational > , iterator , ExprMap< Expr > , CVC3::CDMapOrdered< Key, Data > , CVC3::ExprMap< Data > , iterator , ExprHashMap< bool > , iterator , ExprMap< int > , CVC3::CDMap< Key, Data, HashFcn > , CVC3::ExprMap< Data > , iterator , const_iterator , CDMap< Key, Data, HashFcn > , iterator i CDOmap< Key, Data, HashFcn > , CVC3::ExprHashMap< Data > , CDMapOrdered< Key, Data > , iterator , ExprMap< bool > , iterator , ExprHashMap< Expr > , CVC3::ExprHashMap< Data > , iterator , ExprHashMap< Theorem > , iterator , ExprMap< set< Expr > , hash_map< int, SAT::SatProofNode * > , iterator , const_iterator , iterator , ExprMap< Theorem > , iterator , iterator iterTwoBegin vector< pair< Expr, CDList< Expr > , ExprMap< CDList< Ineq > , iterator
• insertClause() : MiniSat::Solver
• insertLemma() : MiniSat::Solver
• inst() : recCompleteInster , CVC3::CompleteInstPreProcessor
• 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::VCL , CVC3::ArithTheoremProducer , CVC3::TheoryArith , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld , CVC3::ValidityChecker
• intVarEqnConst() : CVC3::ArithProofRules , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld
• inUpdate() : CVC3::TheoryCore
• inUserAssumption() : CVC3::Expr
• invalidateSimpCache() : CVC3::ExprManager
• invertValue() : SAT::Var
• isAbsAtomicFormula() : CVC3::Expr
• isAbsLiteral() : CVC3::Expr , CVC3::Theorem , CVC3::Theorem3
• isActive() : CVC3::TheoremManager , CVC3::ExprManager
• isAnd() : CVC3::Expr
• isApply() : CVC3::Expr , CVC3::ExprApplyTmp , CVC3::ExprApply , CVC3::ExprValue
• isAssump() : CVC3::Theorem , CVC3::Theorem3 , CVC3::TheoremValue
• isAssumption() : CVC3::SearchEngineFast , CVC3::SearchEngine , CVC3::SearchSat , CVC3::SearchImplBase
• 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::ExprClosure , CVC3::Expr , CVC3::ExprValue
• isCNFVar() : CVC3::SearchImplBase
• isConflicting() : MiniSat::Solver
• isConsistent() : MiniSat::Solver
• isConstant() : CVC3::Expr
• isConstrained() : CVC3::TheoryArithOld
• isConstrainedAbove() : CVC3::TheoryArithOld
• isConstrainedBelow() : CVC3::TheoryArithOld
• isCurrent() : CDMap< Key, Data, HashFcn > , CDOmapOrdered< Key, Data > , iterator , CDOmap< Expr, FreeConst > , CDList< size_t > size_t , CDList< size_t > , CVC3::ContextObj , const_iterator , CVC3::Scope , CDMapOrdered< Key, Data > , CDList< T > , CDMap< Expr, CDList< dynTrig > , CDMap< Expr, bool > , iterator , CDO< Theorem > , iterator , CDList< dynTrig > , CDList< Theorem > , CDOmap< Key, Data, HashFcn > , CDOmap< Key, Data, HashFcn > new true CDOmap< Key, Data, HashFcn > , CDOmap< Key, Data, HashFcn > new , CDOmapOrdered< Key, Data > new CDOmapOrdered< Key, Data > , CDO< T > , iterator , CDMap< Expr, Theorem > , CDList< Expr > , iterator , CDList< Ineq > , iterator
• isDefined() : CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo
• isEq() : CVC3::Expr
• isExists() : CVC3::Expr
• isFalse() : SAT::Lit , CVC3::Expr
• isFinite() : CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational , CVC3::Expr
• isFlagged() : CVC3::Theorem , CVC3::TheoremValue , CVC3::TheoremManager
• isForall() : CVC3::Expr
• isFunction() : CVC3::Type
• isGood() : CVC3::CompleteInstPreProcessor
• isGoodQuant() : CVC3::CompleteInstPreProcessor
• isGoodSplitter() : CVC3::SearchImplBase
• isIff() : CVC3::Expr
• isImpl() : CVC3::Expr
• isImpliedAt() : MiniSat::Solver
• isImpliedLiteral() : CVC3::Expr
• isInitialized() : CVC3::Expr
• isIntAssumption() : CVC3::Expr
• isIntConst() : CVC3::ArithProofRules , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld , CVC3::ArithTheoremProducer
• isInteger() : CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational , CVC3::TheoryArithOld , CVC3::TheoryArith3 , CVC3::Rational , CVC3::TheoryArithNew::EpsRational , CVC3::TheoryArithNew
• isIntegerDerive() : CVC3::TheoryArithNew , CVC3::TheoryArithOld , CVC3::TheoryArith3
• IsIntegerElim() : CVC3::ArithTheoremProducerOld , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducer , CVC3::ArithProofRules
• isIntegerThm() : CVC3::TheoryArithOld , CVC3::TheoryArith3 , CVC3::TheoryArithNew
• 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
• isMacro() : CVC3::CompleteInstPreProcessor
• isMultiTrig() : CVC3::Trigger
• isNeg() : CVC3::Trigger
• isNegative() : CVC3::Literal
• isNonlinearEq() : CVC3::TheoryArithOld
• isNonlinearSumTerm() : CVC3::TheoryArithOld
• isNot() : CVC3::Expr
• isNull() : SmartCDO< T > , CVC3::Clause , CVC3::Literal
• IsNull() : SatSolver::Var
• isNull() : CVC3::Proof , CVC3::Expr , CVC3::Theorem3 , CVC3::Variable , CVC3::Type , CVC3::Theorem
• IsNull() : SatSolver::Clause
• isNull() : SAT::Lit , SAT::Var
• IsNull() : SatSolver::Lit
• isNull() : SAT::Clause , CVC3::Op , CVC3::SmartCDO< T >
• isolate_var() : CVC3::BitvectorProofRules , CVC3::BitvectorTheoremProducer
• isolateVariable() : CVC3::TheoryArithOld , CVC3::TheoryArithNew , CVC3::TheoryArith3
• isOr() : CVC3::Expr
• isPermSatisfied() : MiniSat::Solver
• isPos() : CVC3::Trigger
• isPositive() : CVC3::Literal , SAT::Lit
• isPowerEquality() : CVC3::TheoryArithOld
• isPowersEquality() : CVC3::TheoryArithOld
• isPropAtom() : CVC3::Expr
• isPropClause() : CVC3::SearchImplBase
• isPropLiteral() : CVC3::Expr
• isQuantifier() : CVC3::Expr
• isRational() : CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational , CVC3::ExprRational , CVC3::TheoryArithNew::EpsRational , CVC3::Expr , CVC3::ExprValue
• isRawList() : CVC3::Expr
• isReason() : MiniSat::Solver
• isRecord() : CVC3::TheoryRecords
• isRecordAccess() : CVC3::RecordsTheoremProducer , CVC3::TheoryRecords
• isRecordType() : CVC3::RecordsTheoremProducer , CVC3::TheoryRecords , CVC3::RecordsTheoremProducer , CVC3::TheoryRecords
• isRefl() : CVC3::Theorem
• isRegistered() : MiniSat::Solver
• isRegisteredAtom() : CVC3::Expr
• isRewrite() : CVC3::RWTheoremValue , CVC3::TheoremValue , CVC3::Theorem , CVC3::Theorem3
• isRewriteNormal() : CVC3::Expr
• isSatisfied() : SAT::Clause
• isSelected() : CVC3::Expr
• isShield() : CVC3::CompleteInstPreProcessor
• isSimp() : CVC3::Trigger
• isSkolem() : CVC3::Expr
• isStale() : CVC3::TheoryArithOld , CVC3::TheoryArith3 , CVC3::TheoryArithNew
• isStoredPredicate() : CVC3::Expr
• isString() : CVC3::ExprValue , CVC3::ExprString , CVC3::Expr
• isSubst() : CVC3::TheoremValue , CVC3::Theorem
• isSubtype() : CVC3::Type
• isSuperSimp() : CVC3::Trigger
• isSymbol() : CVC3::Expr , CVC3::ExprSymbol , CVC3::ExprValue
• isSyntacticRational() : CVC3::TheoryArith
• isTerm() : CVC3::Expr
• isTermIn() : CVC3::TheoryBitvector
• isTheorem() : CVC3::ExprValue , CVC3::Expr
• isTrans2Like() : CVC3::TheoryQuant
• isTranslated() : CVC3::Expr
• isTransLike() : CVC3::TheoryQuant
• isTrue() : SAT::Lit , CVC3::Expr
• 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::Expr , SAT::Var , CVC3::ExprValue , SAT::Lit , CVC3::ExprBoundVar , CVC3::ExprVar , CVC3::ExprSkolem
• isWellFounded() : CVC3::Expr
• isXor() : CVC3::Expr
• ITE_generator() : CVC3::ExprTransform
• iteBVnegRule() : CVC3::BitvectorProofRules , CVC3::BitvectorTheoremProducer
• iteCNFRule() : CVC3::SearchEngineTheoremProducer , CVC3::SearchEngineRules
• iteExpr() : CVC3::Expr , CVC3::ValidityChecker , CVC3::VCL
• iteExtractRule() : CVC3::BitvectorTheoremProducer , CVC3::BitvectorProofRules
• iterator() : CVC3::CDMap< Key, Data, HashFcn >::iterator , CVC3::ExprMap< Data >::iterator , CVC3::ExprHashMap< Data >::iterator , CVC3::Assumptions::iterator , CVC3::CDMapOrdered< Key, Data >::iterator , CVC3::ExprHashMap< Data >::iterator , CVC3::Expr::iterator , CVC3::Assumptions::iterator , Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::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::Expr::iterator , CVC3::CDMapOrdered< Key, Data >::iterator
• iterBKList() : CVC3::TheoryQuant
• iterFWList() : CVC3::TheoryQuant
• iteToClauses() : CVC3::SearchEngineTheoremProducer , CVC3::SearchEngineRules

---