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

- _ -

• _cmpFunc : CVCL::Dict< _Key, _Data >
• _data : CVCL::Hash_Entry< _Key, _Data >, CVCL::Dict_Entry< _Key, _Data >
• _growFactor : CVCL::Hash_Table< _Key, _Data >
• _growThreshold : CVCL::Hash_Table< _Key, _Data >
• _hash : CVCL::Hash_Ptr< _Key, _Data >
• _hashEntry : CVCL::Hash_Ptr< _Key, _Data >
• _hashFunc : CVCL::Hash_Table< _Key, _Data >
• _Hashtable : CVCL::_Hashtable_const_iterator< _Key, _Data >, CVCL::_Hashtable_iterator< _Key, _Data >
• _Hashtable_const_iterator() : CVCL::_Hashtable_const_iterator< _Key, _Data >
• _Hashtable_const_iterator<_Key, _Data> : CVCL::Hash_Table< _Key, _Data >
• _Hashtable_iterator() : CVCL::_Hashtable_iterator< _Key, _Data >
• _Hashtable_iterator<_Key, _Data> : CVCL::Hash_Table< _Key, _Data >
• _hashTbl : CVCL::Hash_Table< _Key, _Data >
• _index : CVCL::Hash_Ptr< _Key, _Data >
• _key : CVCL::Hash_Entry< _Key, _Data >, CVCL::Dict_Entry< _Key, _Data >
• _link : CVCL::Dict_Ptr< _Key, _Data >
• _list : CVCL::Dict< _Key, _Data >
• _M_cur : CVCL::_Hashtable_const_iterator< _Key, _Data >, CVCL::_Hashtable_iterator< _Key, _Data >
• _M_ht : CVCL::_Hashtable_const_iterator< _Key, _Data >, CVCL::_Hashtable_iterator< _Key, _Data >
• _matchFunc : CVCL::Hash_Table< _Key, _Data >
• _next : CVCL::Hash_Entry< _Key, _Data >, CVCL::Dict_Entry< _Key, _Data >
• _Node : CVCL::_Hashtable_const_iterator< _Key, _Data >, CVCL::_Hashtable_iterator< _Key, _Data >
• _numEntries : CVCL::Hash_Table< _Key, _Data >, CVCL::Dict< _Key, _Data >
• _size : CVCL::Hash_Table< _Key, _Data >
• _val : CVCL::Hash_Entry< _Key, _Data >

- a -

• abs : CVCL::Rational
• add() : CVCL::NotifyList, CVCL::AssumptionsValue, CVCL::Assumptions
• addAssoc() : CVCL::RefinedArithTheoremProducer
• addBoundVar() : CVCL::Theory
• addCNFFact() : CVCL::SearchEngine
• added() : CVCL::VariableValue, CVCL::Literal, CVCL::Variable
• addEdge() : CVCL::TheoryArith::VarOrderGraph
• addEquality() : CVCL::TheoryCore
• addFact() : CVCL::TheoryCore, CVCL::Theory, CVCL::SearchEngine
• addFlag() : CVCL::CLFlags
• addInvR() : CVCL::RefinedArithTheoremProducer
• addLetHeader() : CVCL::ExprStream
• addLID() : CVCL::RefinedArithTheoremProducer
• addLiteralFact() : CVCL::SearchSimple, CVCL::SearchEngineFast, CVCL::SearchEngine
• addNewClause() : CVCL::SearchEngineFast
• addNonLiteralFact() : CVCL::SearchSimple, CVCL::SearchEngineFast, CVCL::SearchEngine
• addNotifyObj() : CVCL::Context
• addR() : CVCL::RefinedArithTheoremProducer
• addRCancel() : CVCL::RefinedArithTheoremProducer
• addRID() : CVCL::RefinedArithTheoremProducer
• addSharedTerm() : CVCL::TheoryUF, CVCL::TheoryQuant, CVCL::TheoryDatatype, CVCL::TheoryCore, CVCL::TheoryBitvector, CVCL::TheoryArray, CVCL::TheoryArith, CVCL::Theory
• addSplitter() : CVCL::TheoryCore, CVCL::Theory, CVCL::SearchEngineFast, CVCL::SearchEngine
• addSymm() : CVCL::RefinedArithTheoremProducer
• addToBuffer() : CVCL::TheoryArith
• addToChain() : CVCL::Scope
• addToCNFCache() : CVCL::SearchEngine
• addToNotify() : CVCL::Expr
• addToVarDB() : CVCL::TheoryCore
• analyzeUIPs() : CVCL::SearchEngineFast
• andCNFRule() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• andConcat() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• andConst() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• andElim() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• andExpr() : CVCL::VCL, CVCL::ValidityChecker, CVCL::Expr
• andFlatten() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• andIntro() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• andOne() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• AndToIte() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• andZero() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• appearsFirstMap : CVCL::TheoryUF::TCMapPair
• appearsSecondMap : CVCL::TheoryUF::TCMapPair
• applyCNFRules() : CVCL::SearchEngine
• applyExpr() : CVCL::TheoryUF
• applyLambda() : CVCL::UFTheoremProducer, CVCL::UFProofRules
• ArithException() : CVCL::ArithException
• arithmetic() : CVCL::RefinedArithTheoremProducer
• ArithTheoremProducer() : CVCL::ArithTheoremProducer
• arity() : CVCL::Type, CVCL::ExprNode, CVCL::ExprValue, CVCL::Expr
• ArrayTheoremProducer() : CVCL::ArrayTheoremProducer
• arrayType() : CVCL::VCL, CVCL::ValidityChecker
• assertAssumptions() : CVCL::SearchEngineFast
• assertDisequalities() : CVCL::TheoryCore
• assertEqualities() : CVCL::TheoryCore, CVCL::Theory
• assertFact() : CVCL::TheoryUF, CVCL::TheorySimulate, CVCL::TheoryRecords, CVCL::TheoryQuant, CVCL::TheoryDatatype, CVCL::TheoryCore, CVCL::TheoryBitvector, CVCL::TheoryArray, CVCL::TheoryArith, CVCL::Theory
• assertFactCore() : CVCL::TheoryCore
• assertFormula() : CVCL::VCL, CVCL::ValidityChecker, CVCL::TheoryCore
• assertTypePred() : CVCL::TheoryBitvector, CVCL::Theory
• assignValue() : CVCL::TheoryCore, CVCL::Theory
• assignVariables() : CVCL::TheoryArith
• assumpRule() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• Assumptions : CVCL::Assumptions, CVCL::AssumptionsValue, CVCL::Assumptions::iterator
• AssumptionsValue() : CVCL::AssumptionsValue
• at() : CVCL::CDList< T >
• AVHash() : CVCL::AVHash

- b -

• b : CVCL::CLFlag
• back() : CVCL::CDList< T >
• bcp() : CVCL::SearchEngineFast
• begin() : CVCL::Hash_Table< _Key, _Data >, CVCL::ExprHashMap< Data >, CVCL::ExprMap< Data >, CVCL::Expr, CVCL::CDMapOrdered< Key, Data >, CVCL::CDMap< Key, Data, HashFcn >, CVCL::CDList< T >, CVCL::Assumptions
• bitBlastDisEqn() : CVCL::TheoryBitvector
• bitBlastDisEqnRule() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• bitBlastEqn() : CVCL::TheoryBitvector
• bitBlastEqnRule() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• bitBlastTerm() : CVCL::TheoryBitvector
• bitExtractAnd() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• bitExtractBitwise() : CVCL::BitvectorTheoremProducer
• bitExtractBVMult() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• bitExtractBVPlus() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• bitExtractConcatenation() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• bitExtractConstant() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• bitExtractConstBVMult() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• bitExtractExtraction() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• bitExtractFixedLeftShift() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• bitExtractFixedRightShift() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• bitExtractNot() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• bitExtractOr() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• bitExtractRewrite() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• bitExtractToExtract() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• BitvectorException() : CVCL::BitvectorException
• bitvectorFalseRule() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• BitvectorTheoremProducer() : CVCL::BitvectorTheoremProducer
• bitvectorTrueRule() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• bitwiseConcat() : CVCL::BitvectorTheoremProducer
• bitwiseConst() : CVCL::BitvectorTheoremProducer
• bitwiseFlatten() : CVCL::BitvectorTheoremProducer
• boolExpr() : CVCL::ExprManager
• boolType() : CVCL::VCL, CVCL::ValidityChecker, CVCL::Theory
• boolVarExpr() : CVCL::Expr
• BoolVarExprValue() : CVCL::BoolVarExprValue
• bottomScope() : CVCL::Context
• boundVarElim() : CVCL::QuantTheoremProducer, CVCL::QuantProofRules
• boundVarExpr() : CVCL::VCL, CVCL::ValidityChecker
• buf : std::fdistream, std::fdostream
• buffer : std::fdinbuf
• bufSize : std::fdinbuf
• buildModel() : CVCL::TheoryCore
• BVConstExpr() : CVCL::BVConstExpr
• bvConstIneqn() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• bvConstMultAssocRule() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• bvMultAssocRule() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• bvmultBVUminus() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• bvmultConst() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• bvMultDistRule() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• bvOne() : CVCL::BitvectorTheoremProducer, CVCL::TheoryBitvector
• BVParameterExpr() : CVCL::BVParameterExpr
• bvPlusAssociativityRule() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• bvplusConst() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• BVPlusExpr() : CVCL::BVPlusExpr
• BVSize() : CVCL::TheoryBitvector
• BVTypePredExpr() : CVCL::BVTypePredExpr
• bvuminusBVConst() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• bvuminusBVMult() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• bvuminusBVPlus() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• bvuminusBVUminus() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• bvuminusToBVPlus() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• bvuminusVar() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• bvZero() : CVCL::BitvectorTheoremProducer, CVCL::TheoryBitvector

- c -

• CacheEntry() : CVCL::DecisionEngineMBTF::CacheEntry, CVCL::DecisionEngineCaching::CacheEntry
• cancelR() : CVCL::RefinedArithTheoremProducer
• canon() : CVCL::TheoryArith
• canonCombineLikeTerms() : CVCL::ArithTheoremProducer
• canonComboLikeTerms() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• canonConjunctionEquiv() : CVCL::TheoryArith
• canonDivide() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• canonDivideConst() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• canonDivideMult() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• canonDividePlus() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• canonDivideVar() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• canonFlattenSum() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• canonicalize() : CVCL::Rational::Impl
• canonInvert() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• canonInvertConst() : CVCL::ArithTheoremProducer
• canonInvertLeaf() : CVCL::ArithTheoremProducer
• canonInvertMult() : CVCL::ArithTheoremProducer
• canonInvertPow() : CVCL::ArithTheoremProducer
• canonMult() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• canonMultConstConst() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• canonMultConstMult() : CVCL::ArithTheoremProducer
• canonMultConstPlus() : CVCL::ArithTheoremProducer
• canonMultConstSum() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• canonMultConstTerm() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• canonMultLeafLeaf() : CVCL::ArithTheoremProducer
• canonMultLeafOrPowMult() : CVCL::ArithTheoremProducer
• canonMultLeafOrPowOrMultPlus() : CVCL::ArithTheoremProducer
• canonMultMtermMterm() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• canonMultOne() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• canonMultPlusPlus() : CVCL::ArithTheoremProducer
• canonMultPowLeaf() : CVCL::ArithTheoremProducer
• canonMultPowPow() : CVCL::ArithTheoremProducer
• canonMultTerm1Term2() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• canonMultTermConst() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• canonMultZero() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• canonPlus() : CVCL::RefinedArithTheoremProducer, CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• canonPowConst() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• canonPred() : CVCL::TheoryArith
• canonPredEquiv() : CVCL::TheoryArith
• canonSimplify() : CVCL::TheoryArith
• canonUMinusToDivide() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• caseSplit() : CVCL::SearchEngineTheoremProducer, CVCL::SearchEngineRules
• CDList() : CVCL::CDList< T >
• CDMap() : CVCL::CDMap< Key, Data, HashFcn >
• CDMapData() : CVCL::CDMapData
• CDMapOrdered() : CVCL::CDMapOrdered< Key, Data >
• CDMapOrderedData() : CVCL::CDMapOrderedData
• CDO() : CVCL::CDO< T >
• CDOmap() : CVCL::CDOmap< Key, Data, HashFcn >
• CDOmap<Key, Data, HashFcn> : CVCL::CDMap< Key, Data, HashFcn >
• CDOmapOrdered() : CVCL::CDOmapOrdered< Key, Data >
• CDOmapOrdered<Key, Data> : CVCL::CDMapOrdered< Key, Data >
• ceil() : CVCL::Rational, CVCL::Rational::Impl
• CharMap : CVCL::CLFlags
• checkContinue() : CVCL::VCL, CVCL::ValidityChecker
• checkSAT() : CVCL::SearchEngineFast
• checkSat() : CVCL::TheoryUF, CVCL::TheorySimulate, CVCL::TheoryRecords, CVCL::TheoryQuant, CVCL::TheoryDatatype, CVCL::TheoryCore, CVCL::TheoryBitvector, CVCL::TheoryArray, CVCL::TheoryArith, CVCL::Theory
• checkSATCore() : CVCL::TheoryCore, CVCL::Theory
• checkSoundNoSkolems() : CVCL::SearchEngineTheoremProducer
• checkUnsat() : CVCL::VCL, CVCL::ValidityChecker
• checkValid() : CVCL::SearchSimple, CVCL::SearchEngineFast, CVCL::SearchEngine
• checkValidMain() : CVCL::SearchSimple, CVCL::SearchEngineFast
• checkValidRec() : CVCL::SearchSimple
• checkValidThm() : CVCL::SearchEngine
• CInterface : CVCL::ExprValue, CVCL::Op, CVCL::Expr
• Circuit : CVCL::Circuit, CVCL::SearchEngineFast
• Clause : CVCL::Clause, CVCL::ClauseValue
• ClauseOwner : CVCL::ClauseOwner, CVCL::Clause
• ClauseValue() : CVCL::ClauseValue
• clear() : CVCL::Hash_Table< _Key, _Data >, CVCL::TheoremManager, CVCL::ExprHashMap< Data >, CVCL::ExprMap< Data >, CVCL::ExprManager, CVCL::Assumptions
• clearAllFlags() : CVCL::TheoremValue, CVCL::TheoremManager, CVCL::Theorem
• clearFacts() : CVCL::SearchEngineFast
• clearFlags() : CVCL::ExprManager, CVCL::Expr
• clearLiterals() : CVCL::SearchEngineFast
• clearRewriteNormal() : CVCL::Expr
• CLException() : CVCL::CLException
• CLFlag() : CVCL::CLFlag
• CNF() : CVCL::CNF
• cnf() : CVCL::CNF
• collectBasicVars() : CVCL::TheoryCore
• collectModelValues() : CVCL::TheoryCore
• collectShared() : CVCL::ExprStream
• collectSharedSubterms() : CVCL::TheoryBitvector
• collectVars() : CVCL::TheoryArith
• column() : CVCL::ExprStream
• combineLikeTerms() : CVCL::TheoryBitvector
• combineLikeTermsRule() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• commitFacts() : CVCL::SearchEngineFast
• CommonTheoremProducer() : CVCL::CommonTheoremProducer
• CompactClause() : CVCL::CompactClause
• compare : CVCL::Theorem, CVCL::Expr
• compareByPtr : CVCL::Theorem
• computeBaseType() : CVCL::TheoryUF, CVCL::TheoryRecords, CVCL::TheoryCore, CVCL::TheoryArray, CVCL::TheoryArith, CVCL::Theory
• computeCarry() : CVCL::BitvectorTheoremProducer
• computeHash() : CVCL::TupleIndex, CVCL::RecField, CVCL::ExprRecord, CVCL::BVTypePredExpr, CVCL::BVParameterExpr, CVCL::BVPlusExpr, CVCL::BVConstExpr, CVCL::ExprGrayShadow, CVCL::BoolVarExprValue, CVCL::NamedExprValue, CVCL::ExprClosure, CVCL::ExprApply, CVCL::ExprBoundVar, CVCL::ExprVar, CVCL::ExprRational, CVCL::ExprSkolem, CVCL::ExprString, CVCL::ExprNode, CVCL::ExprValue
• computeModel() : CVCL::TheoryUF, CVCL::TheoryRecords, CVCL::TheoryBitvector, CVCL::TheoryArray, CVCL::TheoryArith, CVCL::Theory
• computeModelBasic() : CVCL::TheoryCore, CVCL::TheoryArith, CVCL::Theory
• computeModelTerm() : CVCL::TheoryUF, CVCL::TheoryRecords, CVCL::TheoryDatatype, CVCL::TheoryBitvector, CVCL::TheoryArray, CVCL::TheoryArith, CVCL::Theory
• computeNormalFactor() : CVCL::TheoryArith
• computeTCC() : CVCL::TheoryUF, CVCL::TheorySimulate, CVCL::TheoryRecords, CVCL::TheoryQuant, CVCL::TheoryDatatype, CVCL::TheoryCore, CVCL::TheoryBitvector, CVCL::TheoryArray, CVCL::TheoryArith, CVCL::Theory
• computeType() : CVCL::TheoryUF, CVCL::TheorySimulate, CVCL::TheoryRecords, CVCL::TheoryQuant, CVCL::TheoryDatatype, CVCL::TheoryCore, CVCL::TheoryBitvector, CVCL::TheoryArray, CVCL::TheoryArith, CVCL::Theory
• computeTypePred() : CVCL::TheoryRecords, CVCL::TheoryCore, CVCL::TheoryBitvector, CVCL::TheoryArith, CVCL::Theory
• concatConst() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• concatFlatten() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• concatMergeExtract() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• confAndrAF() : CVCL::SearchEngineTheoremProducer, CVCL::SearchEngineRules
• confAndrAT() : CVCL::SearchEngineTheoremProducer, CVCL::SearchEngineRules
• confIffr() : CVCL::SearchEngineTheoremProducer, CVCL::SearchEngineRules
• confIterIfThen() : CVCL::SearchEngineTheoremProducer, CVCL::SearchEngineRules
• confIterThenElse() : CVCL::SearchEngineTheoremProducer, CVCL::SearchEngineRules
• conflictClause() : CVCL::SearchEngineTheoremProducer, CVCL::SearchEngineRules
• ConflictClauseManager : CVCL::SearchEngineFast::ConflictClauseManager, CVCL::SearchEngineFast
• conflictRule() : CVCL::SearchEngineTheoremProducer, CVCL::SearchEngineRules
• const_iterator : CVCL::Hash_Table< _Key, _Data >, CVCL::_Hashtable_const_iterator< _Key, _Data >, CVCL::_Hashtable_iterator< _Key, _Data >, CVCL::CDList< T >
• constMultToPlus() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• constPredicate() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• constRHSGrayShadow() : CVCL::ArithTheoremProducer
• Context : CVCL::Context, CVCL::ContextNotifyObj
• ContextManager() : CVCL::ContextManager
• ContextNotifyObj() : CVCL::ContextNotifyObj
• ContextObj : CVCL::ContextObj, CVCL::ContextObjChain, CVCL::Scope
• ContextObjChain : CVCL::ContextObjChain, CVCL::ContextObj, CVCL::Scope
• contradictionRule() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• convertToCNF() : CVCL::CommonTheoremProducer
• copy() : CVCL::TupleIndex, CVCL::RecField, CVCL::ExprRecord, CVCL::BVTypePredExpr, CVCL::BVParameterExpr, CVCL::BVPlusExpr, CVCL::BVConstExpr, CVCL::ExprGrayShadow, CVCL::BoolVarExprValue, CVCL::NamedExprValue, CVCL::ExprClosure, CVCL::ExprApply, CVCL::ExprCC, CVCL::ExprBoundVar, CVCL::ExprVar, CVCL::ExprRational, CVCL::ExprSkolem, CVCL::ExprString, CVCL::ExprNode, CVCL::ExprValue, CVCL::Assumptions
• Copy() : CVCL::Hash_Table< _Key, _Data >, CVCL::Dict< _Key, _Data >
• core : CVCL::RefinedArithTheoremProducer
• CoreNotifyObj : CVCL::TheoryCore::CoreNotifyObj, CVCL::TheoryCore
• count() : CVCL::Hash_Table< _Key, _Data >, CVCL::VariableValue, CVCL::Literal, CVCL::Variable, CVCL::ExprHashMap< Data >, CVCL::ExprMap< Data >, CVCL::CDMapOrdered< Key, Data >, CVCL::CDMap< Key, Data, HashFcn >
• counter() : CVCL::Statistics, CVCL::Debug
• CounterMap : CVCL::Debug
• countFlags() : CVCL::CLFlags
• countOwner() : CVCL::Clause
• countPrev() : CVCL::VariableValue, CVCL::Literal, CVCL::Variable
• create() : CVCL::ValidityChecker
• create_t() : CVCL::ArithTheoremProducer
• create_t2() : CVCL::ArithTheoremProducer
• create_t3() : CVCL::ArithTheoremProducer
• createContext() : CVCL::ContextManager
• createFlags() : CVCL::ValidityChecker
• createOp() : CVCL::VCL, CVCL::ValidityChecker
• createProofRules() : CVCL::TheoryUF, CVCL::TheorySimulate, CVCL::TheoryRecords, CVCL::TheoryQuant, CVCL::TheoryDatatype, CVCL::TheoryBitvector, CVCL::TheoryArray, CVCL::TheoryArith
• createRules() : CVCL::SearchEngine
• createType() : CVCL::VCL, CVCL::ValidityChecker
• CtxtMap : CVCL::VCCmd
• cutRule() : CVCL::SearchEngineTheoremProducer, CVCL::SearchEngineRules

