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

- d -

• d_active : CVCL::TheoremManager
• d_added : CVCL::VariableValue
• d_allInstCount : CVCL::TheoryQuant
• d_ante : CVCL::VariableValue
• d_anteIdx : CVCL::VariableValue
• d_anyType : CVCL::TheoryUF
• d_applicationsInModel : CVCL::TheoryUF, CVCL::TheoryArray
• d_applyCNFRulesCache : CVCL::SearchImplBase
• d_assump : CVCL::TheoremValue, CVCL::VariableValue
• d_assumptions : CVCL::SearchImplBase
• 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_boolExtractCacheFlag : CVCL::TheoryBitvector
• d_bottomLevel : CVCL::DecisionEngineMBTF, CVCL::DecisionEngineCaching
• d_bottomScope : CVCL::SearchSat, CVCL::SearchImplBase, CVCL::Context, SAT::CNF_Manager
• d_boundVarStack : CVCL::TheoryCore
• d_buffer : CVCL::TheoryArith
• d_bufferIdx : CVCL::TheoryArith
• d_bufferThres : CVCL::TheoryArith
• d_bv32Flag : CVCL::TheoryBitvector
• 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_bvPlusCarryCacheLeftBV : CVCL::TheoryBitvector
• d_bvPlusCarryCacheRightBV : 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_cache : CVCL::DecisionEngineMBTF, CVCL::DecisionEngineCaching, CVCL::TheoryArith::VarOrderGraph
• d_cachedValue : CVCL::TheoremValue
• d_callThisRound : CVCL::TheoryQuant
• 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_clauseIdNext : SAT::CNF_Manager
• d_clauselit : CVCL::TheoremValue
• d_clauses : CVCL::SearchEngineFast
• d_clausesQueryEnd : CVCL::SearchEngineFast
• d_clausesQueryStart : CVCL::SearchEngineFast
• d_clean_time : CVCL::DebugTimer
• d_cm : CVCL::SearchSatTheoryAPI, CVCL::VCL, CVCL::VariableManager, CVCL::TheoryCore, CVCL::TheoremManager, CVCL::ExprManager, CVCL::Context
• d_cnf : SAT::DPLLTBasic
• d_cnfBitBlastFlag : CVCL::TheoryBitvector
• d_cnfCache : CVCL::SearchImplBase
• d_cnfManager : CVCL::SearchSat
• d_cnfOption : CVCL::TheoryCore, CVCL::SearchImplBase
• d_cnfStack : SAT::DPLLTBasic
• d_cnfVars : CVCL::SearchImplBase, SAT::CNF_Manager
• d_col : CVCL::ExprStream
• d_commonRules : CVCL::SearchEngineTheoremProducer, CVCL::Theory, CVCL::SearchEngine, CVCL::ExprTransform, SAT::CNF_Manager
• 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_convertToDiff : CVCL::Translator, CVCL::TheoryArith
• d_core : CVCL::TypeComputerCore, CVCL::PrettyPrinterCore, CVCL::CoreTheoremProducer, CVCL::DecisionEngine, CVCL::SearchEngine, CVCL::ExprTransform
• d_coreSatAPI : CVCL::TheoryCore, CVCL::SearchSat
• d_coreSatAPI_implBase : CVCL::SearchImplBase
• 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, SAT::CNF_Formula
• d_currentRecursiveSimplifier : CVCL::TheoryCore
• 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_datatypes : CVCL::TheoryDatatype
• d_decider : CVCL::SearchSat, SAT::DPLLT
• 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_dpllt : CVCL::SearchSat
• d_dplltReady : CVCL::SearchSat
• d_dpSplitters : CVCL::SearchImplBase
• d_dump : CVCL::VCL
• d_dumpFileOpen : CVCL::VCL
• d_dumpName : CVCL::Debug
• d_dynamicFlags : CVCL::ExprValue
• d_e : CVCL::Expr::iterator::Proxy
• d_edges : CVCL::TheoryArith::VarOrderGraph
• d_elist : CVCL::NotifyList
• d_em : CVCL::RefinedArithTheoremProducer, CVCL::VCL, CVCL::Theory, CVCL::TheoremProducer, CVCL::TheoremManager, CVCL::ExprValue, CVCL::ExprStream, CVCL::ExprManagerNotifyObj, CVCL::ExprManager::HashEV
• d_emptyVec : CVCL::ExprManager
• d_endChunk : CVCL::MemoryManagerChunks
• d_enqueueCNFCache : CVCL::SearchImplBase
• d_eq : CVCL::TheoryBitvector
• d_eqBlastIdx : CVCL::TheoryBitvector
• d_eqIdx : CVCL::TheoryBitvector
• d_equalityQueue : CVCL::TheoryCore
• d_equivCheckMMidx : CVCL::TheoryCore
• d_expand : CVCL::TheoremValue
• d_expr : CVCL::ReflexivityTheoremValue, CVCL::DecisionEngineMBTF::CacheEntry, CVCL::DecisionEngineCaching::CacheEntry, CVCL::VariableValue, CVCL::Type, CVCL::Op, CVCL::Expr
• d_exprSet : CVCL::ExprManager
• d_exprTrans : CVCL::TheoryCore
• d_factQueue : CVCL::SearchEngineFast
• d_facts : CVCL::TheoryDatatype
• d_false : CVCL::ExprManager
• 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::TheoryCore, CVCL::TheoremManager, CVCL::Statistics, CVCL::Debug, CVCL::CDFlags
• d_formula : SAT::CD_CNF_Formula, SAT::CNF_Formula_Impl
• d_freeConstDB : CVCL::TheoryArith
• d_freeList : CVCL::MemoryManagerChunks
• d_funApplications : CVCL::TheoryUF
• d_funApplicationsIdx : CVCL::TheoryUF
• d_globals : CVCL::TheoryCore
• d_goal : CVCL::SearchSimple
• d_graph : 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, SAT::Clause
• d_idCounter : CVCL::ExprStream
• d_idx : CVCL::VCL::UserAssertion, CVCL::ExprSkolem
• d_idxUserAssump : CVCL::SearchSat
• d_ifLiftOption : CVCL::SearchImplBase
• d_ignoreCnfVarsOption : CVCL::SearchImplBase
• d_impliedLiterals : CVCL::TheoryCore
• d_impliedLiteralsIdx : CVCL::TheoryCore
• d_inCheckSAT : CVCL::SearchEngineFast
• d_inCheckSat : CVCL::SearchSat
• 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, SAT::Lit, SAT::Var
• 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_instRound : CVCL::TheoryQuant
• d_insts : CVCL::TheoryQuant
• d_instThisRound : CVCL::TheoryQuant
• d_intAssumptions : CVCL::SearchSat
• d_intConstUsed : CVCL::TheoryArith
• d_intType : CVCL::TheoryArith
• d_intUsed : CVCL::TheoryArith
• d_isAssump : 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_iteLiftArith : CVCL::Translator
• d_iteMap : SAT::CNF_Manager
• d_key : CVCL::CDOmapOrdered< Key, Data >, CVCL::CDOmap< Key, Data, HashFcn >
• d_kind : CVCL::ExprValue, CVCL::Op
• d_kindMap : CVCL::ExprManager
• d_kindMapByName : CVCL::ExprManager
• d_labels : CVCL::TheoryDatatype
• d_lang : CVCL::ExprStream
• d_langUsed : CVCL::TheoryArith
• d_lastCheck : CVCL::SearchSat
• d_lastClosure : CVCL::VCL
• d_lastConflictClause : CVCL::SearchEngineFast
• d_lastConflictScope : CVCL::SearchEngineFast
• d_lastCounterExample : CVCL::SearchImplBase
• d_lastDagSize : CVCL::ExprStream
• d_lastQuery : CVCL::VCL
• d_lastQueryTCC : CVCL::VCL
• d_lastRegisteredVar : CVCL::SearchSat
• d_lastValid : CVCL::SearchSat, CVCL::SearchImplBase
• d_lemmas : CVCL::SearchSat
• d_lemmasNext : CVCL::SearchSat
• 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::SearchImplBase::Splitter
• d_literals : CVCL::SearchEngineFast, CVCL::ClauseValue
• d_literalSet : CVCL::SearchEngineFast
• d_lits : SAT::CNF_Formula_Impl, SAT::Clause, 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_MMIndex : CVCL::BVConstExpr
• d_mng : SAT::DPLLTBasic
• d_mngStack : SAT::DPLLTBasic
• d_modified : CVCL::CLFlag
• d_msg : CVCL::Exception
• d_n : CVCL::Rational::Impl, CVCL::Rational
• d_name : CVCL::Theory, CVCL::SearchSimple, CVCL::SearchSat, CVCL::SearchEngineFast, CVCL::ExprBoundVar, CVCL::ExprSymbol, 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_nextIdx : CVCL::VCL
• d_nextImpliedLiteral : CVCL::SearchSat
• 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::ExprManager
• d_notifyObjList : CVCL::Context
• d_nullExpr : CVCL::ExprManager
• d_num : CVCL::Rational::Impl
• d_numVars : SAT::CD_CNF_Formula, SAT::CNF_Formula_Impl
• d_opExpr : CVCL::ExprApply
• d_origFormulaOption : CVCL::SearchImplBase
• d_os : CVCL::Statistics, CVCL::ExprStream, CVCL::Debug
• d_osdump : CVCL::VCL
• d_osdumpFile : CVCL::VCL
• d_osDumpTrace : CVCL::Debug
• d_osdumpTranslate : CVCL::VCL
• d_osdumpTranslateFile : 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_parent : CVCL::ExprStream
• d_parser : CVCL::VCCmd
• d_pfOp : CVCL::TheoremProducer
• d_pointerHash : CVCL::ExprManager
• d_popScopes : SAT::DPLLTBasic
• 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_printStats : SAT::DPLLTBasic
• d_processIndex : CVCL::TheoryDatatypeLazy
• d_processQueue : CVCL::TheoryDatatypeLazy
• d_processQueueKind : CVCL::TheoryDatatypeLazy
• d_proof : CVCL::TheoremValue, CVCL::Proof
• d_pushNegationFlag : CVCL::TheoryBitvector
• d_pushNegCache : CVCL::TheoryBitvector, CVCL::ExprTransform
• d_quant : CVCL::ExprSkolem
• d_queue : CVCL::TheoryCore
• d_queueSE : CVCL::TheoryCore
• d_r : CVCL::TheoryArith::FreeConst, CVCL::ExprRational
• d_rank : CVCL::DecisionEngineMBTF::CacheEntry, CVCL::DecisionEngineCaching::CacheEntry
• d_reach : CVCL::TheoryDatatype
• d_reads : CVCL::TheoryArray
• d_ready : SAT::DPLLTBasic
• 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::ExprNode
• d_replaceITECache : CVCL::SearchImplBase
• 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_restorer : CVCL::SearchSat
• d_rewriteFlag : CVCL::TheoryBitvector
• d_rhs : CVCL::RWTheoremValue, CVCL::TheoryArith::Ineq
• d_rootLits : CVCL::SearchSat
• d_rules : CVCL::VariableManager, CVCL::TheoryUF, CVCL::TheorySimulate, CVCL::TheoryRecords, CVCL::TheoryQuant, CVCL::TheoryDatatype, CVCL::TheoryCore, CVCL::TheoryBitvector, CVCL::TheoryArray, CVCL::TheoryArith, CVCL::TheoremManager, CVCL::SearchEngine, CVCL::ExprTransform, SAT::CNF_Manager
• d_rwBitBlastFlag : CVCL::TheoryBitvector
• d_rwmm : CVCL::TheoremManager
• d_sat : CVCL::ClauseValue
• d_satisfied : SAT::Clause
• 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::CoreSatAPI_implBase, CVCL::DecisionEngine, CVCL::VCL, CVCL::SearchEngineFast::ConflictClauseManager
• d_selectorMap : CVCL::TheoryDatatype
• 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::ExprNode
• 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_skolem_axioms : CVCL::CommonTheoremProducer
• d_skolemized_thms : CVCL::CommonTheoremProducer
• d_skolemVars : CVCL::CommonTheoremProducer
• d_smartSplits : CVCL::TheoryDatatype
• d_solver : CVCL::TheoryCore
• d_splitterAsserted : CVCL::TheoryDatatype
• d_splitterCount : CVCL::DecisionEngine, CVCL::SearchEngineFast
• d_splitters : CVCL::DecisionEngine, CVCL::TheoryDatatype
• d_splittersIndex : CVCL::TheoryDatatype
• d_ss : CVCL::SearchSatDecider, CVCL::SearchSatTheoryAPI, CVCL::SearchSatCoreSatAPI, CVCL::SearchSat::Restorer
• d_staleDB : CVCL::TheoryBitvector
• d_startLevel : CVCL::DecisionEngineMBTF, CVCL::DecisionEngineCaching
• d_statistics : CVCL::VCL, CVCL::TheoryCore
• 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_tccs : CVCL::TheoryBitvector
• d_tccsIdx : CVCL::TheoryBitvector
• d_terms : CVCL::TheoryCore
• d_testerMap : CVCL::TheoryDatatype
• d_theorems : CVCL::SearchSat, SAT::CNF_Manager
• d_theories : CVCL::VCL, CVCL::TheoryCore
• d_theoryAPI : CVCL::SearchSat, SAT::DPLLT
• d_theoryArith : CVCL::ArithTheoremProducer, CVCL::VCL, CVCL::Translator
• 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::QuantTheoremProducer, CVCL::VCL
• d_theoryRecords : CVCL::RecordsTheoremProducer, CVCL::VCL
• d_theorySimulate : CVCL::VCL
• d_theoryUF : CVCL::UFTheoremProducer, CVCL::VCL
• d_theoryUsed : CVCL::Theory
• 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::TheoryCore, 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_transClosureMap : CVCL::TheoryUF
• d_translate : CVCL::VCL
• d_translateFileOpen : CVCL::VCL
• d_translateQueueFlags : SAT::CNF_Manager
• d_translateQueueThms : SAT::CNF_Manager
• d_translateQueueVars : SAT::CNF_Manager
• d_translator : 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::ExprValue
• d_typeComplete : CVCL::TheoryDatatypeLazy
• d_typeComputer : CVCL::TheoryCore, CVCL::ExprManager
• d_typeExprMap : CVCL::TheoryQuant
• d_typeKinds : CVCL::ExprManager
• d_typePredAsserted : CVCL::TheoryCore
• d_typePredsCache : CVCL::TheoryBitvector
• d_uid : CVCL::ParserTemp, CVCL::ExprBoundVar
• d_unit : SAT::Clause
• d_unitConflictClauses : CVCL::SearchEngineFast
• d_unitPropCount : CVCL::SearchEngineFast
• d_univs : CVCL::TheoryQuant
• d_univsContextPos : CVCL::TheoryQuant
• d_univsPosFull : CVCL::TheoryQuant
• d_univsSavedPos : CVCL::TheoryQuant
• d_univsTriggers : CVCL::TheoryQuant
• d_unreportedLits : CVCL::SearchEngineFast
• d_unreportedLitsHandled : CVCL::SearchEngineFast
• d_update_data : CVCL::TheoryCore
• d_update_thms : CVCL::TheoryCore
• d_updateFlag : CVCL::TheoryBitvector
• d_useAtomSem : CVCL::TheoryQuant
• d_useEnqueueFact : CVCL::SearchEngineFast
• d_useLazyInst : CVCL::TheoryQuant
• d_useNew : CVCL::TheoryQuant
• d_userAssertions : CVCL::VCL
• d_userAssumptions : CVCL::SearchSat
• d_useSemMatch : CVCL::TheoryQuant
• d_val : CVCL::VariableValue, CVCL::Variable, CVCL::Assumptions
• d_var : CVCL::Literal
• d_varAssignments : CVCL::TheoryCore
• d_varInfo : SAT::CNF_Manager
• d_varModelMap : CVCL::TheoryCore
• d_vars : CVCL::VCL, CVCL::TheoryCore, CVCL::SearchSat, CVCL::ExprClosure
• d_varSet : CVCL::VariableManager
• d_vc : CVCL::VCCmd
• d_vector : CVCL::AssumptionsValue
• d_visited : CVCL::DecisionEngine
• d_vm : CVCL::VariableManagerNotifyObj, CVCL::VariableValue, CVCL::SearchImplBase
• d_withAssump : CVCL::TheoremManager
• d_withIndentation : CVCL::ExprManager
• d_withProof : CVCL::TheoremManager
• d_wp : CVCL::VariableValue, CVCL::ClauseValue
• d_zeroVar : CVCL::TheoryArith
• 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
• datatypeTestExpr() : 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
• decide_next_branch() : CSolver
• Decider() : SAT::DPLLT::Decider
• decider() : SAT::DPLLT
• decision_strategy : CSolverParameters
• DecisionEngine : CVCL::DecisionEngine, CVCL::SearchImplBase
• DecisionEngineCaching() : CVCL::DecisionEngineCaching
• DecisionEngineDFS() : CVCL::DecisionEngineDFS
• DecisionEngineMBTF() : CVCL::DecisionEngineMBTF
• decompose() : CVCL::DatatypeTheoremProducer, CVCL::DatatypeProofRules
• decRefcount() : CVCL::ExprValue
• deduce() : CSolver
• Delete() : CVCL::Hash_Table< _Key, _Data >, CVCL::Dict< _Key, _Data >
• delete_unrelevant_clauses() : CSolver
• DeleteClause() : SatSolver
• 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 >
• detail_dump_cl() : CDatabase
• 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
• direction() : CLitPoolElement
• DisableClauseDeletion() : Xchaff, SatSolver
• diseqToIneq() : CVCL::ArithTheoremProducer, CVCL::ArithProofRules
• distribL() : CVCL::RefinedArithTheoremProducer
• distribR() : CVCL::RefinedArithTheoremProducer
• divideDef() : CVCL::RefinedArithTheoremProducer
• divideExpr() : CVCL::VCL, CVCL::ValidityChecker
• dlevel() : CSolver, CVariable
• done : CVCL::Parser, CVCL::ParserTemp
• doSolve() : CVCL::TheoryArith
• DPLLT() : SAT::DPLLT
• DPLLTBasic::DPLLTBasic() : SAT::DPLLTBasic
• dummyTheorem() : CVCL::DatatypeTheoremProducer, CVCL::DatatypeProofRules
• dump() : CSolver, CDatabase, CVariable, CClause, CLitPoolElement
• dump_assignment_stack() : CSolver
• dumpTrace() : CVCL::Debug
• DynamicFlagsEnum : CVCL::Expr

---