Here is a list of all class members with links to the classes they belong to:

- i -

• i : CVCL::CLFlag
• id : CVCL::Context, CVCL::Clause, SatSolver::Clause, SatSolver::Lit, SatSolver::Var
• idExpr() : CVCL::VCL, CVCL::ValidityChecker
• IF_DEBUG() : CVCL::TheoryCore, CVCL::TheoryArray, CVCL::SearchEngineFast, CVCL::ExprManager, CVCL::ContextObj, CVCL::ContextObjChain, CVCL::Clause, CVCL::ClauseValue
• iffAndDistrib() : CVCL::CoreTheoremProducer, CVCL::CoreProofRules
• iffCNFRule() : CVCL::SearchEngineTheoremProducer, CVCL::SearchEngineRules
• iffContrapositive() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• iffExpr() : CVCL::VCL, CVCL::ValidityChecker, CVCL::Expr
• iffFalseElim() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• iffMP() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• iffNotFalse() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• iffOrDistrib() : CVCL::CoreTheoremProducer, CVCL::CoreProofRules
• iffToClauses() : CVCL::SearchEngineTheoremProducer, CVCL::SearchEngineRules
• IffToIte() : CVCL::CoreTheoremProducer, CVCL::CoreProofRules
• iffTrue() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• iffTrueElim() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• ifLiftRule() : CVCL::CNF_TheoremProducer, CVCL::CNF_Rules
• ifLiftUnaryRule() : CVCL::CoreTheoremProducer, CVCL::CoreProofRules
• impCNFRule() : CVCL::SearchEngineTheoremProducer, CVCL::SearchEngineRules
• impExpr() : CVCL::Expr
• Impl() : CVCL::Rational::Impl
• implContrapositive() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• IMPLIED_LITERAL : CVCL::Expr
• impliesExpr() : CVCL::VCL, CVCL::ValidityChecker
• implIntro() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• implIntro3() : CVCL::CoreTheoremProducer, CVCL::CoreProofRules, CVCL::TheoryCore
• implMP() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• importExpr() : CVCL::VCL, CVCL::ValidityChecker
• importType() : CVCL::VCL, CVCL::ValidityChecker
• ImpToIte() : CVCL::CoreTheoremProducer, CVCL::CoreProofRules
• in_new_cl() : CVariable
• in_use() : CClause
• incIndent() : CVCL::ExprManager
• incomplete() : CVCL::VCL, CVCL::ValidityChecker, CVCL::TheoryCore
• inconsistent() : CVCL::VCL, CVCL::ValidityChecker, CVCL::TheoryCore, CVCL::Theory
• INCONSISTENT : SAT::DPLLT
• inconsistentThm() : CVCL::TheoryCore
• incRefcount() : CVCL::ExprValue
• indent() : CVCL::ExprManager, CVCL::Expr
• ineq() : CVCL::TheoryArith::Ineq
• Ineq() : CVCL::TheoryArith::Ineq
• init() : CSolver, CDatabase, CClause, CVCL::Debug, CVCL::Assumptions
• init_num_clauses : CDatabase, CDatabaseStats
• init_num_literals : CDatabase, CDatabaseStats
• initializeLabels() : CVCL::TheoryDatatypeLazy, CVCL::TheoryDatatype
• initParser() : CVCL::Parser
• Insert() : CVCL::Hash_Table< _Key, _Data >, CVCL::Dict< _Key, _Data >
• insert() : CVCL::Hash_Table< _Key, _Data >, CVCL::ExprHashMap< Data >, CVCL::ExprMap< Data >, CVCL::CDMapOrdered< Key, Data >, CVCL::CDMap< Key, Data, HashFcn >
• installExprValue() : CVCL::ExprManager
• installID() : CVCL::Theory
• instantiate() : CVCL::TheoryQuant, CVCL::TheoryDatatypeLazy, CVCL::TheoryDatatype
• interactive : CVCL::ParserTemp
• interchangeIndices() : CVCL::ArrayTheoremProducer, CVCL::ArrayProofRules
• intType() : CVCL::ArithTheoremProducer, CVCL::VCL, CVCL::ValidityChecker, CVCL::TheoryArith
• intUsed() : CVCL::TheoryArith
• intVarEqnConst() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• inv() : CVCL::RefinedArithTheoremProducer
• invalidateSimpCache() : CVCL::ExprManager
• invertValue() : SAT::Var
• is : CVCL::ParserTemp
• IS_ATOMIC : CVCL::Expr
• is_conflict() : CDatabase
• IS_FINITE : CVCL::Expr
• is_ht() : CLitPoolElement
• IS_INT_ASSUMPTION : CVCL::Expr
• IS_JUSTIFIED : CVCL::Expr
• is_literal() : CLitPoolElement
• is_marked() : CVariable
• is_mem_out : CSolverStats
• is_satisfied() : CDatabase
• IS_SELECTED : CVCL::Expr
• is_solver_started : CSolverStats
• IS_TRANSLATED : CVCL::Expr
• IS_USER_ASSUMPTION : CVCL::Expr
• IS_USER_REGISTERED_ATOM : CVCL::Expr
• isAbsAtomicFormula() : CVCL::Expr
• isAbsLiteral() : CVCL::Theorem3, CVCL::Theorem, CVCL::Expr
• isActive() : CVCL::TheoremManager, CVCL::ExprManager
• isAnd() : CVCL::Expr
• isApply() : CVCL::ExprApply, CVCL::ExprValue, CVCL::Expr
• isAssump() : CVCL::TheoremValue, CVCL::Theorem3, CVCL::Theorem
• isAssumption() : CVCL::SearchSat, CVCL::SearchImplBase, CVCL::SearchEngineFast, CVCL::SearchEngine
• isAtomic() : CVCL::Expr
• isAtomicArithFormula() : CVCL::TheoryArith
• isAtomicArithTerm() : CVCL::TheoryArith
• isAtomicFormula() : CVCL::Expr
• isBetter() : CVCL::DecisionEngineMBTF, CVCL::DecisionEngineDFS, CVCL::DecisionEngineCaching, CVCL::DecisionEngine
• isBool() : CVCL::Type
• isBoolConnective() : CVCL::Expr
• isBoolConst() : CVCL::Expr
• isBoundVar() : CVCL::Expr
• isClause() : CVCL::SearchImplBase
• isClosure() : CVCL::ExprClosure, CVCL::ExprValue, CVCL::Expr
• isCNFVar() : CVCL::SearchImplBase
• IsConsistent() : CVCL::SVC_API_impl
• isConst() : CVCL::Assumptions
• isCurrent() : CVCL::ContextObj, CVCL::Scope
• isEq() : CVCL::Expr
• isEquivCheckExpr() : CVCL::TheoryCore
• isExists() : CVCL::Expr
• isFalse() : CVCL::Expr, SAT::Lit
• isFinite() : CVCL::Expr
• isFlagged() : CVCL::TheoremValue, CVCL::Theorem
• isForall() : CVCL::Expr
• isFunction() : CVCL::Type
• isGoodSplitter() : CVCL::SearchImplBase
• isIff() : CVCL::Expr
• isImpl() : CVCL::Expr
• isImpliedLiteral() : CVCL::Expr
• isInitialized() : CVCL::Expr
• isIntAssumption() : CVCL::Expr
• isIntConst() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• isInteger() : CVCL::Rational::Impl, CVCL::TheoryArith, CVCL::Rational
• isIntegerDerive() : CVCL::TheoryArith
• isIntegerThm() : CVCL::TheoryArith
• isInverted() : SAT::Lit
• isITE() : CVCL::Expr
• isJustified() : CVCL::Expr
• isKindRegistered() : CVCL::ExprManager
• isLambda() : CVCL::Expr
• isLeaf() : CVCL::Theory
• isLeafIn() : CVCL::Theory
• isLiteral() : CVCL::Expr
• isNegative() : CVCL::Literal
• isNot() : CVCL::Expr
• IsNull() : SatSolver::Clause, SatSolver::Lit, SatSolver::Var
• isNull() : CVCL::Literal, CVCL::Variable, CVCL::Type, CVCL::Theorem3, CVCL::Theorem, CVCL::SmartCDO< T >, CVCL::Proof, CVCL::Expr, SAT::Clause, SAT::Lit, SAT::Var, CVCL::Clause, CVCL::Assumptions
• isolateVariable() : CVCL::TheoryArith
• isOr() : CVCL::Expr
• isPositive() : CVCL::Literal, SAT::Lit
• isPropAtom() : CVCL::Expr
• isPropClause() : CVCL::SearchImplBase
• isPropLiteral() : CVCL::Expr
• isQuantifier() : CVCL::Expr
• isRational() : CVCL::ExprRational, CVCL::ExprValue, CVCL::Expr
• isRecord() : CVCL::TheoryRecords
• isRecordAccess() : CVCL::RecordsTheoremProducer, CVCL::TheoryRecords
• isRecordType() : CVCL::RecordsTheoremProducer, CVCL::TheoryRecords
• isRewrite() : CVCL::ReflexivityTheoremValue, CVCL::RWTheoremValue, CVCL::TheoremValue, CVCL::Theorem3, CVCL::Theorem
• isRewriteNormal() : CVCL::Expr
• isSatisfied() : SAT::Clause
• isSelected() : CVCL::Expr
• isSkolem() : CVCL::Expr
• IsStable() : CVCL::SVC_API_impl
• isStale() : CVCL::TheoryArith
• isString() : CVCL::ExprString, CVCL::ExprValue, CVCL::Expr
• isSubtype() : CVCL::Type
• isSymbol() : CVCL::ExprSymbol, CVCL::ExprValue, CVCL::Expr
• isSyntacticRational() : CVCL::TheoryArith
• isSyntacticUMinusVar() : CVCL::TheoryArith
• isTerm() : CVCL::Expr
• isTranslated() : CVCL::Expr
• isTrue() : CVCL::Expr, SAT::Lit
• isTuple() : CVCL::TheoryRecords
• isTupleAccess() : CVCL::RecordsTheoremProducer, CVCL::TheoryRecords
• isTupleType() : CVCL::TheoryRecords
• isType() : CVCL::Expr
• isTypeKind() : CVCL::ExprManager
• isUnit() : SAT::Clause
• isUnsigned() : CVCL::Rational
• isUserAssumption() : CVCL::Expr
• isUserRegisteredAtom() : CVCL::Expr
• isValidType() : CVCL::Expr
• isVar() : CVCL::ExprBoundVar, CVCL::ExprVar, CVCL::ExprSkolem, CVCL::ExprValue, CVCL::Expr, SAT::Lit
• isWellFounded() : CVCL::Expr
• isXor() : CVCL::Expr
• ite_convert() : CVCL::ExprTransform
• ite_reorder() : CVCL::ExprTransform
• ite_simplify() : CVCL::ExprTransform
• iteBVnegRule() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• iteCNFRule() : CVCL::SearchEngineTheoremProducer, CVCL::SearchEngineRules
• iteExpr() : CVCL::VCL, CVCL::ValidityChecker, CVCL::Expr
• iteExtractRule() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• iterator : CVCL::ExprHashMap< Data >::iterator, CVCL::ExprMap< Data >::iterator, CVCL::Expr::iterator, CVCL::CDMapOrdered< Key, Data >::iterator, CVCL::CDMap< Key, Data, HashFcn >::iterator, CVCL::Assumptions::iterator, CVCL::Hash_Table< _Key, _Data >, CVCL::_Hashtable_const_iterator< _Key, _Data >, CVCL::_Hashtable_iterator< _Key, _Data >
• iteToClauses() : CVCL::SearchEngineTheoremProducer, CVCL::SearchEngineRules

---