- d -

• d_active : CVCL::TheoremManager
• d_added : CVCL::VariableValue
• d_ante : CVCL::VariableValue
• d_anteIdx : CVCL::VariableValue
• d_applicationsInModel : CVCL::TheoryUF, CVCL::TheoryArray
• d_applyCNFRulesCache : CVCL::SearchEngine
• d_assump : CVCL::TheoremValue, CVCL::VariableValue
• d_assumptions : CVCL::SearchEngine
• d_axiom : CVCL::TheoremValue
• d_basicModelVars : CVCL::TheoryCore
• d_beginningOfLine : CVCL::ExprStream
• d_berkminFlag : CVCL::SearchEngineFast
• d_bestByExpr : CVCL::DecisionEngine
• d_bitvecCache : CVCL::TheoryBitvector
• d_body : CVCL::ExprClosure
• d_bool : CVCL::ExprManager
• d_booleanRWFlag : CVCL::TheoryBitvector
• d_boolExtractCache : CVCL::TheoryBitvector
• d_boolExtractCacheFlag : CVCL::TheoryBitvector
• d_bottomLevel : CVCL::DecisionEngineMBTF, CVCL::DecisionEngineCaching
• d_bottomScope : CVCL::SearchEngine, CVCL::Context
• d_boundVarStack : CVCL::TheoryCore
• d_buffer : CVCL::TheoryArith
• d_bufferIdx : CVCL::TheoryArith
• d_bufferThres : CVCL::TheoryArith
• d_bvAssertDiseq : CVCL::TheoryBitvector
• d_bvAssertEq : CVCL::TheoryBitvector
• d_bvBitBlastDiseq : CVCL::TheoryBitvector
• d_bvBitBlastEq : CVCL::TheoryBitvector
• d_bvconst : CVCL::BVConstExpr
• d_bvConstExprIndex : CVCL::TheoryBitvector
• d_bvDelayDiseq : CVCL::TheoryBitvector
• d_bvDelayEq : CVCL::TheoryBitvector
• d_bvDelayTypePreds : CVCL::TheoryBitvector
• d_bvOne : CVCL::BitvectorTheoremProducer, CVCL::TheoryBitvector
• d_bvParameterExprIndex : CVCL::TheoryBitvector
• d_bvPlusExprIndex : CVCL::TheoryBitvector
• d_bvplusRewriteFlag : CVCL::TheoryBitvector
• d_bvTypePredExprIndex : CVCL::TheoryBitvector
• d_bvTypePreds : CVCL::TheoryBitvector
• d_bvZero : CVCL::BitvectorTheoremProducer, CVCL::TheoryBitvector
• d_c1 : CVCL::ExprGrayShadow
• d_c2 : CVCL::ExprGrayShadow
• d_cache : CVCL::DecisionEngineMBTF, CVCL::DecisionEngineCaching, CVCL::TheoryArith::VarOrderGraph
• d_cachedValue : CVCL::TheoremValue
• d_cdmap : CVCL::CDOmapOrdered< Key, Data >, CVCL::CDOmap< Key, Data, HashFcn >
• d_cdo : CVCL::SmartCDO< T >::RefCDO< U >
• d_checkProofs : CVCL::TheoremProducer
• d_children : CVCL::ExprNode
• d_chunkList : CVCL::MemoryManagerChunks
• d_chunkSize : CVCL::MemoryManagerChunks
• d_chunkSizeBytes : CVCL::MemoryManagerChunks
• d_circuitPropCount : CVCL::SearchEngineFast
• d_circuits : CVCL::SearchEngineFast
• d_circuitsByExpr : CVCL::SearchEngineFast
• d_clause : CVCL::CompactClause, CVCL::ClauseOwner, CVCL::Clause
• d_clauselit : CVCL::TheoremValue
• d_clauses : CVCL::SearchEngineFast
• d_clausesQueryEnd : CVCL::SearchEngineFast
• d_clausesQueryStart : CVCL::SearchEngineFast
• d_clean_time : CVCL::DebugTimer
• d_cm : CVCL::VCL, CVCL::VariableManager, CVCL::ExprManager, CVCL::Context
• d_cnf : CVCL::BitvectorTheoremProducer
• d_cnfBitBlastFlag : CVCL::TheoryBitvector
• d_cnfCache : CVCL::SearchEngine
• d_cnfOption : CVCL::TheoryCore, CVCL::SearchEngine
• d_cnfVars : CVCL::SearchEngine
• d_col : CVCL::ExprStream
• d_commonRules : CVCL::Theory
• d_compute_trans_closure : CVCL::TheoryUF
• d_concatRewriteFlag : CVCL::TheoryBitvector
• d_conflictClauseCount : CVCL::SearchEngineFast
• d_conflictClauseManager : CVCL::SearchEngineFast
• d_conflictClauses : CVCL::SearchEngineFast
• d_conflictClauseStack : CVCL::SearchEngineFast
• d_conflictCount : CVCL::SearchEngineFast
• d_conflictTheorem : CVCL::SearchEngineFast
• d_const : CVCL::TheoryArith::Ineq, CVCL::AssumptionsValue
• d_context : CVCL::ContextNotifyObj, CVCL::Scope, CVCL::CDMapOrdered< Key, Data >, CVCL::CDMap< Key, Data, HashFcn >
• d_contextCache : CVCL::TheoryQuant
• d_contextMap : CVCL::TheoryQuant
• d_contexts : CVCL::ContextManager
• d_contextTerms : CVCL::TheoryQuant
• d_core : CVCL::PrettyPrinterCore, CVCL::CommonTheoremProducer, CVCL::ArrayTheoremProducer, CVCL::DecisionEngine, CVCL::CNF, CVCL::SearchEngine
• d_count : CVCL::VariableValue
• d_counter : CVCL::StatCounter, CVCL::DebugCounter
• d_counters : CVCL::Statistics, CVCL::Debug
• d_countLeft : CVCL::TheoryArith
• d_countPrev : CVCL::VariableValue
• d_countRight : CVCL::TheoryArith
• d_curContext : CVCL::ContextManager
• d_currDepth : CVCL::ExprStream
• d_current : CVCL::ExprStream
• d_dag : CVCL::ExprStream
• d_dagBuilt : CVCL::ExprStream
• d_dagMap : CVCL::ExprStream
• d_dagPrinting : CVCL::ExprManager
• d_dagPtr : CVCL::ExprStream
• d_dagStack : CVCL::ExprStream
• d_data : CVCL::SmartCDO< T >, CVCL::Parser, CVCL::ContextObjChain, CVCL::CLFlag, CVCL::CDO< T >, CVCL::CDOmapOrdered< Key, Data >, CVCL::CDOmap< Key, Data, HashFcn >
• d_dataSize : CVCL::MemoryManagerChunks
• d_decisionEngine : CVCL::SearchSimple, CVCL::SearchEngineFast
• d_delay : CVCL::SmartCDO< T >::RefCDO< U >
• d_delayDelete : CVCL::Scope
• d_deleted : CVCL::VariableManager, CVCL::Scope, CVCL::ClauseValue
• d_denom : CVCL::Rational::Impl
• d_depth : CVCL::ExprStream
• d_dir : CVCL::ClauseValue
• d_disableGC : CVCL::VariableManager, CVCL::ExprManager
• d_diseq : CVCL::TheoryCore, CVCL::TheoryBitvector, CVCL::TheoryArith
• d_diseqIdx : CVCL::TheoryBitvector, CVCL::TheoryArith
• d_dpSplitters : CVCL::SearchEngine
• d_e : CVCL::ExprGrayShadow, CVCL::Expr::iterator::Proxy
• d_edges : CVCL::TheoryArith::VarOrderGraph
• d_elist : CVCL::NotifyList
• d_em : CVCL::UFTheoremProducer, CVCL::RecordsTheoremProducer, CVCL::QuantTheoremProducer, CVCL::DatatypeTheoremProducer, CVCL::BitvectorTheoremProducer, CVCL::ArrayTheoremProducer, CVCL::RefinedArithTheoremProducer, CVCL::VCL, CVCL::TheoryCore, CVCL::TheoremProducer, CVCL::TheoremManager, CVCL::ExprValue, CVCL::ExprStream, CVCL::ExprManagerNotifyObj, CVCL::ExprManager::HashEV
• d_emptyVec : CVCL::ExprManager
• d_endChunk : CVCL::MemoryManagerChunks
• d_enqueueCNFCache : CVCL::SearchEngine
• d_eq : CVCL::TheoryBitvector
• d_eqBlastIdx : CVCL::TheoryBitvector
• d_eqIdx : CVCL::TheoryBitvector
• d_equalityQueue : CVCL::TheoryCore
• d_expand : CVCL::TheoremValue
• d_expr : CVCL::BVTypePredExpr, CVCL::ReflexivityTheoremValue, CVCL::DecisionEngineMBTF::CacheEntry, CVCL::DecisionEngineCaching::CacheEntry, CVCL::VariableValue, CVCL::Type, CVCL::Op, CVCL::Expr
• d_exprGenericMap : CVCL::ExprManager
• d_exprRecFieldIdx : CVCL::TheoryRecords
• d_exprRecordIdx : CVCL::TheoryRecords
• d_exprSet : CVCL::ExprManager
• d_exprTupleIdx : CVCL::TheoryRecords
• d_exprVars : CVCL::CNF
• d_factQueue : CVCL::SearchEngineFast
• d_false : CVCL::ExprManager
• d_field : CVCL::RecField
• d_fields : CVCL::ExprRecord
• d_find : CVCL::ExprValue
• d_first : CVCL::CDMapOrdered< Key, Data >, CVCL::CDMap< Key, Data, HashFcn >
• d_flag : CVCL::TheoremValue, CVCL::TheoremManager, CVCL::StatFlag, CVCL::ExprValue, CVCL::DebugFlag, CVCL::ScopeWatcher
• d_flagCounter : CVCL::ExprManager
• d_flags : CVCL::VCL, CVCL::Statistics, CVCL::Debug
• d_freeConstDB : CVCL::TheoryArith
• d_freeList : CVCL::MemoryManagerChunks
• d_fun : CVCL::ExprApply
• d_funApplications : CVCL::TheoryUF
• d_funApplicationsIdx : CVCL::TheoryUF
• d_globals : CVCL::TheoryCore
• d_goal : CVCL::SearchSimple
• d_graph : CVCL::TheoryArith
• d_grayShadowMMIndex : CVCL::TheoryArith
• d_hash : CVCL::ExprValue
• d_height : CVCL::DecisionEngineMBTF, CVCL::DecisionEngineCaching, CVCL::ExprValue
• d_help : CVCL::CLFlag
• d_highestKid : CVCL::ExprValue
• d_hole : CVCL::TheoremProducer
• d_id : CVCL::Context
• d_idCounter : CVCL::ExprStream
• d_idx : CVCL::TupleIndex, CVCL::VCL::UserAssertion, CVCL::ExprSkolem
• d_ifLiftOption : CVCL::SearchEngine
• d_ignoreCnfVarsOption : CVCL::SearchEngine
• d_inCheckSAT : CVCL::SearchEngineFast
• d_incomplete : CVCL::TheoryCore
• d_inconsistent : CVCL::TheoryCore
• d_incThm : CVCL::TheoryCore
• d_indent : CVCL::ExprStream, CVCL::ExprManager
• d_indentLast : CVCL::ExprStream
• d_indentReg : CVCL::ExprStream
• d_indentStack : CVCL::ExprStream
• d_indentTransient : CVCL::ExprManager
• d_index : CVCL::DecisionEngineMBTF, CVCL::DecisionEngineCaching, CVCL::ExprValue, CVCL::ExprManager
• d_ineq : CVCL::TheoryArith::Ineq
• d_inequalitiesLeftDB : CVCL::TheoryArith
• d_inequalitiesRightDB : CVCL::TheoryArith
• d_inMap : CVCL::CDOmapOrdered< Key, Data >, CVCL::CDOmap< Key, Data, HashFcn >
• d_inModelCreation : CVCL::TheoryArith
• d_inputLang : CVCL::ExprManager
• d_instCount : CVCL::TheoryQuant
• d_insts : CVCL::TheoryQuant
• d_intConstUsed : CVCL::TheoryArith
• d_intType : CVCL::TheoryArith
• d_intUsed : CVCL::TheoryArith
• d_isLit : CVCL::TheoremValue
• d_it : CVCL::ExprHashMap< Data >::iterator, CVCL::ExprMap< Data >::iterator, CVCL::Expr::iterator, CVCL::CDMapOrdered< Key, Data >::orderedIterator, CVCL::CDMapOrdered< Key, Data >::iterator, CVCL::CDMap< Key, Data, HashFcn >::orderedIterator, CVCL::CDMap< Key, Data, HashFcn >::iterator, CVCL::Assumptions::iterator
• d_key : CVCL::CDOmapOrdered< Key, Data >, CVCL::CDOmap< Key, Data, HashFcn >
• d_kind : CVCL::ExprValue
• d_kindMap : CVCL::ExprManager
• d_kindMapByName : CVCL::ExprManager
• d_lang : CVCL::ExprStream
• d_langUsed : CVCL::TheoryArith
• d_lastClosure : CVCL::VCL
• d_lastConflictClause : CVCL::SearchEngineFast
• d_lastConflictScope : CVCL::SearchEngineFast
• d_lastCounterExample : CVCL::SearchEngine
• d_lastDagSize : CVCL::ExprStream
• d_lastQuery : CVCL::VCL
• d_lastQueryTCC : CVCL::VCL
• d_lastValid : CVCL::SearchEngine
• d_level : CVCL::Scope
• d_lhs : CVCL::RWTheoremValue
• d_lhsMinusRhsFlag : CVCL::TheoryBitvector
• d_lineWidth : CVCL::ExprStream, CVCL::ExprManager
• d_list : CVCL::CDList< T >
• d_lit : CVCL::SearchEngine::Splitter
• d_literals : CVCL::SearchEngineFast, CVCL::SearchEngine, CVCL::ClauseValue
• d_literalSet : CVCL::SearchEngineFast
• d_lits : CVCL::Circuit
• d_litsAlive : CVCL::SearchEngineFast
• d_litsByScores : CVCL::SearchEngineFast
• d_litsMaxScorePos : CVCL::SearchEngineFast
• d_litSortCount : CVCL::SearchEngineFast
• d_map : CVCL::VCCmd, CVCL::ExprHashMap< Data >, CVCL::ExprMap< Data >, CVCL::CLFlags, CVCL::CDMapOrdered< Key, Data >, CVCL::CDMap< Key, Data, HashFcn >
• d_master : CVCL::ContextObjChain
• d_maxQuantInst : CVCL::TheoryQuant
• d_mm : CVCL::VariableManager, CVCL::TheoremManager, CVCL::ExprManager
• d_mmFlag : CVCL::ExprManager
• d_mmIdx : CVCL::TupleIndex, CVCL::RecField, CVCL::ExprRecord, CVCL::ExprGrayShadow
• d_MMIndex : CVCL::BVTypePredExpr, CVCL::BVParameterExpr, CVCL::BVPlusExpr, CVCL::BVConstExpr
• d_modified : CVCL::CLFlag
• d_msg : CVCL::Exception
• d_n : CVCL::Rational, CVCL::Rational::Impl
• d_name : CVCL::Theory, CVCL::NamedExprValue, CVCL::ExprBoundVar, CVCL::ExprVar, CVCL::Context
• d_name_of_cur_ctxt : CVCL::VCCmd
• d_neg : CVCL::VariableValue
• d_negAdded : CVCL::VariableValue
• d_negative : CVCL::Literal
• d_negCount : CVCL::VariableValue
• d_negCountPrev : CVCL::VariableValue
• d_negScore : CVCL::VariableValue
• d_negwp : CVCL::VariableValue
• d_newDagMap : CVCL::ExprStream
• d_next : CVCL::CDOmapOrdered< Key, Data >, CVCL::CDOmap< Key, Data, HashFcn >
• d_nextFree : CVCL::MemoryManagerChunks
• d_nextNum : CVCL::CNF
• d_nodag : CVCL::ExprStream
• d_nonLiterals : CVCL::SearchSimple, CVCL::SearchEngineFast
• d_nonLiteralsSaved : CVCL::SearchEngineFast
• d_nonlitQueryEnd : CVCL::SearchEngineFast
• d_nonlitQueryStart : CVCL::SearchEngineFast
• d_notifyList : CVCL::ExprValue
• d_notifyObj : CVCL::VariableManager, CVCL::TheoryCore, CVCL::SmartCDO< T >::RefCDO< U >, CVCL::SearchEngine, CVCL::ExprManager
• d_notifyObjList : CVCL::Context
• d_nullExpr : CVCL::ExprManager
• d_num : CVCL::Rational::Impl
• d_numOfBits : CVCL::BVPlusExpr
• d_op : CVCL::BoolVarExprValue
• d_origFormulaOption : CVCL::SearchEngine
• d_os : CVCL::Statistics, CVCL::ExprStream, CVCL::Debug
• d_osdump : CVCL::VCL
• d_osDumpTrace : CVCL::Debug
• d_osdumpTranslate : CVCL::VCL
• d_outputLang : CVCL::ExprManager
• d_pair : CVCL::ExprHashMap< Data >::iterator::Proxy, CVCL::ExprMap< Data >::iterator::Proxy, CVCL::CDMapOrdered< Key, Data >::orderedIterator::Proxy, CVCL::CDMapOrdered< Key, Data >::iterator::Proxy, CVCL::CDMap< Key, Data, HashFcn >::orderedIterator::Proxy, CVCL::CDMap< Key, Data, HashFcn >::iterator::Proxy
• d_param1 : CVCL::BVParameterExpr
• d_param2 : CVCL::BVParameterExpr
• d_parent : CVCL::ExprStream
• d_parser : CVCL::VCCmd
• d_pfOp : CVCL::TheoremProducer
• d_pointerHash : CVCL::ExprManager
• d_postponed : CVCL::ExprManager
• d_postponeGC : CVCL::VariableManager, CVCL::ExprManager
• d_prettyPrinter : CVCL::ExprManager
• d_prev : CVCL::CDOmapOrdered< Key, Data >, CVCL::CDOmap< Key, Data, HashFcn >
• d_prevScope : CVCL::Scope
• d_printDepth : CVCL::ExprManager
• d_printer : CVCL::TheoryCore
• d_proof : CVCL::TheoremValue, CVCL::Proof
• d_pushNegCache : CVCL::TheoryCore
• d_q : CVCL::CNF
• d_quant : CVCL::ExprSkolem
• d_query_axioms : CVCL::SearchEngine
• d_queue : CVCL::TheoryCore
• d_queueSE : CVCL::TheoryCore
• d_r : CVCL::TheoryArith::FreeConst, CVCL::ExprRational
• d_rank : CVCL::DecisionEngineMBTF::CacheEntry, CVCL::DecisionEngineCaching::CacheEntry
• d_reads : CVCL::TheoryArray
• d_realType : CVCL::TheoryArith
• d_realUsed : CVCL::TheoryArith
• d_rebuildCache : CVCL::ExprManager
• d_ref : CVCL::SmartCDO< T >::RefCDO< U >::RefNotifyObj
• d_refCount : CVCL::SmartCDO< T >::RefCDO< U >
• d_refcount : CVCL::TheoremValue, CVCL::VariableValue, CVCL::ExprValue, CVCL::ClauseValue, CVCL::AssumptionsValue
• d_refcountOwner : CVCL::ClauseValue
• d_reflmm : CVCL::TheoremManager
• d_renameThms : CVCL::TheoryArray
• d_rep : CVCL::ExprCC
• d_replaceITECache : CVCL::SearchEngine
• d_resourceLimit : CVCL::TheoryCore
• d_restore : CVCL::ContextObj, CVCL::ContextObjChain
• d_restoreChain : CVCL::Scope
• d_restoreChainNext : CVCL::ContextObjChain
• d_restoreChainPrev : CVCL::ContextObjChain
• d_restorePoints : CVCL::SearchEngineFast::ConflictClauseManager
• d_rewriteFlag : CVCL::TheoryBitvector
• d_rhs : CVCL::RWTheoremValue, CVCL::TheoryArith::Ineq
• d_rules : CVCL::VariableManager, CVCL::TheoryUF, CVCL::TheorySimulate, CVCL::TheoryRecords, CVCL::TheoryQuant, CVCL::TheoryDatatype, CVCL::TheoryBitvector, CVCL::TheoryArray, CVCL::TheoryArith, CVCL::SearchEngine
• d_rwBitBlastFlag : CVCL::TheoryBitvector
• d_rwmm : CVCL::TheoremManager
• d_sat : CVCL::ClauseValue
• d_savedCache : CVCL::TheoryQuant
• d_savedMap : CVCL::TheoryQuant
• d_savedTerms : CVCL::TheoryQuant
• d_savedTermsPos : CVCL::TheoryQuant
• d_scope : CVCL::VariableValue, CVCL::ContextObj, CVCL::ClauseValue
• d_scopeLevel : CVCL::TheoremValue
• d_scopeStack : CVCL::VCL
• d_score : CVCL::VariableValue
• d_se : CVCL::DecisionEngine, CVCL::VCL, CVCL::SearchEngineFast::ConflictClauseManager, CVCL::SearchEngine::SearchNotifyObj
• d_setupFlag : CVCL::TheoryBitvector
• d_setupSharedFlag : CVCL::TheoryBitvector
• d_sharedSubterms : CVCL::TheoryBitvector
• d_sharedTerms : CVCL::TheoryCore, CVCL::TheoryArith
• d_sharedVars : CVCL::TheoryArith
• d_sig : CVCL::ExprCC
• d_simpCache : CVCL::ExprValue
• d_simpCacheTag : CVCL::ExprValue
• d_simpCacheTagCurrent : CVCL::ExprManager
• d_simpFrom : CVCL::ExprValue
• d_simplifiedModelVars : CVCL::TheoryCore
• d_simplifiedThm : CVCL::SearchSimple, CVCL::SearchEngineFast
• d_simplifyFlag : CVCL::TheoryBitvector
• d_simplifyInPlace : CVCL::TheoryCore
• d_size : CVCL::CDList< T >
• d_skolemized_thms : CVCL::SearchEngine
• d_skolemVars : CVCL::SearchEngine
• d_solver : CVCL::TheoryCore
• d_splitterCount : CVCL::DecisionEngine, CVCL::SearchEngineFast
• d_splitters : CVCL::DecisionEngine
• d_staleDB : CVCL::TheoryBitvector
• d_startLevel : CVCL::DecisionEngineMBTF, CVCL::DecisionEngineCaching
• d_staticFlags : CVCL::ExprValue
• d_statistics : CVCL::VCL
• d_str : CVCL::ExprString
• d_strict : CVCL::TheoryArith::FreeConst
• d_subtypePred : CVCL::ExprValue
• d_t : CVCL::Assumptions::iterator::Proxy
• d_tcc : CVCL::VCL::UserAssertion, CVCL::ExprValue
• d_tccFlag : CVCL::Theory
• d_tccs : CVCL::TheoryBitvector
• d_tccsIdx : CVCL::TheoryBitvector
• d_terms : CVCL::TheoryCore
• d_theories : CVCL::VCL, CVCL::TheoryCore
• d_theoryArith : CVCL::ArithTheoremProducer, CVCL::VCL
• d_theoryArray : CVCL::VCL
• d_theoryBitvector : CVCL::BitvectorTheoremProducer, CVCL::VCL
• d_theoryCore : CVCL::VCL, CVCL::TheoryCore::CoreNotifyObj, CVCL::Theory
• d_theoryDatatype : CVCL::DatatypeTheoremProducer, CVCL::VCL
• d_theoryMap : CVCL::TheoryCore
• d_theoryQuant : CVCL::VCL
• d_theoryRecords : CVCL::RecordsTheoremProducer, CVCL::VCL
• d_theorySimulate : CVCL::VCL
• d_theoryUF : CVCL::UFTheoremProducer, CVCL::VCL
• d_theoryUsed : CVCL::Theory
• d_thisType : CVCL::TheoryDatatype
• d_thm : CVCL::TheoremValue, CVCL::VCL::UserAssertion, CVCL::VariableValue, CVCL::Theorem3, CVCL::Theorem, CVCL::ClauseValue, CVCL::Circuit
• d_time : CVCL::DebugTimer
• d_timers : CVCL::Debug
• d_tlist : CVCL::NotifyList
• d_tm : CVCL::TheoremValue, CVCL::VCL, CVCL::TheoremProducer
• d_tmpFile : CVCL::VCL
• d_topLevel : CVCL::DecisionEngineMBTF, CVCL::DecisionEngineCaching
• d_topLevelLock : CVCL::DecisionEngineMBTF, CVCL::DecisionEngineCaching
• d_topScope : CVCL::Context
• d_tp : CVCL::CLFlag
• d_traceFlags : CVCL::Debug
• d_traceOptions : CVCL::Debug
• d_trackLiterals : CVCL::SearchEngine
• d_transClosureMap : CVCL::TheoryUF
• d_translate : CVCL::VCL
• d_trash : CVCL::CDMapOrdered< Key, Data >, CVCL::CDMap< Key, Data, HashFcn >
• d_true : CVCL::ExprManager
• d_trust : CVCL::DecisionEngineMBTF::CacheEntry, CVCL::DecisionEngineCaching::CacheEntry
• d_tv : CVCL::DebugTime
• d_type : CVCL::BVTypePredExpr, CVCL::ExprValue
• d_typeKinds : CVCL::ExprManager
• d_uid : CVCL::ParserTemp, CVCL::ExprBoundVar
• d_unitConflictClauses : CVCL::SearchEngineFast
• d_unitPropCount : CVCL::SearchEngineFast
• d_univs : CVCL::TheoryQuant
• d_univsContextPos : CVCL::TheoryQuant
• d_univsSavedPos : CVCL::TheoryQuant
• d_unreportedLits : CVCL::SearchEngineFast
• d_unreportedLitsHandled : CVCL::SearchEngineFast
• d_updateFlag : CVCL::TheoryBitvector
• d_useEnqueueFact : CVCL::SearchEngineFast
• d_userAssertions : CVCL::VCL
• d_v : CVCL::ExprGrayShadow
• d_val : CVCL::VariableValue, CVCL::Variable, CVCL::Assumptions
• d_var : CVCL::Literal
• d_varAssignments : CVCL::TheoryCore
• d_varModelMap : CVCL::TheoryCore
• d_vars : CVCL::VCL, CVCL::TheoryCore, CVCL::ExprClosure
• d_varSet : CVCL::VariableManager
• d_vc : CVCL::VCCmd
• d_vcl : CVCL::RecordsTheoremProducer, CVCL::QuantTheoremProducer, CVCL::DecisionEngine, CVCL::CNF, CVCL::TheoryUF, CVCL::TheoryRecords, CVCL::TheoryQuant, CVCL::TheoryDatatype, CVCL::TheoryCore, CVCL::TheoryBitvector, CVCL::TheoryArray, CVCL::TheoryArith, CVCL::TheoremManager, CVCL::SearchEngine, CVCL::Debug
• d_vector : CVCL::AssumptionsValue
• d_visited : CVCL::DecisionEngine
• d_vm : CVCL::VariableManagerNotifyObj, CVCL::VariableValue, CVCL::SearchEngine
• d_withAssump : CVCL::TheoremManager
• d_withIndentation : CVCL::ExprManager
• d_withProof : CVCL::TheoremManager
• d_wp : CVCL::VariableValue, CVCL::ClauseValue
• dagFlag() : CVCL::ExprStream
• dagPrinting() : CVCL::ExprManager
• darkGrayShadow2ab() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• darkGrayShadow2ba() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• darkShadow() : CVCL::ArithTheoremProducer, CVCL::TheoryArith
• Data() : CVCL::Hash_Entry< _Key, _Data >, CVCL::Dict_Entry< _Key, _Data >
• dataType() : CVCL::VCL, CVCL::ValidityChecker, CVCL::TheoryDatatype
• datatypeConsExpr() : CVCL::VCL, CVCL::ValidityChecker, CVCL::TheoryDatatype
• datatypeSelExpr() : CVCL::VCL, CVCL::ValidityChecker, CVCL::TheoryDatatype
• DatatypeTheoremProducer() : CVCL::DatatypeTheoremProducer
• Debug : CVCL::Debug, CVCL::DebugTimer
• DebugCounter() : CVCL::DebugCounter
• DebugException() : CVCL::DebugException
• DebugFlag() : CVCL::DebugFlag
• DebugTime() : CVCL::DebugTime
• DebugTimer : CVCL::DebugTimer, CVCL::DebugTime
• DecisionEngine : CVCL::DecisionEngine, CVCL::SearchEngine
• DecisionEngineCaching() : CVCL::DecisionEngineCaching
• DecisionEngineDFS() : CVCL::DecisionEngineDFS
• DecisionEngineMBTF() : CVCL::DecisionEngineMBTF
• decRefcount() : CVCL::ExprValue
• Delete() : CVCL::Hash_Table< _Key, _Data >, CVCL::Dict< _Key, _Data >
• deleted() : CVCL::Clause
• deleteData() : CVCL::MemoryManagerMalloc, CVCL::MemoryManagerChunks, CVCL::MemoryManager
• deleteNotifyObj() : CVCL::Context
• deleteParser() : CVCL::Parser
• depth() : CVCL::ExprStream
• deriveClosure() : CVCL::VCL
• deriveTheorem() : CVCL::Literal, CVCL::Variable
• deriveThmRec() : CVCL::Variable
• Destroy() : CVCL::Hash_Table< _Key, _Data >, CVCL::Dict< _Key, _Data >
• dfs() : CVCL::TheoryArith::VarOrderGraph
• Dict() : CVCL::Dict< _Key, _Data >
• Dict<_Key, _Data> : CVCL::Dict_Entry< _Key, _Data >
• Dict_Ptr() : CVCL::Dict_Ptr< _Key, _Data >
• Dict_Ptr<_Key, _Data> : CVCL::Dict< _Key, _Data >, CVCL::Dict_Entry< _Key, _Data >
• dir() : CVCL::Clause
• diseqToIneq() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• distribL() : CVCL::RefinedArithTheoremProducer
• distribR() : CVCL::RefinedArithTheoremProducer
• divideDef() : CVCL::RefinedArithTheoremProducer
• divideExpr() : CVCL::VCL, CVCL::ValidityChecker
• done : CVCL::Parser, CVCL::ParserTemp
• doSolve() : CVCL::TheoryArith
• dumpTrace() : CVCL::Debug

