- i -

• id() : CVC3::Clause , CVC3::Context , MiniSat::Lit , MiniSat::Clause
• idExpr() : CVC3::ValidityChecker , CVC3::VCL
• IF_DEBUG() : CVC3::ClauseValue , CVC3::Clause
• iffAndDistrib() : CVC3::CoreProofRules , CVC3::CoreTheoremProducer
• iffCNFRule() : CVC3::SearchEngineRules , CVC3::SearchEngineTheoremProducer
• iffContrapositive() : CVC3::CommonTheoremProducer , CVC3::CommonProofRules
• iffExpr() : CVC3::VCL , CVC3::Expr , CVC3::ValidityChecker
• iffFalseElim() : CVC3::CommonTheoremProducer , CVC3::CommonProofRules
• iffMP() : CVC3::CommonProofRules , CVC3::CommonTheoremProducer , CVC3::Theory
• iffNotFalse() : CVC3::CommonTheoremProducer , CVC3::CommonProofRules
• iffOrDistrib() : CVC3::CoreProofRules , CVC3::CoreTheoremProducer
• iffToClauses() : CVC3::SearchEngineRules , CVC3::SearchEngineTheoremProducer
• IffToIte() : CVC3::CoreProofRules , CVC3::CoreTheoremProducer
• iffTrue() : CVC3::CommonTheoremProducer , CVC3::CommonProofRules
• 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::VCL , CVC3::ValidityChecker
• implIntro() : CVC3::CommonProofRules , CVC3::CommonTheoremProducer
• implIntro3() : CVC3::CommonTheoremProducer , CVC3::CommonProofRules
• implMP() : CVC3::CommonProofRules , CVC3::CommonTheoremProducer
• implyNegatedInequality() : CVC3::ArithProofRules , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducerOld
• implyWeakerInequality() : CVC3::ArithProofRules , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducerOld
• importExpr() : CVC3::ValidityChecker , CVC3::VCL
• importType() : CVC3::VCL , CVC3::ValidityChecker
• ImpToIte() : CVC3::CoreProofRules , CVC3::CoreTheoremProducer
• in_new_cl() : CVariable
• in_use() : CClause
• incIndent() : CVC3::ExprManager
• incomplete() : CVC3::VCL , CVC3::TheoryCore , CVC3::ValidityChecker
• inconsistent() : CVC3::VCL , CVC3::Theory , CVC3::TheoryCore , CVC3::ValidityChecker
• inconsistentThm() : CVC3::TheoryCore
• increase() : MiniSat::Heap< C >
• incRefcount() : CVC3::ExprValue
• indent() : CVC3::Expr , CVC3::ExprManager
• index() : MiniSat::Lit
• Ineq() : CVC3::TheoryArithNew::Ineq
• ineq() : CVC3::TheoryArithNew::Ineq
• Ineq() : CVC3::TheoryArithNew::Ineq
• ineq() : CVC3::TheoryArithNew::Ineq
• Ineq() : CVC3::TheoryArithOld::Ineq
• ineq() : CVC3::TheoryArithOld::Ineq
• Inference() : MiniSat::Inference
• inHeap() : MiniSat::Heap< C >
• init() : Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey > , MiniSat::vec< T > , CClause , CSolver , CDatabase , CVC3::Debug , CVC3::RWTheoremValue , vec< T >
• init_num_clauses() : CDatabase
• init_num_literals() : CDatabase
• initializeLabels() : CVC3::TheoryDatatype , CVC3::TheoryDatatypeLazy
• initParser() : CVC3::Parser
• inPush() : MiniSat::Solver
• inSearch() : MiniSat::Solver
• insert() : Hash::hash_set< _Key, _HashFcn, _EqualKey > , iterator , CDMap< Expr, bool > , Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey > , Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey > , MiniSat::Heap< C > , CVC3::CDMap< Key, Data, HashFcn > , iterator , ExprMap< bool > , iterator , ExprMap< Rational > , iterator , ExprMap< Expr > , iterator , ExprMap< int > , iterator , CDMap< Key, Data, HashFcn > , iterator i CDOmap< Key, Data, HashFcn > , CDMapOrdered< Key, Data > , iterator , ExprMap< bool > , iterator , ExprHashMap< Expr > , iterator , CDMap< Expr, Theorem > , iterator , const_iterator , iterator , ExprMap< Theorem > , CVC3::ExprMap< Data > , iterator , CVC3::ExprMap< Data > , iterator , CVC3::CDMapOrdered< Key, Data > , iterator , ExprMap< CDList< Ineq > , iterator , CVC3::ExprHashMap< Data > , iterator , ExprMap< unsigned > , CVC3::ExprHashMap< Data > , iterator , ExprMap< Polarity > , iterator , ExprMap< vector< dynTrig > , iterator , CDMap< Expr, CDList< dynTrig > , iterator , ExprMap< ExprMap< vector< dynTrig > , iterator
• insertClause() : MiniSat::Solver
• insertLemma() : MiniSat::Solver
• installExprValue() : CVC3::ExprManager
• installID() : CVC3::Theory
• instantiate() : CVC3::TheoryDatatype , CVC3::TheoryDatatypeLazy , CVC3::TheoryQuant
• insted() : CVC3::TheoryQuant
• integerSplit() : CVC3::ArithProofRules , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducerOld
• interchangeIndices() : CVC3::ArrayProofRules , CVC3::ArrayTheoremProducer
• intersect() : CVC3::TheoryCore
• intType() : CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducerOld , CVC3::TheoryArith , CVC3::ValidityChecker , CVC3::VCL
• intVarEqnConst() : CVC3::ArithProofRules , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducerOld
• 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::Theorem , CVC3::Theorem3 , CVC3::Expr
• isActive() : CVC3::TheoremManager , CVC3::ExprManager
• isAnd() : CVC3::Expr
• isApply() : CVC3::Expr , CVC3::ExprValue , CVC3::ExprApplyTmp , CVC3::ExprApply
• isAssump() : CVC3::Theorem , CVC3::TheoremValue , CVC3::Theorem3
• isAssumption() : CVC3::SearchEngineFast , CVC3::SearchEngine , 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::DecisionEngineDFS , CVC3::DecisionEngineCaching , CVC3::DecisionEngineMBTF
• isBool() : CVC3::Type
• isBoolConnective() : CVC3::Expr
• isBoolConst() : CVC3::Expr
• isBoundVar() : CVC3::Expr
• isClause() : CVC3::SearchImplBase
• isClosure() : CVC3::ExprClosure , CVC3::Expr , CVC3::ExprValue
• isCNFVar() : CVC3::SearchImplBase
• isConflicting() : MiniSat::Solver
• isConsistent() : MiniSat::Solver
• isCurrent() : iterator , const_iterator , CDList< Expr > , CDOmapOrdered< Key, Data > , CDOmap< Key, Data, HashFcn > , CDList< Ineq > , CVC3::ContextObj , CDOmap< Key, Data, HashFcn > new true CDOmap< Key, Data, HashFcn > , CDMap< Key, Data, HashFcn > , CDList< size_t > size_t , CDOmap< Expr, FreeConst > , CVC3::Scope , iterator , CDMap< Expr, CDList< dynTrig > , CDList< T > , CDOmap< Key, Data, HashFcn > new , CDOmapOrdered< Key, Data > , CDMapOrdered< Key, Data > , CDO< T > , CDList< Theorem > , CDOmapOrdered< Key, Data > new CDOmapOrdered< Key, Data > , iterator , CDMap< Expr, bool > , CDO< Theorem > , iterator , CDList< dynTrig > , iterator , vector< Expr > , CDMap< Expr, Theorem > , CDList< size_t >
• isEq() : CVC3::Expr
• isExists() : CVC3::Expr
• isFalse() : SAT::Lit , CVC3::Expr
• isFinite() : CVC3::Expr
• isFlagged() : CVC3::TheoremValue , CVC3::TheoremManager , CVC3::Theorem
• isForall() : CVC3::Expr
• isFunction() : CVC3::Type
• isGoodSplitter() : CVC3::SearchImplBase
• isIff() : CVC3::Expr
• isImpl() : CVC3::Expr
• isImpliedAt() : MiniSat::Solver
• isImpliedLiteral() : CVC3::Expr
• isInitialized() : CVC3::Expr
• isIntAssumption() : CVC3::Expr
• isIntConst() : CVC3::ArithTheoremProducerOld , CVC3::ArithTheoremProducer , CVC3::ArithProofRules
• isInteger() : CVC3::Rational , CVC3::TheoryArithNew::EpsRational , CVC3::TheoryArithNew , CVC3::TheoryArithNew::EpsRational , CVC3::TheoryArithOld , CVC3::TheoryArithNew
• isIntegerDerive() : CVC3::TheoryArithOld , CVC3::TheoryArithNew
• isIntegerThm() : CVC3::TheoryArithNew , CVC3::TheoryArithOld
• isInverted() : SAT::Lit
• isITE() : CVC3::Expr
• isJustified() : CVC3::Expr
• isKindRegistered() : CVC3::ExprManager
• isLambda() : CVC3::Expr
• isLeaf() : CVC3::Theory
• isLeafIn() : CVC3::Theory
• isLiteral() : CVC3::Expr
• isMultiTrig() : CVC3::Trigger
• isNeg() : CVC3::Trigger
• isNegative() : CVC3::Literal
• isNot() : CVC3::Expr
• isNull() : SAT::Lit , SmartCDO< T >
• IsNull() : SatSolver::Clause
• isNull() : SAT::Var , CVC3::Variable , CVC3::SmartCDO< T > , CVC3::Theorem , SAT::Clause , CVC3::Proof , CVC3::Type , CVC3::Clause , CVC3::Theorem3 , CVC3::Expr
• IsNull() : SatSolver::Var
• isNull() : CVC3::Literal
• IsNull() : SatSolver::Lit
• isolateVariable() : CVC3::TheoryArithNew , CVC3::TheoryArithOld
• isOr() : CVC3::Expr
• isPermSatisfied() : MiniSat::Solver
• isPos() : CVC3::Trigger
• isPositive() : SAT::Lit , CVC3::Literal
• isPropAtom() : CVC3::Expr
• isPropClause() : CVC3::SearchImplBase
• isPropLiteral() : CVC3::Expr
• isQuantifier() : CVC3::Expr
• isRational() : CVC3::Expr , CVC3::TheoryArithNew::EpsRational , CVC3::ExprValue , CVC3::ExprRational
• isReason() : MiniSat::Solver
• isRecord() : CVC3::TheoryRecords
• isRecordAccess() : CVC3::RecordsTheoremProducer , CVC3::TheoryRecords
• isRecordType() : CVC3::RecordsTheoremProducer , CVC3::TheoryRecords
• isRefl() : CVC3::Theorem
• isRegistered() : MiniSat::Solver
• isRegisteredAtom() : CVC3::Expr
• isRewrite() : CVC3::TheoremValue , CVC3::Theorem3 , CVC3::RWTheoremValue , CVC3::Theorem
• isRewriteNormal() : CVC3::Expr
• isSatisfied() : SAT::Clause
• isSelected() : CVC3::Expr
• isSimp() : CVC3::Trigger
• isSkolem() : CVC3::Expr
• isSorted() : CVC3::TheoryCore
• isStale() : CVC3::TheoryArithNew , CVC3::TheoryArithOld , CVC3::TheoryArithNew , CVC3::TheoryArithOld
• isStoredPredicate() : CVC3::Expr
• isString() : CVC3::Expr , CVC3::ExprValue , CVC3::ExprString
• isSubtype() : CVC3::Type
• isSuperSimp() : CVC3::Trigger
• isSymbol() : CVC3::ExprValue , CVC3::ExprSymbol , CVC3::Expr
• isSyntacticRational() : CVC3::TheoryArith
• isTerm() : CVC3::Expr
• isTheorem() : CVC3::ExprValue , CVC3::Expr , CVC3::ExprTheorem
• isTrans2Like() : CVC3::TheoryQuant
• isTranslated() : CVC3::Expr
• isTransLike() : CVC3::TheoryQuant
• isTrue() : CVC3::Expr , SAT::Lit
• isTuple() : CVC3::TheoryRecords
• isTupleAccess() : CVC3::RecordsTheoremProducer , CVC3::TheoryRecords
• isTupleType() : CVC3::TheoryRecords
• isType() : CVC3::Expr
• isTypeKind() : CVC3::ExprManager
• isUnit() : SAT::Clause
• isUnsigned() : CVC3::Rational
• isUserAssumption() : CVC3::Expr
• isUserRegisteredAtom() : CVC3::Expr
• isValidType() : CVC3::Expr
• isVar() : CVC3::ExprBoundVar , CVC3::ExprSkolem , CVC3::Expr , CVC3::ExprValue , CVC3::ExprVar , SAT::Lit
• isWellFounded() : CVC3::Expr
• isXor() : CVC3::Expr
• iteBVnegRule() : CVC3::BitvectorTheoremProducer , CVC3::BitvectorProofRules
• iteCNFRule() : CVC3::SearchEngineTheoremProducer , CVC3::SearchEngineRules
• iteExpr() : CVC3::ValidityChecker , CVC3::VCL , CVC3::Expr
• iteExtractRule() : CVC3::BitvectorTheoremProducer , CVC3::BitvectorProofRules
• iterator() : CVC3::CDMapOrdered< Key, Data >::iterator , CVC3::CDMap< Key, Data, HashFcn >::iterator , CVC3::Expr::iterator , CVC3::CDMapOrdered< Key, Data >::iterator , CVC3::CDMap< Key, Data, HashFcn >::iterator , CVC3::Assumptions::iterator , CVC3::CDMapOrdered< Key, Data >::iterator , Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::iterator , CVC3::ExprMap< Data >::iterator , CVC3::ExprHashMap< Data >::iterator , CVC3::Assumptions::iterator , CVC3::CDMap< Key, Data, HashFcn >::iterator , Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::iterator , CVC3::ExprMap< Data >::iterator , CVC3::ExprHashMap< Data >::iterator , Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::iterator
• iteToClauses() : CVC3::SearchEngineTheoremProducer , CVC3::SearchEngineRules

---