- e -

• eliminateSkolemAxioms() : CVCL::SearchEngineTheoremProducer, CVCL::SearchEngineRules
• empty() : CVCL::Hash_Table< _Key, _Data >, CVCL::ExprHashMap< Data >, CVCL::ExprMap< Data >, CVCL::Assumptions
• emptyTrash() : CVCL::CDMapOrdered< Key, Data >, CVCL::CDMap< Key, Data, HashFcn >
• end() : CVCL::Hash_Table< _Key, _Data >, CVCL::ExprHashMap< Data >, CVCL::ExprMap< Data >, CVCL::Expr, CVCL::CDMapOrdered< Key, Data >, CVCL::CDMap< Key, Data, HashFcn >, CVCL::CDList< T >, CVCL::Assumptions
• enqueueCNF() : CVCL::SearchEngine
• enqueueCNFrec() : CVCL::SearchEngine
• enqueueEquality() : CVCL::TheoryCore, CVCL::Theory
• enqueueFact() : CVCL::TheoryCore, CVCL::Theory, CVCL::SearchEngineFast
• enqueueSE() : CVCL::TheoryCore
• eqConst() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• eqElimIntRule() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• eqExpr() : CVCL::VCL, CVCL::ValidityChecker, CVCL::Expr
• eqToBits() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• equalLeaves1() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• equalLeaves2() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• equalLeaves3() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• equalLeaves4() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• erase() : CVCL::Hash_Table< _Key, _Data >, CVCL::ExprHashMap< Data >, CVCL::ExprMap< Data >, CVCL::AssumptionsValue
• error() : CVCL::ParserTemp
• eval() : CVCL::RefinedArithTheoremProducer
• EvalException() : CVCL::EvalException
• evaluateCommand() : CVCL::VCCmd
• evaluateNext() : CVCL::VCCmd
• Exception() : CVCL::Exception
• existsExpr() : CVCL::VCL, CVCL::ValidityChecker
• expandDarkShadow() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• expandEq() : CVCL::RecordsTheoremProducer, CVCL::RecordsProofRules
• expandGrayShadow() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• expandGrayShadow0() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• expandGrayShadowConst() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• expandNeq() : CVCL::RecordsTheoremProducer, CVCL::RecordsProofRules
• expandRecord() : CVCL::RecordsTheoremProducer, CVCL::RecordsProofRules
• expandSimulate() : CVCL::SimulateTheoremProducer, CVCL::SimulateProofRules
• expandTuple() : CVCL::RecordsTheoremProducer, CVCL::RecordsProofRules
• expandTypePred() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• Expr : CVCL::Expr, CVCL::TupleIndex, CVCL::RecField, CVCL::ExprRecord, CVCL::BoolVarExprValue, CVCL::NamedExprValue, CVCL::ExprClosure, CVCL::ExprApply, CVCL::ExprCC, CVCL::ExprBoundVar, CVCL::ExprVar, CVCL::ExprRational, CVCL::ExprSkolem, CVCL::ExprString, CVCL::ExprNode, CVCL::ExprValue, CVCL::Op, CVCL::ExprManager, CVCL::Expr::iterator
• expr : CVCL::ParserTemp
• Expr::iterator : CVCL::ExprValue
• ExprApply() : CVCL::ExprApply
• ExprBoundVar() : CVCL::ExprBoundVar
• ExprCC() : CVCL::ExprCC
• ExprClosure() : CVCL::ExprClosure
• ExprGeneric() : CVCL::ExprGeneric
• ExprGrayShadow() : CVCL::ExprGrayShadow
• ExprHasher : CVCL::Expr
• ExprHashMap : CVCL::ExprHashMap< Data >, CVCL::ExprHashMap< Data >::iterator
• ExprHashMapType : CVCL::ExprHashMap< Data >
• ExprManager : CVCL::ExprManager, CVCL::TupleIndex, CVCL::RecField, CVCL::ExprRecord, CVCL::BoolVarExprValue, CVCL::NamedExprValue, CVCL::ExprClosure, CVCL::ExprApply, CVCL::ExprCC, CVCL::ExprBoundVar, CVCL::ExprVar, CVCL::ExprRational, CVCL::ExprSkolem, CVCL::ExprString, CVCL::ExprNode, CVCL::ExprValue, CVCL::Expr
• ExprManagerNotifyObj() : CVCL::ExprManagerNotifyObj
• ExprMap : CVCL::ExprMap< Data >, CVCL::ExprMap< Data >::iterator
• ExprMapType : CVCL::ExprMap< Data >
• ExprNode : CVCL::ExprNode, CVCL::Expr
• ExprRational() : CVCL::ExprRational
• ExprRecord() : CVCL::ExprRecord
• ExprSkolem() : CVCL::ExprSkolem
• ExprStream() : CVCL::ExprStream
• ExprString() : CVCL::ExprString
• ExprValue : CVCL::ExprValue, CVCL::ExprManager, CVCL::Expr
• ExprValueSet : CVCL::ExprManager
• exprVar() : CVCL::CNF
• ExprVar() : CVCL::ExprVar
• extractAnd() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• extractBitwise() : CVCL::BitvectorTheoremProducer
• extractBVMult() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• extractBVPlus() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• extractConcat() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• extractConst() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• extractExtract() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• extractNeg() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• extractOr() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• extractWhole() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules

- f -

• f() : CVCL::ArithTheoremProducer
• falseExpr : CVCL::VCL, CVCL::ValidityChecker, CVCL::Theory, CVCL::ExprManager, CVCL::Expr
• fd : std::fdinbuf, std::fdoutbuf
• fdinbuf() : std::fdinbuf
• fdistream() : std::fdistream
• fdostream() : std::fdostream
• fdoutbuf() : std::fdoutbuf
• Fetch() : CVCL::Hash_Table< _Key, _Data >, CVCL::Dict< _Key, _Data >
• fileName : CVCL::ParserTemp
• find() : CVCL::Hash_Table< _Key, _Data >, CVCL::Theory, CVCL::ExprHashMap< Data >, CVCL::ExprMap< Data >, CVCL::CDMapOrdered< Key, Data >, CVCL::CDMap< Key, Data, HashFcn >, CVCL::AssumptionsValue, CVCL::Assumptions
• Find_Hash_Entry() : CVCL::Hash_Table< _Key, _Data >
• Find_Insert_Point() : CVCL::Dict< _Key, _Data >
• findAxioms() : CVCL::VCCmd
• findBounds() : CVCL::TheoryArith
• findExpr : CVCL::Theory, CVCL::Assumptions
• findExprs : CVCL::Assumptions
• findInCNFCache() : CVCL::SearchEngine
• findInLocalCache() : CVCL::CommonTheoremProducer
• findInstAssumptions() : CVCL::TheoryQuant
• findRationalBound() : CVCL::TheoryArith
• findSplitter() : CVCL::DecisionEngineMBTF, CVCL::DecisionEngineDFS, CVCL::DecisionEngineCaching, CVCL::DecisionEngine, CVCL::SearchEngineFast
• findSplitterRec() : CVCL::DecisionEngine
• findTheorem() : CVCL::Assumptions
• finiteInterval() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• fixConflict() : CVCL::SearchEngineFast
• flag() : CVCL::Statistics, CVCL::Debug
• FlagMap : CVCL::Debug
• flattenBVPlus() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules, CVCL::TheoryBitvector
• flipBVMult() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• flipInequality() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• floor() : CVCL::Rational, CVCL::Rational::Impl
• forallExpr() : CVCL::VCL, CVCL::ValidityChecker
• frac() : CVCL::RefinedArithTheoremProducer
• FreeConst() : CVCL::TheoryArith::FreeConst
• freeConstIneq() : CVCL::TheoryArith
• full_cleanup : args
• funExpr() : CVCL::VCL, CVCL::ValidityChecker
• funType() : CVCL::VCL, CVCL::ValidityChecker, CVCL::Type

- g -

• gc() : CVCL::VariableManager, CVCL::ExprManager
• gcd : CVCL::Rational, CVCL::Rational::Impl
• geExpr() : CVCL::VCL, CVCL::ValidityChecker
• generalIneqn() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• get() : CVCL::SmartCDO< T >, CVCL::CDO< T >, CVCL::CDOmapOrdered< Key, Data >, CVCL::CDOmap< Key, Data, HashFcn >
• getAntecedent() : CVCL::VariableValue, CVCL::Variable
• getAntecedentIdx() : CVCL::VariableValue, CVCL::Variable
• getAssertions() : CVCL::VCL, CVCL::ValidityChecker, CVCL::SearchEngine
• getAssumpThm() : CVCL::VariableValue, CVCL::Variable
• getAssumptions() : CVCL::TheoremValue, CVCL::VCL, CVCL::ValidityChecker, CVCL::Theorem3, CVCL::Theorem, CVCL::SearchEngine
• getAssumptionsCopy() : CVCL::Theorem3, CVCL::Theorem
• getAssumptionsRec() : CVCL::VCL, CVCL::Theorem
• getAssumptionsRef() : CVCL::TheoremValue, CVCL::Theorem3, CVCL::Theorem
• getAssumptionsTCC() : CVCL::VCL, CVCL::ValidityChecker
• getAxiomAssumptions() : CVCL::Theorem
• getBaseType() : CVCL::VCL, CVCL::ValidityChecker, CVCL::Theory, CVCL::TheoremProducer
• getBitvectorTypeParam() : CVCL::TheoryBitvector
• getBody() : CVCL::ExprClosure, CVCL::ExprValue, CVCL::Expr
• getBool() : CVCL::CLFlag
• getBoolExtractIndex() : CVCL::TheoryBitvector
• getBoundIndex() : CVCL::ExprSkolem, CVCL::ExprValue, CVCL::Expr
• getBVMultParam() : CVCL::TheoryBitvector
• getBVPlusParam() : CVCL::TheoryBitvector
• getC1() : CVCL::ArithTheoremProducer, CVCL::TheoryArith
• getC2() : CVCL::ArithTheoremProducer, CVCL::TheoryArith
• getCachedValue() : CVCL::TheoremValue, CVCL::Theorem
• getCDExprAttr() : CVCL::ExprValue, CVCL::Expr
• getCDExprAttrSize() : CVCL::ExprValue, CVCL::Expr
• getCDExprValue() : CVCL::ExprValue, CVCL::Expr
• getCDExprValueSize() : CVCL::ExprValue, CVCL::Expr
• getCDIntAttr() : CVCL::ExprValue, CVCL::Expr
• getCDIntAttrSize() : CVCL::ExprValue, CVCL::Expr
• getCDIntValue() : CVCL::ExprValue, CVCL::Expr
• getCDIntValueSize() : CVCL::ExprValue, CVCL::Expr
• getCDTheoremAttr() : CVCL::ExprValue, CVCL::Expr
• getCDTheoremAttrSize() : CVCL::ExprValue, CVCL::Expr
• getCDTheoremValue() : CVCL::ExprValue, CVCL::Expr
• getCDTheoremValueSize() : CVCL::ExprValue, CVCL::Expr
• getClosure() : CVCL::VCL, CVCL::ValidityChecker
• getCM() : CVCL::VCL, CVCL::VariableManager, CVCL::ExprManager, CVCL::Debug, CVCL::Context
• getConcreteModel() : CVCL::VCL, CVCL::ValidityChecker, CVCL::SearchEngine
• getConst() : CVCL::TheoryArith::Ineq, CVCL::TheoryArith::FreeConst
• getCounterExample() : CVCL::VCL, CVCL::ValidityChecker, CVCL::SearchEngineFast, CVCL::SearchEngine
• getCreated() : CVCL::Rational
• getCurrentContext() : CVCL::VCL, CVCL::ValidityChecker, CVCL::ExprManager, CVCL::ContextManager
• getDeleted() : CVCL::Rational
• getDen() : CVCL::Rational::Impl
• getDenominator() : CVCL::Rational
• getE() : CVCL::ArithTheoremProducer, CVCL::TheoryArith
• getEM() : CVCL::VCL, CVCL::ValidityChecker, CVCL::Theory, CVCL::TheoremManager, CVCL::Op, CVCL::Expr, CVCL::Debug
• getEmptyVector() : CVCL::ExprManager
• getExistential() : CVCL::ExprSkolem, CVCL::ExprValue, CVCL::Expr
• getExpandFlag() : CVCL::TheoremValue, CVCL::Theorem
• getExpr() : CVCL::ReflexivityTheoremValue, CVCL::RWTheoremValue, CVCL::TheoremValue, CVCL::VariableValue, CVCL::Literal, CVCL::Variable, CVCL::Type, CVCL::Theorem3, CVCL::Theorem, CVCL::Proof, CVCL::NotifyList, CVCL::Op
• getExprAttr() : CVCL::ExprValue, CVCL::Expr
• getExprAttrSize() : CVCL::ExprValue, CVCL::Expr
• getExprValue() : CVCL::BVTypePredExpr, CVCL::ExprGrayShadow, CVCL::ExprValue, CVCL::Expr
• getExprValueSize() : CVCL::BVTypePredExpr, CVCL::ExprGrayShadow, CVCL::ExprValue, CVCL::Expr
• getExtractHi() : CVCL::TheoryBitvector
• getExtractLow() : CVCL::TheoryBitvector
• getField() : CVCL::RecordsTheoremProducer, CVCL::TheoryRecords, CVCL::ExprValue
• getFieldIndex() : CVCL::RecordsTheoremProducer, CVCL::TheoryRecords
• getFields() : CVCL::RecordsTheoremProducer, CVCL::TheoryRecords, CVCL::ExprValue
• getFind() : CVCL::Expr
• getFixedLeftShiftParam() : CVCL::TheoryBitvector
• getFixedRightShiftParam() : CVCL::TheoryBitvector
• getFlag() : CVCL::TheoremManager, CVCL::ExprManager, CVCL::Expr, CVCL::CLFlags
• getFlag0() : CVCL::CLFlags
• getFlags() : CVCL::VCL, CVCL::ValidityChecker
• getFun() : CVCL::ExprApply, CVCL::ExprValue, CVCL::Expr
• getHeight() : CVCL::ExprValue, CVCL::Expr
• getHelp() : CVCL::CLFlag
• getHighestKid() : CVCL::ExprValue, CVCL::Expr
• getImpliedLiteral() : CVCL::VCL, CVCL::ValidityChecker, CVCL::SearchEngine
• getIndex() : CVCL::RecordsTheoremProducer, CVCL::TheoryRecords, CVCL::Expr
• getInputLang() : CVCL::ExprManager
• getInt() : CVCL::Rational, CVCL::CLFlag, CVCL::Rational::Impl
• getIntAttr() : CVCL::ExprValue, CVCL::Expr
• getIntAttrSize() : CVCL::ExprValue, CVCL::Expr
• getIntValue() : CVCL::TupleIndex, CVCL::BVParameterExpr, CVCL::BVPlusExpr, CVCL::BVConstExpr, CVCL::ExprValue, CVCL::Expr
• getIntValueSize() : CVCL::TupleIndex, CVCL::BVParameterExpr, CVCL::BVPlusExpr, CVCL::BVConstExpr, CVCL::ExprValue, CVCL::Expr
• getIsAtomicFlag() : CVCL::Expr
• getKey() : CVCL::CDOmapOrdered< Key, Data >, CVCL::CDOmap< Key, Data, HashFcn >
• getKids() : CVCL::ExprBoundVar, CVCL::ExprVar, CVCL::ExprRational, CVCL::ExprNode, CVCL::ExprValue, CVCL::Expr
• getKind() : CVCL::ExprValue, CVCL::Op, CVCL::ExprManager, CVCL::Expr
• getKindName() : CVCL::ExprManager
• getLangUsed() : CVCL::TheoryArith
• getLHS() : CVCL::ReflexivityTheoremValue, CVCL::RWTheoremValue, CVCL::TheoremValue, CVCL::Theorem3, CVCL::Theorem
• getLiteral() : CVCL::Clause
• getLiterals() : CVCL::Clause
• getLitFlag() : CVCL::TheoremValue, CVCL::Theorem
• getMM() : CVCL::ReflexivityTheoremValue, CVCL::RWTheoremValue, CVCL::TheoremValue, CVCL::TheoremManager, CVCL::ExprValue, CVCL::ExprManager
• getMMIndex() : CVCL::TupleIndex, CVCL::RecField, CVCL::ExprRecord, CVCL::BVTypePredExpr, CVCL::BVParameterExpr, CVCL::BVPlusExpr, CVCL::BVConstExpr, CVCL::ExprGrayShadow, CVCL::BoolVarExprValue, CVCL::NamedExprValue, CVCL::ExprClosure, CVCL::ExprApply, CVCL::ExprCC, CVCL::ExprBoundVar, CVCL::ExprVar, CVCL::ExprRational, CVCL::ExprSkolem, CVCL::ExprString, CVCL::ExprNode, CVCL::ExprValue, CVCL::Expr
• getModelTerm() : CVCL::Theory
• getModelValue() : CVCL::TheoryCore, CVCL::Theory
• getName() : CVCL::Theory, CVCL::NamedExprValue, CVCL::ExprBoundVar, CVCL::ExprVar, CVCL::ExprValue, CVCL::Expr
• getNeg() : CVCL::TheoryCore
• getNegExpr() : CVCL::VariableValue, CVCL::Variable
• getNotify() : CVCL::Expr
• getNullExpr() : CVCL::ExprManager
• getNum() : CVCL::Rational::Impl
• getNumerator() : CVCL::Rational
• getNumTheories() : CVCL::Theory
• getOpKind() : CVCL::Theory
• getOS() : CVCL::Debug
• getOSDumpTrace() : CVCL::Debug
• getOtherAttr() : CVCL::ExprValue, CVCL::Expr
• getOtherAttrSize() : CVCL::ExprValue, CVCL::Expr
• getOtherValue() : CVCL::ExprRecord, CVCL::ExprValue, CVCL::Expr
• getOtherValueSize() : CVCL::ExprRecord, CVCL::ExprValue, CVCL::Expr
• getOutputLang() : CVCL::ExprManager
• getParent() : CVCL::ExprStream
• getPrinter() : CVCL::ExprManager
• getPrompt() : CVCL::ParserTemp
• getProof() : CVCL::TheoremValue, CVCL::VCL, CVCL::ValidityChecker, CVCL::Theorem3, CVCL::Theorem, CVCL::SearchEngine
• getProofClosure() : CVCL::VCL, CVCL::ValidityChecker
• getProofTCC() : CVCL::VCL, CVCL::ValidityChecker
• getQuantBody() : CVCL::Expr
• getRational() : CVCL::ExprRational, CVCL::ExprValue, CVCL::Expr
• getRatValue() : CVCL::ExprGrayShadow, CVCL::ExprValue, CVCL::Expr
• getRatValueSize() : CVCL::ExprGrayShadow, CVCL::ExprValue, CVCL::Expr
• getReflMM() : CVCL::TheoremManager
• getRep() : CVCL::ExprCC, CVCL::ExprValue, CVCL::Expr
• getResource() : CVCL::TheoryCore
• getRHS() : CVCL::ReflexivityTheoremValue, CVCL::RWTheoremValue, CVCL::TheoremValue, CVCL::Theorem3, CVCL::Theorem
• getRules() : CVCL::VariableManager
• getRWMM() : CVCL::TheoremManager
• getScope() : CVCL::TheoremValue, CVCL::VariableValue, CVCL::Literal, CVCL::Variable, CVCL::Theorem3, CVCL::Theorem, CVCL::Clause
• getSE() : CVCL::VCL, CVCL::Debug
• getSig() : CVCL::ExprCC, CVCL::ExprValue, CVCL::Expr
• getSimpCache() : CVCL::Expr
• getSimpCacheTag() : CVCL::ExprManager
• getSimpFrom() : CVCL::ExprValue, CVCL::Expr
• getStatistics() : CVCL::VCL, CVCL::ValidityChecker
• getString() : CVCL::ExprString, CVCL::ExprValue, CVCL::Expr, CVCL::CLFlag
• getStringValue() : CVCL::RecField, CVCL::ExprRecord, CVCL::ExprValue, CVCL::Expr
• getStringValueSize() : CVCL::RecField, CVCL::ExprRecord, CVCL::ExprValue, CVCL::Expr
• getStrVec() : CVCL::CLFlag
• getTCC() : CVCL::VCL, CVCL::ValidityChecker, CVCL::Theory
• getTerms() : CVCL::TheoryCore, CVCL::Theory
• getTheorem() : CVCL::VariableValue, CVCL::Literal, CVCL::Variable, CVCL::Clause
• getTheoremAttr() : CVCL::ExprValue, CVCL::Expr
• getTheoremAttrSize() : CVCL::ExprValue, CVCL::Expr
• getTheoremValue() : CVCL::ExprValue, CVCL::Expr
• getTheoremValueSize() : CVCL::ExprValue, CVCL::Expr
• getTheory() : CVCL::NotifyList
• getTM() : CVCL::VCL
• getTupleIndex() : CVCL::ExprValue
• getType() : CVCL::VCL, CVCL::ValidityChecker, CVCL::Theory, CVCL::TheoremProducer, CVCL::CLFlag
• getTypeDeclName() : CVCL::Type
• getTypePred() : CVCL::VCL, CVCL::ValidityChecker, CVCL::Theory
• getTypePredExpr() : CVCL::TheoryBitvector
• getTypePredType() : CVCL::TheoryBitvector
• getUid() : CVCL::ExprBoundVar, CVCL::ExprValue, CVCL::Expr
• getUnsigned() : CVCL::Rational, CVCL::Rational::Impl
• getV() : CVCL::ArithTheoremProducer, CVCL::TheoryArith
• getValue() : CVCL::VariableValue, CVCL::Literal, CVCL::Variable
• getVar() : CVCL::Literal, CVCL::BoolVarExprValue, CVCL::ExprValue, CVCL::Expr
• getVars() : CVCL::ExprClosure, CVCL::ExprValue, CVCL::Expr
• getVCL() : CVCL::TheoremManager, CVCL::Debug
• goalSatisfied() : CVCL::DecisionEngineMBTF, CVCL::DecisionEngineDFS, CVCL::DecisionEngineCaching, CVCL::DecisionEngine
• grayShadow() : CVCL::ArithTheoremProducer, CVCL::TheoryArith
• grayShadowConst() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• greaterthan() : CVCL::ArithTheoremProducer
• gtExpr() : CVCL::VCL, CVCL::ValidityChecker

- h -

• h : CVCL::ExprManager::HashString, endif::hash< std::string >, CVCL::AVHash
• hasFind() : CVCL::Expr
• hash() : CVCL::ExprGrayShadow, CVCL::Rational, CVCL::ExprRational, CVCL::ExprString, CVCL::ExprValue, CVCL::ExprManager, CVCL::Expr
• Hash_Entry() : CVCL::Hash_Entry< _Key, _Data >
• Hash_Ptr() : CVCL::Hash_Ptr< _Key, _Data >
• Hash_Ptr<_Key, _Data> : CVCL::Hash_Table< _Key, _Data >
• Hash_Table() : CVCL::Hash_Table< _Key, _Data >
• Hash_Table<_Key, _Data> : CVCL::Hash_Entry< _Key, _Data >
• HashEV : CVCL::ExprManager::HashEV, CVCL::ExprManager
• hasLastIndex() : CVCL::Expr
• hasRep() : CVCL::Expr
• hasSig() : CVCL::Expr
• hasSimpFrom() : CVCL::Expr
• hasTheory() : CVCL::TheoryCore

- i -

• i : CVCL::CLFlag
• id() : CVCL::Context, CVCL::Clause
• idExpr() : CVCL::VCL, CVCL::ValidityChecker
• IF_DEBUG() : CVCL::TheoryCore, CVCL::TheoryArray, CVCL::SearchEngineFast, CVCL::ExprManager, CVCL::ContextObj, CVCL::ContextObjChain, CVCL::Clause, CVCL::ClauseValue
• iffCNFRule() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• iffContrapositive() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• iffExpr() : CVCL::VCL, CVCL::ValidityChecker, CVCL::Expr
• iffFalseElim() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• iffMP() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• iffNotFalse() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• iffToAndOr() : CVCL::CommonTheoremProducer
• iffToClauses() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• IffToIte() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• iffTrue() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• iffTrueElim() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• ifLiftRule() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• impCNFRule() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• impExpr() : CVCL::Expr
• Impl() : CVCL::Rational::Impl
• implContrapositive() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• impliesExpr() : CVCL::VCL, CVCL::ValidityChecker
• implIntro() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• implIntro3() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• implMP() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• importExpr() : CVCL::VCL, CVCL::ValidityChecker
• importType() : CVCL::VCL, CVCL::ValidityChecker
• ImpToIte() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• incIndent() : CVCL::ExprManager
• incomplete() : CVCL::VCL, CVCL::ValidityChecker, CVCL::TheoryCore, CVCL::Theory
• inconsistent() : CVCL::VCL, CVCL::ValidityChecker, CVCL::TheoryCore, CVCL::Theory
• inconsistentThm() : CVCL::TheoryCore, CVCL::Theory
• incRefcount() : CVCL::ExprValue
• indent() : CVCL::ExprManager, CVCL::Expr
• Ineq() : CVCL::TheoryArith::Ineq
• ineq() : CVCL::TheoryArith::Ineq
• init() : CVCL::TheoremManager, CVCL::Debug, CVCL::Assumptions
• initParser() : CVCL::Parser
• insert() : CVCL::Hash_Table< _Key, _Data >, CVCL::ExprHashMap< Data >, CVCL::ExprMap< Data >, CVCL::CDMapOrdered< Key, Data >, CVCL::CDMap< Key, Data, HashFcn >
• Insert() : CVCL::Hash_Table< _Key, _Data >, CVCL::Dict< _Key, _Data >
• installExprValue() : CVCL::ExprManager
• instantiate() : CVCL::TheoryQuant
• 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
• is : CVCL::ParserTemp
• IS_ATOMIC : CVCL::Expr
• isActive() : CVCL::TheoremManager, CVCL::ExprManager
• isAnd() : CVCL::Expr
• isApply() : CVCL::ExprApply, CVCL::ExprValue, CVCL::Expr
• isAtomic() : CVCL::Theory
• isAtomicFormula() : CVCL::Theory
• isAxiom() : CVCL::TheoremValue, CVCL::Theorem3, CVCL::Theorem
• isBetter() : CVCL::DecisionEngineMBTF, CVCL::DecisionEngineDFS, CVCL::DecisionEngineCaching, CVCL::DecisionEngine
• isBool() : CVCL::Type
• isBoolConst() : CVCL::Expr
• isBoolVar() : CVCL::BoolVarExprValue, CVCL::ExprValue, CVCL::Expr
• isBoundVar() : CVCL::ExprBoundVar, CVCL::ExprValue
• isClause() : CVCL::SearchEngine
• isClosure() : CVCL::ExprClosure, CVCL::ExprValue, CVCL::Expr
• isCNFVar() : CVCL::SearchEngine
• isConst() : CVCL::Assumptions
• isCurrent() : CVCL::ContextObj, CVCL::Scope
• isEq() : CVCL::Expr
• isExists() : CVCL::Expr
• isFalse() : CVCL::Expr
• isFinite() : CVCL::Type
• isFlagged() : CVCL::TheoremValue, CVCL::Theorem
• isForall() : CVCL::Expr
• isFunction() : CVCL::Type
• isGeneric() : CVCL::BVTypePredExpr, CVCL::BVParameterExpr, CVCL::BVPlusExpr, CVCL::BVConstExpr, CVCL::ExprValue, CVCL::Expr
• isGoodSplitter() : CVCL::SearchEngine
• isGrayShadow() : CVCL::ArithTheoremProducer, CVCL::TheoryArith
• isIff() : CVCL::Expr
• isImpl() : CVCL::Expr
• isInitialized() : CVCL::Expr
• isIntConst() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• isInteger() : CVCL::TheoryArith, CVCL::Rational, CVCL::Rational::Impl
• isIntegerDerive() : CVCL::TheoryArith
• isIntegerThm() : CVCL::TheoryArith
• isITE() : CVCL::Expr
• isKindRegistered() : CVCL::ExprManager
• isLambda() : CVCL::Expr
• isLeaf() : CVCL::Theory
• isLeafIn() : CVCL::Theory
• isLiteral() : CVCL::VCL, CVCL::Theory, CVCL::Theorem3, CVCL::Theorem, CVCL::SearchEngine
• isNegative() : CVCL::Literal
• isNot() : CVCL::Expr
• isNull() : CVCL::Literal, CVCL::Variable, CVCL::Type, CVCL::Theorem3, CVCL::Theorem, CVCL::SmartCDO< T >, CVCL::Proof, CVCL::Expr, CVCL::Clause, CVCL::Assumptions
• isolateVariable() : CVCL::TheoryArith
• isOr() : CVCL::Expr
• isPositive() : CVCL::Literal
• isPropAtom() : CVCL::TheoryCore, CVCL::SearchEngine
• isPropClause() : CVCL::SearchEngine
• isPropLiteral() : CVCL::TheoryCore, CVCL::SearchEngine
• 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
• isSkolem() : CVCL::Expr
• isStale() : CVCL::TheoryArith
• isString() : CVCL::ExprString, CVCL::ExprValue, CVCL::Expr
• isSubtype() : CVCL::Type
• isSyntacticRational() : CVCL::TheoryArith
• isSyntacticUMinusVar() : CVCL::TheoryArith
• isTerm() : CVCL::Theory
• isTrue() : CVCL::Expr
• isTuple() : CVCL::TheoryRecords
• isTupleAccess() : CVCL::RecordsTheoremProducer, CVCL::TheoryRecords
• isTupleType() : CVCL::TheoryRecords
• isType() : CVCL::Type, CVCL::Expr
• isTypeDecl() : CVCL::Type
• isTypeKind() : CVCL::ExprManager
• isUnsigned() : CVCL::Rational
• isVar() : CVCL::ExprBoundVar, CVCL::ExprVar, CVCL::ExprSkolem, CVCL::ExprValue, CVCL::Expr
• isXor() : CVCL::Expr
• ite_convert() : CVCL::TheoryCore
• ite_reorder() : CVCL::TheoryCore
• ite_simplify() : CVCL::TheoryCore
• iteCNFRule() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• iteExpr() : CVCL::VCL, CVCL::ValidityChecker, CVCL::Expr
• 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::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules

- k -

• Key() : CVCL::Hash_Entry< _Key, _Data >, CVCL::Dict_Entry< _Key, _Data >
• kidsCanonical() : CVCL::TheoryArith
• kill() : CVCL::SmartCDO< T >::RefCDO< U >

- l -

• lambdaExpr() : CVCL::VCL, CVCL::ValidityChecker, CVCL::TheoryUF
• lang() : CVCL::ExprStream
• lastIndex() : CVCL::ExprManager
• lastSplitter() : CVCL::DecisionEngine
• lcm : CVCL::Rational, CVCL::Rational::Impl
• leavesAreSimp() : CVCL::Theory
• leExpr() : CVCL::VCL, CVCL::ValidityChecker
• leftShiftToConcat() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• lessThan() : CVCL::TheoryArith::VarOrderGraph
• lessThanToLE() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• lessThanVar() : CVCL::TheoryArith
• level() : CVCL::Context, CVCL::ContextObj, CVCL::Scope
• lhsEqRhsIneqn() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• lhsMinusRhsRule() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• lineNum : CVCL::ParserTemp
• lineWidth() : CVCL::ExprStream, CVCL::ExprManager
• listExpr() : CVCL::VCL, CVCL::ValidityChecker
• Literal() : CVCL::Literal
• loadFile() : CVCL::VCL, CVCL::ValidityChecker
• lookupSubtypePred() : CVCL::Expr
• lookupTCC() : CVCL::Expr
• lookupType() : CVCL::VCL, CVCL::ValidityChecker, CVCL::Expr
• lookupVar() : CVCL::VCL, CVCL::ValidityChecker, CVCL::Theory
• ltAddR() : CVCL::RefinedArithTheoremProducer
• ltExpr() : CVCL::VCL, CVCL::ValidityChecker
• ltScale() : CVCL::RefinedArithTheoremProducer
• ltTrans() : CVCL::RefinedArithTheoremProducer

- m -

• makeCopy() : CVCL::NotifyList, CVCL::ContextObj, CVCL::CDO< T >, CVCL::CDMapOrdered< Key, Data >, CVCL::CDMapOrderedData, CVCL::CDOmapOrdered< Key, Data >, CVCL::CDMap< Key, Data, HashFcn >, CVCL::CDMapData, CVCL::CDOmap< Key, Data, HashFcn >, CVCL::CDList< T >
• makeCurrent() : CVCL::ContextObj
• mapTermsByType() : CVCL::TheoryQuant
• markDeleted() : CVCL::Clause
• markSat() : CVCL::Clause
• matches() : CVCL::Theorem
• MemoryManagerChunks() : CVCL::MemoryManagerChunks
• MemoryManagerMalloc() : CVCL::MemoryManagerMalloc
• minusDef() : CVCL::RefinedArithTheoremProducer
• minusExpr() : CVCL::VCL, CVCL::ValidityChecker
• minusToPlus() : CVCL::RefinedArithTheoremProducer, CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• mod : CVCL::Rational, CVCL::Rational::Impl
• modEq() : CVCL::ArithTheoremProducer
• modified() : CVCL::CLFlag
• monomialModM() : CVCL::ArithTheoremProducer
• monomialMulF() : CVCL::ArithTheoremProducer
• multAssoc() : CVCL::RefinedArithTheoremProducer
• multEqn() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• multExpr() : CVCL::VCL, CVCL::ValidityChecker
• multIneqn() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• multInvR() : CVCL::RefinedArithTheoremProducer
• multLID() : CVCL::RefinedArithTheoremProducer
• multSymm() : CVCL::RefinedArithTheoremProducer
• multZeroL() : CVCL::RefinedArithTheoremProducer

- n -

• name() : CVCL::Context
• NamedExprValue() : CVCL::NamedExprValue
• neg() : CVCL::RefinedArithTheoremProducer
• negate() : CVCL::Expr
• negatedInequality() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• negConcat() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• negConst() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• negIntro() : CVCL::SearchEngineTheoremProducer, CVCL::SearchEngineRules
• negNeg() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• newApplyExpr : CVCL::Expr
• newAssertion() : CVCL::SearchEngineFast, CVCL::SearchEngine
• newAxiom() : CVCL::TheoremProducer
• newAxiom3() : CVCL::TheoremProducer
• newBitvectorType() : CVCL::TheoryBitvector
• newBitvectorTypeExpr() : CVCL::TheoryBitvector
• newBitvectorTypePred() : CVCL::TheoryBitvector
• newBoolExtractExpr() : CVCL::TheoryBitvector
• newBoolVarExpr : CVCL::Expr
• newBoundVar() : CVCL::Theory
• newBoundVarExpr : CVCL::Expr
• newBVAndExpr() : CVCL::TheoryBitvector
• newBVConstExpr() : CVCL::TheoryBitvector
• newBVExtractExpr() : CVCL::TheoryBitvector
• newBVLEExpr() : CVCL::TheoryBitvector
• newBVLTExpr() : CVCL::TheoryBitvector
• newBVMultExpr() : CVCL::TheoryBitvector
• newBVNandExpr() : CVCL::TheoryBitvector
• newBVNegExpr() : CVCL::TheoryBitvector
• newBVNorExpr() : CVCL::TheoryBitvector
• newBVOneString() : CVCL::TheoryBitvector
• newBVOrExpr() : CVCL::TheoryBitvector
• newBVPlusExpr() : CVCL::TheoryBitvector
• newBVUminusExpr() : CVCL::TheoryBitvector
• newBVXnorExpr() : CVCL::TheoryBitvector
• newBVXorExpr() : CVCL::TheoryBitvector
• newBVZeroString() : CVCL::TheoryBitvector
• newChunk() : CVCL::MemoryManagerChunks
• newClosureExpr : CVCL::Expr
• newCommonRules() : CVCL::TheoryCore
• newConcatExpr() : CVCL::TheoryBitvector
• newData() : CVCL::MemoryManagerMalloc, CVCL::MemoryManagerChunks, CVCL::MemoryManager
• newExpr : CVCL::ExprGeneric, CVCL::Expr
• newExprBoundVar() : CVCL::CommonTheoremProducer
• newExprValue() : CVCL::ExprManager
• newFixedLeftShiftExpr() : CVCL::TheoryBitvector
• newFixedRightShiftExpr() : CVCL::TheoryBitvector
• newFunction() : CVCL::Theory
• newKind() : CVCL::ExprManager
• newLabel() : CVCL::TheoremProducer
• newLiteral() : CVCL::SearchEngine
• newName() : CVCL::ExprStream
• newNamedExpr : CVCL::Expr
• newPf() : CVCL::TheoremProducer
• newRatExpr : CVCL::Expr
• newReflTheorem() : CVCL::TheoremProducer
• newRWTheorem() : CVCL::TheoremProducer
• newRWTheorem3() : CVCL::TheoremProducer
• newSkolemExpr : CVCL::Expr
• newStringExpr : CVCL::Expr
• newTheorem() : CVCL::TheoremProducer
• newTheorem3() : CVCL::TheoremProducer
• newTimer() : CVCL::Debug
• newTypeExpr() : CVCL::Theory
• newUserAssertion() : CVCL::SearchEngine
• newVar() : CVCL::Theory
• newVarable() : CVCL::SearchEngine
• newVarExpr : CVCL::Expr
• newVariableValue() : CVCL::VariableManager
• next() : CVCL::Parser, CVCL::CDOmapOrdered< Key, Data >, CVCL::CDOmap< Key, Data, HashFcn >
• Next() : CVCL::Hash_Entry< _Key, _Data >
• nextFlag() : CVCL::ExprManager
• nextIndex() : CVCL::ExprManager
• nodag : CVCL::ExprStream
• normalize() : CVCL::TheoryArith
• normalizeBVArith() : CVCL::TheoryBitvector
• normalizeConcat() : CVCL::TheoryBitvector
• normalizeProjectIneqs() : CVCL::TheoryArith
• notBVLTRule() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• notExpr() : CVCL::VCL, CVCL::ValidityChecker, CVCL::Expr
• notify() : CVCL::VariableManagerNotifyObj, CVCL::TheoryCore::CoreNotifyObj, CVCL::SmartCDO< T >::RefCDO< U >::RefNotifyObj, CVCL::SearchEngineFast::ConflictClauseManager, CVCL::SearchEngine::SearchNotifyObj, CVCL::ExprManagerNotifyObj, CVCL::ContextNotifyObj
• notifyInconsistent() : CVCL::TheoryQuant, CVCL::Theory
• NotifyList() : CVCL::NotifyList
• notifyPre() : CVCL::VariableManagerNotifyObj, CVCL::SmartCDO< T >::RefCDO< U >::RefNotifyObj, CVCL::ExprManagerNotifyObj, CVCL::ContextNotifyObj
• notNotElim() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• notToIff() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• NotToIte() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• Null() : CVCL::Hash_Ptr< _Key, _Data >
• NumEntries() : CVCL::Dict< _Key, _Data >

- o -

• one : CVCL::RefinedArithTheoremProducer
• oneCoeffBVMult() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• Op : CVCL::Op, CVCL::ExprManager, CVCL::Expr
• opCNFRule() : CVCL::CommonTheoremProducer
• operator &&() : CVCL::Expr
• operator * : CVCL::Hash_Ptr< _Key, _Data >, CVCL::_Hashtable_const_iterator< _Key, _Data >, CVCL::_Hashtable_iterator< _Key, _Data >, CVCL::Dict_Ptr< _Key, _Data >, CVCL::Rational, CVCL::ExprHashMap< Data >::iterator::Proxy, CVCL::ExprHashMap< Data >::iterator, CVCL::ExprMap< Data >::iterator::Proxy, CVCL::ExprMap< Data >::iterator, CVCL::Expr::iterator::Proxy, CVCL::Expr::iterator, CVCL::CDMapOrdered< Key, Data >::orderedIterator::Proxy, CVCL::CDMapOrdered< Key, Data >::orderedIterator, CVCL::CDMapOrdered< Key, Data >::iterator::Proxy, CVCL::CDMapOrdered< Key, Data >::iterator, CVCL::CDMap< Key, Data, HashFcn >::orderedIterator::Proxy, CVCL::CDMap< Key, Data, HashFcn >::orderedIterator, CVCL::CDMap< Key, Data, HashFcn >::iterator::Proxy, CVCL::CDMap< Key, Data, HashFcn >::iterator, CVCL::Assumptions::iterator::Proxy, CVCL::Assumptions::iterator, CVCL::Rational::Impl
• operator *=() : CVCL::Rational
• operator bool() : CVCL::StatFlag, CVCL::Parser, CVCL::DebugFlag
• operator Clause &() : CVCL::ClauseOwner
• operator const Clause &() : CVCL::ClauseOwner
• operator Data() : CVCL::CDOmapOrdered< Key, Data >, CVCL::CDOmap< Key, Data, HashFcn >
• operator delete() : CVCL::TupleIndex, CVCL::RecField, CVCL::ExprRecord, CVCL::BVTypePredExpr, CVCL::BVParameterExpr, CVCL::BVPlusExpr, CVCL::BVConstExpr, CVCL::ExprGrayShadow, CVCL::ReflexivityTheoremValue, CVCL::RWTheoremValue, CVCL::TheoremValue, CVCL::VariableValue, CVCL::BoolVarExprValue, CVCL::NamedExprValue, CVCL::ExprClosure, CVCL::ExprApply, CVCL::ExprCC, CVCL::ExprBoundVar, CVCL::ExprVar, CVCL::ExprRational, CVCL::ExprSkolem, CVCL::ExprString, CVCL::ExprNode, CVCL::ExprValue
• operator int() : CVCL::StatCounter, CVCL::DebugCounter
• operator Literal() : CVCL::SearchEngine::Splitter
• operator new() : CVCL::TupleIndex, CVCL::RecField, CVCL::ExprRecord, CVCL::BVTypePredExpr, CVCL::BVParameterExpr, CVCL::BVPlusExpr, CVCL::BVConstExpr, CVCL::ExprGrayShadow, CVCL::ReflexivityTheoremValue, CVCL::RWTheoremValue, CVCL::TheoremValue, CVCL::VariableValue, CVCL::BoolVarExprValue, CVCL::NamedExprValue, CVCL::ExprClosure, CVCL::ExprApply, CVCL::ExprCC, CVCL::ExprBoundVar, CVCL::ExprVar, CVCL::ExprRational, CVCL::ExprSkolem, CVCL::ExprString, CVCL::ExprNode, CVCL::ExprValue
• operator T() : CVCL::SmartCDO< T >, CVCL::CDO< T >
• operator Theorem() : CVCL::VCL::UserAssertion, CVCL::TheoryArith::Ineq
• operator void_pointer() : CVCL::Hash_Ptr< _Key, _Data >
• operator void_ptr() : CVCL::Dict_Ptr< _Key, _Data >
• operator!() : CVCL::Expr
• operator!= : CVCL::Hash_Entry< _Key, _Data >, CVCL::_Hashtable_const_iterator< _Key, _Data >, CVCL::_Hashtable_iterator< _Key, _Data >, CVCL::Theorem3, CVCL::Theorem, CVCL::StatCounter, CVCL::StatFlag, CVCL::Rational, CVCL::ExprHashMap< Data >, CVCL::ExprHashMap< Data >::iterator, CVCL::ExprMap< Data >, CVCL::ExprMap< Data >::iterator, CVCL::Expr, CVCL::Expr::iterator, CVCL::DebugTimer, CVCL::DebugCounter, CVCL::DebugFlag, CVCL::CDMapOrdered< Key, Data >::orderedIterator, CVCL::CDMapOrdered< Key, Data >::iterator, CVCL::CDMap< Key, Data, HashFcn >::orderedIterator, CVCL::CDMap< Key, Data, HashFcn >::iterator, CVCL::AssumptionsValue, CVCL::Assumptions, CVCL::Assumptions::iterator, CVCL::Rational::Impl, CVCL::DebugTime
• operator% : CVCL::Rational, CVCL::Rational::Impl
• operator()() : StrPairLess< T >, MonomialLess, CVCL::TheoremLess, CVCL::ltstr, CVCL::VariableManager::EqLV, CVCL::VariableManager::HashLV, CVCL::TheoryQuant::TypeComp, CVCL::ExprManager::EqEV, CVCL::ExprManager::HashEV, CVCL::ExprManager::HashString, endif::hash< std::string >, endif::hash< CVCL::Expr >, CVCL::Debug::stringHash, CVCL::AVHash
• operator+ : CVCL::Rational, CVCL::DebugTimer, CVCL::AssumptionsValue, CVCL::Assumptions, CVCL::Rational::Impl
• operator++() : CVCL::Hash_Ptr< _Key, _Data >, CVCL::_Hashtable_const_iterator< _Key, _Data >, CVCL::_Hashtable_iterator< _Key, _Data >, CVCL::Dict_Ptr< _Key, _Data >, CVCL::StatCounter, CVCL::StatFlag, CVCL::Rational, CVCL::ExprHashMap< Data >::iterator, CVCL::ExprMap< Data >::iterator, CVCL::Expr::iterator, CVCL::DebugCounter, CVCL::DebugFlag, CVCL::CDMapOrdered< Key, Data >::orderedIterator, CVCL::CDMapOrdered< Key, Data >::iterator, CVCL::CDMap< Key, Data, HashFcn >::orderedIterator, CVCL::CDMap< Key, Data, HashFcn >::iterator, CVCL::Assumptions::iterator
• operator+=() : CVCL::StatCounter, CVCL::Rational, CVCL::DebugTimer, CVCL::DebugCounter, CVCL::DebugTime
• operator-() : CVCL::Rational, CVCL::DebugTimer, CVCL::AssumptionsValue, CVCL::Assumptions, CVCL::Rational::Impl
• operator--() : CVCL::StatCounter, CVCL::StatFlag, CVCL::Rational, CVCL::DebugCounter, CVCL::DebugFlag
• operator-=() : CVCL::StatCounter, CVCL::Rational, CVCL::DebugTimer, CVCL::DebugCounter, CVCL::DebugTime
• operator->() : CVCL::Hash_Ptr< _Key, _Data >, CVCL::_Hashtable_const_iterator< _Key, _Data >, CVCL::_Hashtable_iterator< _Key, _Data >, CVCL::Dict_Ptr< _Key, _Data >, CVCL::ExprHashMap< Data >::iterator, CVCL::ExprMap< Data >::iterator, CVCL::Expr::iterator, CVCL::Assumptions::iterator
• operator/ : CVCL::Rational, CVCL::Rational::Impl
• operator/=() : CVCL::Rational
• operator< : CVCL::VCL::UserAssertion, CVCL::Rational, CVCL::Expr, CVCL::DebugTimer, CVCL::Rational::Impl, CVCL::DebugTime
• operator<< : CVCL::VariableValue, CVCL::Literal, CVCL::Variable, CVCL::TheoryArith, CVCL::Theorem3, CVCL::Theorem, CVCL::Statistics, CVCL::StatCounter, CVCL::StatFlag, CVCL::Rational, CVCL::Proof, CVCL::ExprStream, CVCL::Op, CVCL::Expr, CVCL::Exception, CVCL::DebugTimer, CVCL::DebugCounter, CVCL::DebugFlag, CVCL::CompactClause, CVCL::Clause, CVCL::AssumptionsValue, CVCL::Assumptions, CVCL::Rational::Impl, CVCL::DebugTime
• operator<= : CVCL::Rational, CVCL::Expr, CVCL::DebugTimer, CVCL::Rational::Impl, CVCL::DebugTime
• operator=() : CVCL::Hash_Table< _Key, _Data >, CVCL::Dict< _Key, _Data >, CVCL::TheoremValue, CVCL::Variable, CVCL::Theorem, CVCL::StatCounter, CVCL::StatFlag, CVCL::SmartCDO< T >, CVCL::SearchEngine::Splitter, CVCL::Rational, CVCL::NotifyList, CVCL::Op, CVCL::Expr, CVCL::DebugTimer, CVCL::DebugCounter, CVCL::DebugFlag, CVCL::ContextObj, CVCL::CLFlag, CVCL::ClauseOwner, CVCL::Clause, CVCL::ClauseValue, CVCL::CDO< T >, CVCL::CDOmapOrdered< Key, Data >, CVCL::CDOmap< Key, Data, HashFcn >, CVCL::Assumptions, CVCL::Rational::Impl
• operator== : CVCL::TupleIndex, CVCL::RecField, CVCL::ExprRecord, CVCL::Hash_Entry< _Key, _Data >, CVCL::_Hashtable_const_iterator< _Key, _Data >, CVCL::_Hashtable_iterator< _Key, _Data >, CVCL::BVTypePredExpr, CVCL::BVParameterExpr, CVCL::BVPlusExpr, CVCL::BVConstExpr, CVCL::ExprGrayShadow, CVCL::VariableValue, CVCL::Literal, CVCL::Variable, CVCL::Theorem3, CVCL::Theorem, CVCL::StatCounter, CVCL::StatFlag, CVCL::Rational, CVCL::BoolVarExprValue, CVCL::NamedExprValue, CVCL::ExprClosure, CVCL::ExprApply, CVCL::ExprCC, CVCL::ExprBoundVar, CVCL::ExprVar, CVCL::ExprRational, CVCL::ExprSkolem, CVCL::ExprString, CVCL::ExprNode, CVCL::ExprValue, CVCL::ExprHashMap< Data >, CVCL::ExprHashMap< Data >::iterator, CVCL::ExprMap< Data >, CVCL::ExprMap< Data >::iterator, CVCL::Expr, CVCL::Expr::iterator, CVCL::DebugTimer, CVCL::DebugCounter, CVCL::DebugFlag, CVCL::Clause, CVCL::CDMapOrdered< Key, Data >::orderedIterator, CVCL::CDMapOrdered< Key, Data >::iterator, CVCL::CDMap< Key, Data, HashFcn >::orderedIterator, CVCL::CDMap< Key, Data, HashFcn >::iterator, CVCL::AssumptionsValue, CVCL::Assumptions, CVCL::Assumptions::iterator, CVCL::Rational::Impl, CVCL::DebugTime
• operator> : CVCL::Rational, CVCL::Expr, CVCL::DebugTimer, CVCL::Rational::Impl, CVCL::DebugTime
• operator>= : CVCL::Rational, CVCL::Expr, CVCL::DebugTimer, CVCL::Rational::Impl, CVCL::DebugTime
• operator[]() : CVCL::Hash_Table< _Key, _Data >, CVCL::Dict< _Key, _Data >, CVCL::Type, CVCL::ExprHashMap< Data >, CVCL::ExprMap< Data >, CVCL::Expr, CVCL::CLFlags, CVCL::Clause, CVCL::CDMapOrdered< Key, Data >, CVCL::CDMap< Key, Data, HashFcn >, CVCL::CDList< T >, CVCL::Assumptions
• operator||() : CVCL::Expr
• orCNFRule() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• orConcat() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• orConst() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• orderedBegin() : CVCL::CDMapOrdered< Key, Data >, CVCL::CDMap< Key, Data, HashFcn >
• orderedEnd() : CVCL::CDMapOrdered< Key, Data >, CVCL::CDMap< Key, Data, HashFcn >
• orderedIterator() : CVCL::CDMapOrdered< Key, Data >::orderedIterator, CVCL::CDMap< Key, Data, HashFcn >::orderedIterator
• orExpr() : CVCL::VCL, CVCL::ValidityChecker, CVCL::Expr
• orFlatten() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• orOne() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• OrToIte() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• orZero() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• os() : CVCL::ExprStream
• overflow() : std::fdoutbuf
• owners() : CVCL::Clause

- p -

• pad() : CVCL::BitvectorTheoremProducer, CVCL::TheoryBitvector
• padBVLTRule() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• padBVMult() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• padBVPlus() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules, CVCL::TheoryBitvector
• parseExpr() : CVCL::VCL, CVCL::ValidityChecker, CVCL::TheoryCore, CVCL::Theory
• parseExprOp() : CVCL::TheoryUF, CVCL::TheoryRecords, CVCL::TheoryQuant, CVCL::TheoryDatatype, CVCL::TheoryCore, CVCL::TheoryBitvector, CVCL::TheoryArray, CVCL::TheoryArith, CVCL::Theory
• parseExprTop() : CVCL::TheoryCore
• Parser() : CVCL::Parser
• ParserException() : CVCL::ParserException
• ParserTemp() : CVCL::ParserTemp
• parseType() : CVCL::VCL, CVCL::ValidityChecker
• pbSize : std::fdinbuf
• pickIntEqMonomial() : CVCL::TheoryArith
• pickMonomial() : CVCL::TheoryArith
• plus() : CVCL::RefinedArithTheoremProducer
• plusExpr() : CVCL::VCL, CVCL::ValidityChecker
• plusPredicate() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• pointer : CVCL::_Hashtable_const_iterator< _Key, _Data >, CVCL::_Hashtable_iterator< _Key, _Data >
• pointerHash() : CVCL::ExprValue
• pop() : CVCL::VCL, CVCL::ValidityChecker, CVCL::ExprStream, CVCL::ContextManager, CVCL::Context
• popDag() : CVCL::ExprStream
• popdag : CVCL::ExprStream
• popDecision() : CVCL::DecisionEngine
• popIndent() : CVCL::ExprStream
• popSave : CVCL::ExprStream
• popScope() : CVCL::VCL, CVCL::ValidityChecker
• popTo() : CVCL::DecisionEngine
• popto() : CVCL::VCL, CVCL::ValidityChecker, CVCL::ContextManager, CVCL::Context
• poptoScope() : CVCL::VCL, CVCL::ValidityChecker
• postponeGC() : CVCL::VariableManager, CVCL::ExprManager
• powExpr() : CVCL::VCL, CVCL::ValidityChecker
• preprocess() : CVCL::TheoryCore
• PrettyPrinter() : CVCL::PrettyPrinter
• PrettyPrinterCore() : CVCL::PrettyPrinterCore
• prevScope() : CVCL::Scope
• print() : CVCL::PrettyPrinterCore, CVCL::TheoryUF, CVCL::TheorySimulate, CVCL::TheoryRecords, CVCL::TheoryQuant, CVCL::TheoryDatatype, CVCL::TheoryCore, CVCL::TheoryBitvector, CVCL::TheoryArray, CVCL::TheoryArith, CVCL::Theory, CVCL::Theorem3, CVCL::Theorem, CVCL::Rational, CVCL::PrettyPrinter, CVCL::Expr, CVCL::Assumptions
• Print() : CVCL::Hash_Table< _Key, _Data >, CVCL::Hash_Entry< _Key, _Data >
• printAll() : CVCL::Statistics, CVCL::Debug
• printDebug() : CVCL::Theorem3, CVCL::Theorem
• printDepth() : CVCL::ExprManager
• printExpr() : CVCL::VCL, CVCL::ValidityChecker
• printStatistics() : CVCL::VCL, CVCL::ValidityChecker
• printStats() : CVCL::Rational
• printV() : CVCL::VCL, CVCL::ValidityChecker
• printx() : CVCL::Theorem3, CVCL::Theorem
• processBuffer() : CVCL::TheoryArith
• processCommands() : CVCL::VCCmd
• processCond() : CVCL::TheoryCore
• processConflict() : CVCL::SearchEngineFast
• processEquality() : CVCL::TheoryCore
• processFactQueue() : CVCL::TheoryCore
• processFiniteInterval() : CVCL::TheoryArith
• processFiniteIntervals() : CVCL::TheoryArith
• processIntEq() : CVCL::TheoryArith
• processRealEq() : CVCL::TheoryArith
• processResult() : CVCL::SearchEngine
• processSimpleIntEq() : CVCL::TheoryArith
• projectInequalities() : CVCL::TheoryArith
• prompt : CVCL::ParserTemp
• prompt1 : CVCL::ParserTemp
• prompt2 : CVCL::ParserTemp
• Proof() : CVCL::Proof
• proofByContradiction() : CVCL::SearchEngineTheoremProducer, CVCL::SearchEngineRules
• propagate() : CVCL::SearchEngineFast, CVCL::Circuit
• propAndrAF() : CVCL::SearchEngineTheoremProducer, CVCL::SearchEngineRules
• propAndrAT() : CVCL::SearchEngineTheoremProducer, CVCL::SearchEngineRules
• propAndrLF() : CVCL::SearchEngineTheoremProducer, CVCL::SearchEngineRules
• propAndrLRT() : CVCL::SearchEngineTheoremProducer, CVCL::SearchEngineRules
• propAndrRF() : CVCL::SearchEngineTheoremProducer, CVCL::SearchEngineRules
• propIffr() : CVCL::SearchEngineTheoremProducer, CVCL::SearchEngineRules
• propIterIfThen() : CVCL::SearchEngineTheoremProducer, CVCL::SearchEngineRules
• propIterIte() : CVCL::SearchEngineTheoremProducer, CVCL::SearchEngineRules
• propIterThen() : CVCL::SearchEngineTheoremProducer, CVCL::SearchEngineRules
• proves() : CVCL::Theorem
• Proxy() : CVCL::ExprHashMap< Data >::iterator::Proxy, CVCL::ExprMap< Data >::iterator::Proxy, CVCL::Expr::iterator::Proxy, CVCL::CDMapOrdered< Key, Data >::orderedIterator::Proxy, CVCL::CDMapOrdered< Key, Data >::iterator::Proxy, CVCL::CDMap< Key, Data, HashFcn >::orderedIterator::Proxy, CVCL::CDMap< Key, Data, HashFcn >::iterator::Proxy, CVCL::Assumptions::iterator::Proxy
• push() : CVCL::VCL, CVCL::ValidityChecker, CVCL::ExprStream, CVCL::ContextManager, CVCL::Context
• push_back() : CVCL::CDList< T >
• pushdag : CVCL::ExprStream
• pushDag() : CVCL::ExprStream
• pushDecision() : CVCL::DecisionEngine
• pushIndent() : CVCL::ExprStream
• pushNegation() : CVCL::TheoryCore
• pushNegationRec() : CVCL::TheoryCore
• pushRestore : CVCL::ExprStream
• pushScope() : CVCL::VCL, CVCL::ValidityChecker

- q -

• QuantTheoremProducer() : CVCL::QuantTheoremProducer
• query() : CVCL::VCL, CVCL::ValidityChecker
• queryTCC() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules

- r -

• rat() : CVCL::BitvectorTheoremProducer, CVCL::RefinedArithTheoremProducer, CVCL::ArithTheoremProducer, CVCL::TheoryBitvector, CVCL::TheoryArith
• ratExpr() : CVCL::VCL, CVCL::ValidityChecker
• Rational() : CVCL::Rational
• readArrayLiteral() : CVCL::ArrayTheoremProducer, CVCL::ArrayProofRules
• readExpr() : CVCL::VCL, CVCL::ValidityChecker
• realShadow() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• realShadowEq() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• realType() : CVCL::ArithTheoremProducer, CVCL::VCL, CVCL::ValidityChecker, CVCL::TheoryArith
• realUsed() : CVCL::TheoryArith
• rebuild() : CVCL::BVTypePredExpr, CVCL::BoolVarExprValue, CVCL::ExprClosure, CVCL::ExprApply, CVCL::ExprSkolem, CVCL::ExprNode, CVCL::ExprValue, CVCL::ExprManager, CVCL::Expr
• rebuildExpr() : CVCL::ExprValue, CVCL::ExprManager
• rebuildExprs() : CVCL::ExprValue
• rebuildRec() : CVCL::ExprManager
• RecField() : CVCL::RecField
• recFindBoundVars() : CVCL::QuantTheoremProducer
• recInstantiate() : CVCL::TheoryQuant
• recordExpr() : CVCL::RecordsTheoremProducer, CVCL::VCL, CVCL::ValidityChecker, CVCL::TheoryRecords
• recordFact() : CVCL::SearchEngineFast
• recordSelect() : CVCL::RecordsTheoremProducer, CVCL::TheoryRecords
• RecordsTheoremProducer() : CVCL::RecordsTheoremProducer
• recordType() : CVCL::RecordsTheoremProducer, CVCL::VCL, CVCL::ValidityChecker, CVCL::TheoryRecords
• recordUpdate() : CVCL::RecordsTheoremProducer, CVCL::TheoryRecords
• recSelectExpr() : CVCL::VCL, CVCL::ValidityChecker
• recUpdateExpr() : CVCL::VCL, CVCL::ValidityChecker
• recursiveMap() : CVCL::TheoryQuant
• recursivePrint() : CVCL::Theorem
• RefCDO() : CVCL::SmartCDO< T >::RefCDO< U >
• RefCDO<U> : CVCL::SmartCDO< T >::RefCDO< U >::RefNotifyObj
• reference : CVCL::_Hashtable_const_iterator< _Key, _Data >, CVCL::_Hashtable_iterator< _Key, _Data >
• refineCounterExample() : CVCL::TheoryCore, CVCL::TheoryArith, CVCL::Theory
• RefinedArithTheoremProducer() : CVCL::RefinedArithTheoremProducer
• reflexivityRule() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• ReflexivityTheoremValue : CVCL::ReflexivityTheoremValue, CVCL::TheoremValue
• RefNotifyObj : CVCL::SmartCDO< T >::RefCDO< U >::RefNotifyObj, CVCL::SmartCDO< T >::RefCDO< U >
• refutes() : CVCL::Theorem
• registerKinds() : CVCL::Theory
• registerPrettyPrinter() : CVCL::ExprManager
• registerSubclass() : CVCL::ExprManager
• registerTheory() : CVCL::Theory
• relToClosure() : CVCL::UFTheoremProducer, CVCL::UFProofRules
• relTrans() : CVCL::UFTheoremProducer, CVCL::UFProofRules
• remove() : CVCL::NotifyList
• removeFromNotify() : CVCL::Expr
• renameExpr() : CVCL::TheoryArray
• replaceITE() : CVCL::SearchEngine
• replaceITErec() : CVCL::SearchEngine
• reset() : CVCL::ExprStream, CVCL::DebugTimer, CVCL::DebugTime
• Reset() : CVCL::Hash_Ptr< _Key, _Data >, CVCL::Dict_Ptr< _Key, _Data >
• resetDag() : CVCL::ExprStream
• resetIndent() : CVCL::ExprStream
• Resize() : CVCL::Hash_Table< _Key, _Data >
• resolveID() : CVCL::Theory
• restart() : CVCL::VCL, CVCL::ValidityChecker, CVCL::SearchSimple, CVCL::SearchEngineFast, CVCL::SearchEngine
• restartThm() : CVCL::SearchEngine
• restore() : CVCL::ContextObjChain, CVCL::Scope
• restoreData() : CVCL::NotifyList, CVCL::ContextObj, CVCL::CDO< T >, CVCL::CDMapOrdered< Key, Data >, CVCL::CDMapOrderedData, CVCL::CDOmapOrdered< Key, Data >, CVCL::CDMap< Key, Data, HashFcn >, CVCL::CDMapData, CVCL::CDOmap< Key, Data, HashFcn >, CVCL::CDList< T >
• restoreIndent() : CVCL::ExprManager
• resumeGC() : CVCL::VariableManager, CVCL::ExprManager
• rewrite() : CVCL::TheoryUF, CVCL::TheorySimulate, CVCL::TheoryRecords, CVCL::TheoryDatatype, CVCL::TheoryCore, CVCL::TheoryBitvector, CVCL::TheoryArray, CVCL::TheoryArith, CVCL::Theory
• REWRITE_NORMAL : CVCL::Expr
• rewriteAnd() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• rewriteAtomic() : CVCL::TheoryBitvector, CVCL::Theory
• rewriteAux() : CVCL::TheoryRecords
• rewriteBoolean() : CVCL::TheoryBitvector
• rewriteBV() : CVCL::TheoryBitvector
• rewriteCC() : CVCL::Theory
• rewriteConst() : CVCL::TheoryBitvector
• rewriteConstDef() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• rewriteCore() : CVCL::TheoryCore, CVCL::Theory
• rewriteIff() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• rewriteImplies() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• rewriteIte() : CVCL::TheoryCore
• rewriteIteBool() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• rewriteIteElse() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• rewriteIteFalse() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• rewriteIteSame() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• rewriteIteThen() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• rewriteIteToAnd() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• rewriteIteToIff() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• rewriteIteToImp() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• rewriteIteToNot() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• rewriteIteToOr() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• rewriteIteTrue() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• rewriteLetDecl() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• rewriteLitCore() : CVCL::TheoryCore
• rewriteLiteral() : CVCL::TheoryCore, CVCL::Theory
• rewriteLitSelect() : CVCL::RecordsTheoremProducer, CVCL::RecordsProofRules
• rewriteLitUpdate() : CVCL::RecordsTheoremProducer, CVCL::RecordsProofRules
• rewriteNotAnd() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• rewriteNotExists() : CVCL::QuantTheoremProducer, CVCL::QuantProofRules, CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• rewriteNotFalse() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• rewriteNotForall() : CVCL::QuantTheoremProducer, CVCL::QuantProofRules, CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• rewriteNotIff() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• rewriteNotIte() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• rewriteNotNot() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• rewriteNotOr() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• rewriteNotTrue() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• rewriteOpDef() : CVCL::UFTheoremProducer, CVCL::UFProofRules
• rewriteOr() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• rewriteReadWrite() : CVCL::ArrayTheoremProducer, CVCL::ArrayProofRules
• rewriteRedundantWrite1() : CVCL::ArrayTheoremProducer, CVCL::ArrayProofRules
• rewriteRedundantWrite2() : CVCL::ArrayTheoremProducer, CVCL::ArrayProofRules
• rewriteReflexivity() : CVCL::CommonTheoremProducer, CVCL::CommonProofRules
• rewriteSameStore() : CVCL::ArrayTheoremProducer, CVCL::ArrayProofRules
• rewriteThm() : CVCL::Theory
• rewriteUpdateSelect() : CVCL::RecordsTheoremProducer, CVCL::RecordsProofRules
• rewriteUsingSymmetry() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• rewriteWriteWrite() : CVCL::ArrayTheoremProducer, CVCL::ArrayProofRules
• rightMinusLeft() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• rightShiftToConcat() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• RWTheoremValue : CVCL::RWTheoremValue, CVCL::TheoremValue

- s -

• s : CVCL::CLFlag
• s_charHash : CVCL::ExprValue
• s_intHash : CVCL::ExprValue
• s_nextIdx : CVCL::VCL::UserAssertion
• sameKidCheck() : CVCL::BitvectorTheoremProducer
• sat() : CVCL::Clause
• Scope : CVCL::Scope, CVCL::ContextObj, CVCL::ContextObjChain
• scopeLevel() : CVCL::VCL, CVCL::ValidityChecker, CVCL::SearchEngine, CVCL::Debug, CVCL::ContextManager
• ScopeWatcher() : CVCL::ScopeWatcher
• score() : CVCL::VariableValue, CVCL::Literal, CVCL::Variable
• SearchEngine() : CVCL::SearchEngine
• SearchEngineFast() : CVCL::SearchEngineFast
• SearchEngineTheoremProducer() : CVCL::SearchEngineTheoremProducer
• SearchNotifyObj : CVCL::SearchEngine::SearchNotifyObj, CVCL::SearchEngine
• SearchSimple() : CVCL::SearchSimple
• selectLargest() : CVCL::TheoryArith::VarOrderGraph
• selectSmallest() : CVCL::TheoryArith::VarOrderGraph
• separateMonomial() : CVCL::TheoryArith
• set() : CVCL::SmartCDO< T >, CVCL::CDO< T >, CVCL::CDOmapOrdered< Key, Data >, CVCL::CDOmap< Key, Data, HashFcn >
• Set_Next_Hash_Entry() : CVCL::Hash_Ptr< _Key, _Data >
• setAssumpThm() : CVCL::VariableValue, CVCL::Variable
• setCachedValue() : CVCL::TheoremValue, CVCL::Theorem
• setConst() : CVCL::Assumptions
• setCurrentTime() : CVCL::Debug
• setElapsed() : CVCL::Debug
• setExpandFlag() : CVCL::TheoremValue, CVCL::Theorem
• setFind() : CVCL::Expr
• setFindLiteral() : CVCL::TheoryCore
• setFlag() : CVCL::TheoremValue, CVCL::Theorem, CVCL::Expr, CVCL::CLFlags
• setIncomplete() : CVCL::TheoryCore, CVCL::Theory
• setInconsistent() : CVCL::TheoryCore, CVCL::Theory, CVCL::SearchEngineFast
• setIndex() : CVCL::ExprValue
• setIsAtomicFlag() : CVCL::Expr
• setLitFlag() : CVCL::TheoremValue, CVCL::Theorem
• setMessage() : CVCL::Exception
• setNull() : CVCL::NotifyList, CVCL::ContextObj, CVCL::CDO< T >, CVCL::CDMapOrdered< Key, Data >, CVCL::CDMapOrderedData, CVCL::CDOmapOrdered< Key, Data >, CVCL::CDMap< Key, Data, HashFcn >, CVCL::CDMapData, CVCL::CDOmap< Key, Data, HashFcn >, CVCL::CDList< T >
• setOS() : CVCL::Debug
• setPrompt1() : CVCL::ParserTemp
• setPrompt2() : CVCL::ParserTemp
• setRep() : CVCL::ExprCC, CVCL::ExprValue, CVCL::Expr
• setResourceLimit() : CVCL::VCL, CVCL::ValidityChecker, CVCL::TheoryCore, CVCL::Theory
• setRestorePoint() : CVCL::SearchEngineFast::ConflictClauseManager
• setRewriteNormal() : CVCL::Expr
• setSig() : CVCL::ExprCC, CVCL::ExprValue, CVCL::Expr
• setSimpCache() : CVCL::Expr
• setSimpFrom() : CVCL::ExprValue, CVCL::Expr
• setSubtypePred() : CVCL::Expr
• setTCC() : CVCL::Expr
• setType() : CVCL::Expr
• setup() : CVCL::TheoryUF, CVCL::TheoryRecords, CVCL::TheoryQuant, CVCL::TheoryDatatype, CVCL::TheoryCore, CVCL::TheoryBitvector, CVCL::TheoryArray, CVCL::TheoryArith, CVCL::Theory
• setupCC() : CVCL::Theory
• setupExpr() : CVCL::TheoryBitvector
• setupRec() : CVCL::TheoryArith
• setupTerm() : CVCL::TheoryCore, CVCL::Theory
• setValue() : CVCL::VariableValue, CVCL::Literal, CVCL::Variable
• simplifiedMultExpr() : CVCL::ArithTheoremProducer
• simplify() : CVCL::VCL, CVCL::ValidityChecker, CVCL::TheoryCore, CVCL::Theory, CVCL::SearchEngine
• simplifyExpr() : CVCL::Theory
• simplifyInPlaceThmRec() : CVCL::TheoryCore
• simplifyOp() : CVCL::TheoryCore, CVCL::Theory
• simplifyThm() : CVCL::VCL, CVCL::ValidityChecker, CVCL::TheoryCore, CVCL::Theory
• simplifyThm2() : CVCL::VCL, CVCL::ValidityChecker
• simulateExpr() : CVCL::VCL, CVCL::ValidityChecker
• SimulateTheoremProducer() : CVCL::SimulateTheoremProducer
• size() : CVCL::Hash_Table< _Key, _Data >, CVCL::NotifyList, CVCL::ExprHashMap< Data >, CVCL::ExprMap< Data >, CVCL::Clause, CVCL::CDMapOrdered< Key, Data >, CVCL::CDMap< Key, Data, HashFcn >, CVCL::CDList< T >, CVCL::AssumptionsValue, CVCL::Assumptions
• skolemExpr() : CVCL::Expr
• skolemize() : CVCL::SearchEngineTheoremProducer, CVCL::TheoryCore, CVCL::Theory, CVCL::SearchEngine
• skolemizeAx() : CVCL::VCCmd
• skolemizeRewrite() : CVCL::SearchEngineTheoremProducer, CVCL::SearchEngineRules
• skolemizeRewriteVar() : CVCL::SearchEngineTheoremProducer, CVCL::SearchEngineRules
• SmartCDO : CVCL::SmartCDO< T >, CVCL::SmartCDO< T >::RefCDO< U >
• SmtlibException() : CVCL::SmtlibException
• solve() : CVCL::TheoryCore, CVCL::TheoryBitvector, CVCL::TheoryArray, CVCL::TheoryArith, CVCL::Theory
• solvedForm() : CVCL::TheoryArith
• soundError() : CVCL::TheoremProducer
• SoundException() : CVCL::SoundException
• space : CVCL::ExprStream
• split() : CVCL::SearchEngineFast
• splitGrayShadow() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• Splitter() : CVCL::SearchEngine::Splitter
• stackLevel() : CVCL::VCL, CVCL::ValidityChecker
• StatCounter() : CVCL::StatCounter
• StatCounterMap : CVCL::Statistics
• StatFlag() : CVCL::StatFlag
• StatFlagMap : CVCL::Statistics
• StaticFlagsEnum : CVCL::Expr
• Statistics() : CVCL::Statistics
• std::endl : CVCL::ExprStream
• strict() : CVCL::TheoryArith::FreeConst
• stringExpr() : CVCL::VCL, CVCL::ValidityChecker
• subExprOf() : CVCL::Expr
• subrangeType() : CVCL::VCL, CVCL::ValidityChecker, CVCL::TheoryArith
• subst() : CVCL::RefinedArithTheoremProducer
• substAndCanonize() : CVCL::TheoryArith
• substExpr : CVCL::Expr
• substitute() : CVCL::ArithTheoremProducer, CVCL::TheoryCore
• substitutivityRule() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• subtypePredicate() : CVCL::TheoryCore, CVCL::Theory
• subtypeType() : CVCL::VCL, CVCL::ValidityChecker
• sumModM() : CVCL::ArithTheoremProducer
• sumMulF() : CVCL::ArithTheoremProducer
• sv : CVCL::CLFlag
• switchContext() : CVCL::ContextManager
• symm() : CVCL::RefinedArithTheoremProducer
• symmetryRule() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• sys_flags : args
• sys_params : args

- t -

• tcc() : CVCL::VCL::UserAssertion
• TCMapPair : CVCL::TheoryUF
• Theorem : CVCL::Theorem, CVCL::ReflexivityTheoremValue, CVCL::RWTheoremValue, CVCL::TheoremValue
• Theorem3 : CVCL::Theorem3, CVCL::Theorem
• TheoremManager() : CVCL::TheoremManager
• TheoremProducer : CVCL::TheoremProducer, CVCL::Theorem3, CVCL::Theorem
• TheoremValue() : CVCL::TheoremValue
• Theory : CVCL::Theory, CVCL::TheoryCore
• TheoryArith() : CVCL::TheoryArith
• TheoryArray() : CVCL::TheoryArray
• TheoryBitvector() : CVCL::TheoryBitvector
• TheoryBitvector::bitBlastIneqn() : CVCL::TheoryBitvector
• TheoryCore : CVCL::TheoryCore, CVCL::Theory
• theoryCore() : CVCL::CNF, CVCL::VCL, CVCL::Theory, CVCL::Debug
• TheoryDatatype() : CVCL::TheoryDatatype
• theoryOf() : CVCL::Theory
• TheoryQuant() : CVCL::TheoryQuant
• TheoryRecords() : CVCL::TheoryRecords
• TheorySimulate() : CVCL::TheorySimulate
• TheorySimulate::parseExprOp() : CVCL::TheorySimulate
• TheoryUF() : CVCL::TheoryUF
• theoryUsed() : CVCL::TheoryArith, CVCL::Theory
• thm() : CVCL::VCL::UserAssertion
• timer() : CVCL::Debug
• TimerMap : CVCL::Debug
• topScope() : CVCL::Context, CVCL::Scope
• toString() : CVCL::BitvectorException, CVCL::ArithException, CVCL::TheoremValue, CVCL::Literal, CVCL::Variable, CVCL::TypecheckException, CVCL::Type, CVCL::Theorem3, CVCL::Theorem, CVCL::SoundException, CVCL::SmtlibException, CVCL::Rational, CVCL::Proof, CVCL::ParserException, CVCL::Op, CVCL::Expr, CVCL::Exception, CVCL::EvalException, CVCL::DebugException, CVCL::CLException, CVCL::CompactClause, CVCL::Clause, CVCL::AssumptionsValue, CVCL::Assumptions, CVCL::Rational::Impl
• trace() : CVCL::Debug
• traceAll() : CVCL::Debug
• traceConflict() : CVCL::SearchEngineFast
• traceFlag() : CVCL::Debug
• track_use_of_memory : args
• trans() : CVCL::RefinedArithTheoremProducer
• transClosureExpr() : CVCL::TheoryUF
• transformDiseq() : CVCL::TheoryCore
• transitivityRule() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• traverseDiseq() : CVCL::TheoryCore
• trueExpr : CVCL::VCL, CVCL::ValidityChecker, CVCL::Theory, CVCL::ExprManager, CVCL::Expr
• trueTheorem() : CVCL::Theory
• tupleExpr() : CVCL::RecordsTheoremProducer, CVCL::VCL, CVCL::ValidityChecker, CVCL::TheoryRecords
• TupleIndex() : CVCL::TupleIndex
• tupleSelect() : CVCL::RecordsTheoremProducer, CVCL::TheoryRecords
• tupleSelectExpr() : CVCL::VCL, CVCL::ValidityChecker
• tupleType() : CVCL::RecordsTheoremProducer, CVCL::VCL, CVCL::ValidityChecker, CVCL::TheoryRecords
• tupleUpdate() : CVCL::RecordsTheoremProducer, CVCL::TheoryRecords
• tupleUpdateExpr() : CVCL::VCL, CVCL::ValidityChecker
• Type() : CVCL::Type
• typeBool() : CVCL::Type
• TypecheckException() : CVCL::TypecheckException
• typeMap : CVCL::TheoryQuant
• typePred() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• typePredBit() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules

- u -

• UFTheoremProducer() : CVCL::UFTheoremProducer
• uminusExpr() : CVCL::VCL, CVCL::ValidityChecker
• uMinusToMult() : CVCL::RefinedArithTheoremProducer, CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• underflow() : std::fdinbuf
• uniqueID() : CVCL::ParserTemp
• unitProp() : CVCL::SearchEngineTheoremProducer, CVCL::SearchEngineRules
• unitPropagation() : CVCL::SearchEngineFast
• universalInst() : CVCL::QuantTheoremProducer, CVCL::QuantProofRules
• unregisterPrettyPrinter() : CVCL::ExprManager
• update() : CVCL::TheoryUF, CVCL::TheoryRecords, CVCL::TheoryQuant, CVCL::TheoryDatatype, CVCL::TheoryCore, CVCL::TheoryBitvector, CVCL::TheoryArray, CVCL::TheoryArith, CVCL::Theory, CVCL::ContextObj
• updateCC() : CVCL::Theory
• updateHelper() : CVCL::Theory
• updateLitCounts() : CVCL::SearchEngineFast
• updateLitScores() : CVCL::SearchEngineFast
• updateStats() : CVCL::TheoryArith
• updateSubsumptionDB() : CVCL::TheoryArith
• UserAssertion() : CVCL::VCL::UserAssertion

- v -

• Val() : CVCL::Hash_Entry< _Key, _Data >
• VALID_IS_ATOMIC : CVCL::Expr
• validIsAtomicFlag() : CVCL::Expr
• ValidityChecker() : CVCL::ValidityChecker
• validSimpCache() : CVCL::Expr
• varExpr() : CVCL::VCL, CVCL::ValidityChecker
• Variable : CVCL::Variable, CVCL::VariableManager, CVCL::VariableValue
• VariableManager : CVCL::VariableManager, CVCL::VariableValue
• VariableManagerNotifyObj() : CVCL::VariableManagerNotifyObj
• VariableValue : CVCL::VariableValue, CVCL::VariableManager
• VariableValueSet : CVCL::VariableManager
• varIntroRule() : CVCL::CommonTheoremProducer, CVCL::Theory, CVCL::CommonProofRules
• varIntroSkolem() : CVCL::TheoryCore, CVCL::Theory, CVCL::SearchEngine
• varOnLHS() : CVCL::TheoryArith::Ineq
• varOnRHS() : CVCL::TheoryArith::Ineq
• vc : CVCL::ParserTemp
• VCCmd() : CVCL::VCCmd
• vcl : CVCL::RefinedArithTheoremProducer
• VCL() : CVCL::VCL
• verifyConflict() : CVCL::SearchEngineTheoremProducer

- w -

• wasAsserted() : CVCL::SearchEngineFast, CVCL::SearchEngine
• watched() : CVCL::Clause
• withAssumptions() : CVCL::TheoremProducer, CVCL::TheoremManager, CVCL::Theorem3, CVCL::Theorem
• withIndentation() : CVCL::ExprManager
• withProof() : CVCL::TheoremProducer, CVCL::TheoremManager, CVCL::Theorem3, CVCL::Theorem
• wp() : CVCL::Literal, CVCL::Variable, CVCL::SearchEngineFast, CVCL::Clause
• writeExpr() : CVCL::VCL, CVCL::ValidityChecker

- x -

• xsputn() : std::fdoutbuf

- z -

• zero : CVCL::RefinedArithTheoremProducer
• zeroCoeffBVMult() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules
• zeroPaddingRule() : CVCL::BitvectorTheoremProducer, CVCL::BitvectorProofRules

- ~ -

• ~ArithException() : CVCL::ArithException
• ~ArithProofRules() : CVCL::ArithProofRules
• ~ArrayProofRules() : CVCL::ArrayProofRules
• ~Assumptions() : CVCL::Assumptions
• ~BitvectorException() : CVCL::BitvectorException
• ~BitvectorProofRules() : CVCL::BitvectorProofRules
• ~BitvectorTheoremProducer() : CVCL::BitvectorTheoremProducer
• ~CDList() : CVCL::CDList< T >
• ~CDMap() : CVCL::CDMap< Key, Data, HashFcn >
• ~CDMapOrdered() : CVCL::CDMapOrdered< Key, Data >
• ~CDO() : CVCL::CDO< T >
• ~CDOmap() : CVCL::CDOmap< Key, Data, HashFcn >
• ~CDOmapOrdered() : CVCL::CDOmapOrdered< Key, Data >
• ~Clause() : CVCL::Clause
• ~ClauseOwner() : CVCL::ClauseOwner
• ~ClauseValue() : CVCL::ClauseValue
• ~CLException() : CVCL::CLException
• ~CLFlag() : CVCL::CLFlag
• ~CommonProofRules() : CVCL::CommonProofRules
• ~CommonTheoremProducer() : CVCL::CommonTheoremProducer
• ~Context() : CVCL::Context
• ~ContextManager() : CVCL::ContextManager
• ~ContextNotifyObj() : CVCL::ContextNotifyObj
• ~ContextObj() : CVCL::ContextObj
• ~ContextObjChain() : CVCL::ContextObjChain
• ~DatatypeProofRules() : CVCL::DatatypeProofRules
• ~Debug() : CVCL::Debug
• ~DebugCounter() : CVCL::DebugCounter
• ~DebugFlag() : CVCL::DebugFlag
• ~DebugTimer() : CVCL::DebugTimer
• ~DecisionEngine() : CVCL::DecisionEngine
• ~DecisionEngineCaching() : CVCL::DecisionEngineCaching
• ~DecisionEngineDFS() : CVCL::DecisionEngineDFS
• ~DecisionEngineMBTF() : CVCL::DecisionEngineMBTF
• ~Dict() : CVCL::Dict< _Key, _Data >
• ~Dict_Entry() : CVCL::Dict_Entry< _Key, _Data >
• ~EvalException() : CVCL::EvalException
• ~Exception() : CVCL::Exception
• ~Expr() : CVCL::Expr
• ~ExprApply() : CVCL::ExprApply
• ~ExprBoundVar() : CVCL::ExprBoundVar
• ~ExprCC() : CVCL::ExprCC
• ~ExprClosure() : CVCL::ExprClosure
• ~ExprGeneric() : CVCL::ExprGeneric
• ~ExprGrayShadow() : CVCL::ExprGrayShadow
• ~ExprManager() : CVCL::ExprManager
• ~ExprNode() : CVCL::ExprNode
• ~ExprRational() : CVCL::ExprRational
• ~ExprRecord() : CVCL::ExprRecord
• ~ExprSkolem() : CVCL::ExprSkolem
• ~ExprStream() : CVCL::ExprStream
• ~ExprString() : CVCL::ExprString
• ~ExprValue() : CVCL::ExprValue
• ~ExprVar() : CVCL::ExprVar
• ~Hash_Entry() : CVCL::Hash_Entry< _Key, _Data >
• ~Hash_Table() : CVCL::Hash_Table< _Key, _Data >
• ~Impl() : CVCL::Rational::Impl
• ~iterator() : CVCL::Assumptions::iterator
• ~MemoryManager() : CVCL::MemoryManager
• ~MemoryManagerChunks() : CVCL::MemoryManagerChunks
• ~MemoryManagerMalloc() : CVCL::MemoryManagerMalloc
• ~Op() : CVCL::Op
• ~Parser() : CVCL::Parser
• ~ParserException() : CVCL::ParserException
• ~PrettyPrinter() : CVCL::PrettyPrinter
• ~QuantProofRules() : CVCL::QuantProofRules
• ~Rational() : CVCL::Rational
• ~RecField() : CVCL::RecField
• ~RecordsProofRules() : CVCL::RecordsProofRules
• ~RefCDO() : CVCL::SmartCDO< T >::RefCDO< U >
• ~ReflexivityTheoremValue() : CVCL::ReflexivityTheoremValue
• ~RWTheoremValue() : CVCL::RWTheoremValue
• ~Scope() : CVCL::Scope
• ~ScopeWatcher() : CVCL::ScopeWatcher
• ~SearchEngine() : CVCL::SearchEngine
• ~SearchEngineFast() : CVCL::SearchEngineFast
• ~SearchEngineRules() : CVCL::SearchEngineRules
• ~SearchEngineTheoremProducer() : CVCL::SearchEngineTheoremProducer
• ~SearchSimple() : CVCL::SearchSimple
• ~SimulateProofRules() : CVCL::SimulateProofRules
• ~SimulateTheoremProducer() : CVCL::SimulateTheoremProducer
• ~SmartCDO() : CVCL::SmartCDO< T >
• ~SmtlibException() : CVCL::SmtlibException
• ~SoundException() : CVCL::SoundException
• ~Splitter() : CVCL::SearchEngine::Splitter
• ~StatCounter() : CVCL::StatCounter
• ~StatFlag() : CVCL::StatFlag
• ~Statistics() : CVCL::Statistics
• ~Theorem() : CVCL::Theorem
• ~Theorem3() : CVCL::Theorem3
• ~TheoremManager() : CVCL::TheoremManager
• ~TheoremProducer() : CVCL::TheoremProducer
• ~TheoremValue() : CVCL::TheoremValue
• ~Theory() : CVCL::Theory
• ~TheoryArith() : CVCL::TheoryArith
• ~TheoryArray() : CVCL::TheoryArray
• ~TheoryBitvector() : CVCL::TheoryBitvector
• ~TheoryCore() : CVCL::TheoryCore
• ~TheoryDatatype() : CVCL::TheoryDatatype
• ~TheoryQuant() : CVCL::TheoryQuant
• ~TheoryRecords() : CVCL::TheoryRecords
• ~TheorySimulate() : CVCL::TheorySimulate
• ~TheoryUF() : CVCL::TheoryUF
• ~TupleIndex() : CVCL::TupleIndex
• ~TypecheckException() : CVCL::TypecheckException
• ~UFProofRules() : CVCL::UFProofRules
• ~ValidityChecker() : CVCL::ValidityChecker
• ~Variable() : CVCL::Variable
• ~VariableManager() : CVCL::VariableManager
• ~VariableValue() : CVCL::VariableValue
• ~VCCmd() : CVCL::VCCmd
• ~VCL() : CVCL::VCL

---