- d -

• d_active : CVC3::ContextObj , CVC3::TheoremManager
• d_activity : MiniSat::Solver
• d_added : CVC3::VariableValue
• d_all_multTrigsInfo : CVC3::TheoryQuant
• d_allInstCount : CVC3::TheoryQuant
• d_allInsts : CVC3::TheoryQuant
• d_allmap_trigs : CVC3::TheoryQuant
• d_allout : CVC3::TheoryQuant
• d_alltrig_list : CVC3::TheoryQuant
• d_analyze_redundant : MiniSat::Solver
• d_analyze_seen : MiniSat::Solver
• d_analyze_stack : MiniSat::Solver
• d_ante : CVC3::VariableValue
• d_anteIdx : CVC3::VariableValue
• d_applicationsInModel : CVC3::TheoryUF , CVC3::TheoryArray
• d_applyCNFRulesCache : CVC3::SearchImplBase
• d_arithUsed : CVC3::Translator
• d_arrayIndic : CVC3::TheoryQuant
• d_arrayTrigs : CVC3::TheoryQuant
• d_assertions : SAT::DPLLTBasic
• d_assertionsStack : SAT::DPLLTBasic
• d_assigns : MiniSat::Solver
• d_assump : CVC3::VariableValue , CVC3::RegTheoremValue , CVC3::RWTheoremValue
• d_assumptions : CVC3::SearchImplBase
• d_ax : CVC3::Translator
• d_basicModelVars : CVC3::TheoryCore
• d_beginningOfLine : CVC3::ExprStream
• d_berkminFlag : CVC3::SearchEngineFast
• d_bestByExpr : CVC3::DecisionEngine
• d_bindHistory : CVC3::TheoryQuant
• d_bitvecCache : CVC3::TheoryBitvector
• d_body : CVC3::ExprClosure
• d_bool : CVC3::ExprManager
• d_booleanRWFlag : CVC3::TheoryBitvector
• d_boolExtractCacheFlag : CVC3::TheoryBitvector
• d_bottomLevel : CVC3::DecisionEngineCaching , CVC3::DecisionEngineMBTF
• d_bottomScope : CVC3::SearchImplBase , SAT::CNF_Manager , CVC3::SearchSat , CVC3::Context
• d_boundVarMap : CVC3::TheoryCore
• d_boundVarStack : CVC3::TheoryCore
• d_buffer : CVC3::TheoryArithNew , CVC3::TheoryArithOld
• d_bufferIdx : CVC3::TheoryArithNew , CVC3::TheoryArithOld
• d_bufferThres : CVC3::TheoryArithNew , CVC3::TheoryArithOld
• d_bv32Flag : CVC3::TheoryBitvector
• d_bvAssertDiseq : CVC3::TheoryBitvector
• d_bvAssertEq : CVC3::TheoryBitvector
• d_bvBitBlastDiseq : CVC3::TheoryBitvector
• d_bvBitBlastEq : CVC3::TheoryBitvector
• d_bvconst : CVC3::BVConstExpr
• d_bvConstExprIndex : CVC3::TheoryBitvector
• d_bvDelayDiseq : CVC3::TheoryBitvector
• d_bvDelayEq : CVC3::TheoryBitvector
• d_bvDelayTypePreds : CVC3::TheoryBitvector
• d_bvOne : CVC3::TheoryBitvector , CVC3::BitvectorTheoremProducer
• d_bvParameterExprIndex : CVC3::TheoryBitvector
• d_bvPlusCarryCacheLeftBV : CVC3::TheoryBitvector
• d_bvPlusCarryCacheRightBV : CVC3::TheoryBitvector
• d_bvPlusExprIndex : CVC3::TheoryBitvector
• d_bvplusRewriteFlag : CVC3::TheoryBitvector
• d_bvTypePredExprIndex : CVC3::TheoryBitvector
• d_bvTypePreds : CVC3::TheoryBitvector
• d_bvZero : CVC3::TheoryBitvector , CVC3::BitvectorTheoremProducer
• d_cache : CVC3::TheoryArithNew::VarOrderGraph , CVC3::DecisionEngineCaching , CVC3::DecisionEngineMBTF , CVC3::TheoryArithNew::VarOrderGraph , CVC3::TheoryArithOld::VarOrderGraph
• d_cachedValue : CVC3::TheoremValue
• d_cachedValues : CVC3::TheoremManager
• d_cacheTheorem : CVC3::TheoryQuant
• d_cacheThmPos : CVC3::TheoryQuant
• d_callThisRound : CVC3::TheoryQuant
• d_category : CVC3::Translator
• d_cdmap : CDOmap< Expr, FreeConst > , CVC3::CDOmap< Key, Data, HashFcn > , CVC3::CDOmapOrdered< Key, Data > , CDOmap< Key, Data, HashFcn > , CDOmap< Key, Data, HashFcn > new , CDOmap< Key, Data, HashFcn > new true CDOmap< Key, Data, HashFcn > , CDOmapOrdered< Key, Data > , CDOmapOrdered< Key, Data > new CDOmapOrdered< Key, Data >
• d_cdo : CVC3::SmartCDO< T >::RefCDO< U > , RefCDO< U >
• d_checkProofs : CVC3::TheoremProducer
• d_children : CVC3::ExprNode , CVC3::ExprNodeTmp
• d_chunkList : CVC3::ContextMemoryManager , CVC3::MemoryManagerChunks
• d_chunkSize : CVC3::MemoryManagerChunks
• d_chunkSizeBytes : CVC3::ContextMemoryManager , CVC3::MemoryManagerChunks
• d_circuitPropCount : CVC3::SearchEngineFast
• d_circuits : CVC3::SearchEngineFast
• d_circuitsByExpr : CVC3::SearchEngineFast
• d_cla_decay : MiniSat::Solver
• d_cla_inc : MiniSat::Solver
• d_clause : CVC3::Clause , CVC3::ClauseOwner , CVC3::CompactClause
• d_clauseID : MiniSat::PushEntry
• d_clauseIDCounter : MiniSat::Solver
• d_clauseIdNext : SAT::CNF_Manager
• d_clauselit : CVC3::TheoremValue
• d_clauses : CVC3::SearchEngineFast , MiniSat::Derivation , MiniSat::Solver
• d_clausesQueryEnd : CVC3::SearchEngineFast
• d_clausesQueryStart : CVC3::SearchEngineFast
• d_clean_time : CVC3::DebugTimer
• d_clock : CVC3::DebugTime
• d_cm : CVC3::TheoryCore , CVC3::ExprManager , CVC3::Context , CVC3::VariableManager , CVC3::TheoremManager , CVC3::VCL , CVC3::SearchSatTheoryAPI , SAT::DPLLTBasic
• d_cmm : CVC3::Scope
• d_cmmStack : CVC3::Context
• d_cnf : SAT::DPLLTBasic
• d_cnfBitBlastFlag : CVC3::TheoryBitvector
• d_cnfCache : CVC3::SearchImplBase
• d_cnfCallback : SAT::CNF_Manager , CVC3::SearchSat
• d_cnfManager : CVC3::SearchSat
• d_cnfOption : CVC3::SearchImplBase
• d_cnfStack : SAT::DPLLTBasic
• d_cnfVars : SAT::CNF_Manager , CVC3::SearchImplBase
• d_col : CVC3::ExprStream
• d_combineAssump : CVC3::Translator
• d_commonRules : CVC3::SearchEngine , SAT::CNF_Manager , CVC3::Theory , CVC3::ExprTransform , CVC3::SearchEngineTheoremProducer
• d_concatRewriteFlag : CVC3::TheoryBitvector
• d_conflict : MiniSat::Solver
• d_conflictClauseCount : CVC3::SearchEngineFast
• d_conflictClauseManager : CVC3::SearchEngineFast
• d_conflictClauses : CVC3::SearchEngineFast
• d_conflictClauseStack : CVC3::SearchEngineFast
• d_conflictCount : CVC3::SearchEngineFast
• d_conflictTheorem : CVC3::SearchEngineFast
• d_const : CVC3::TheoryArithNew::Ineq , CVC3::TheoryArithOld::Ineq
• d_context : iterator , CDMap< Expr, bool > , CDMap< Expr, CDList< dynTrig > , iterator , CVC3::Scope , CVC3::CDMap< Key, Data, HashFcn > , CVC3::ContextNotifyObj , CDMap< Key, Data, HashFcn > , CDMapOrdered< Key, Data > , CVC3::CDMapOrdered< Key, Data > , iterator , CDMap< Expr, Theorem > , iterator
• d_contextCache : CVC3::TheoryQuant
• d_contextMap : CVC3::TheoryQuant
• d_contexts : CVC3::ContextManager
• d_contextTerms : CVC3::TheoryQuant
• d_convertArith : CVC3::Translator
• d_convertArray : CVC3::Translator
• d_convertToDiff : CVC3::Translator
• d_core : CVC3::SearchEngine , CVC3::ExprTransform , CVC3::DecisionEngine , CVC3::CoreTheoremProducer , CVC3::TypeComputerCore , CVC3::PrettyPrinterCore
• d_coreSatAPI : CVC3::TheoryCore , CVC3::SearchSat
• d_coreSatAPI_implBase : CVC3::SearchImplBase
• d_count : CVC3::VariableValue
• d_counter : CVC3::StatCounter , CVC3::DebugCounter
• d_counters : CVC3::Statistics , CVC3::Debug
• d_countLeft : CVC3::TheoryArithNew , CVC3::TheoryArithOld
• d_countPrev : CVC3::VariableValue
• d_countRight : CVC3::TheoryArithNew , CVC3::TheoryArithOld
• d_curContext : CVC3::ContextManager
• d_curMaxExprScore : CVC3::TheoryQuant
• d_currDepth : CVC3::ExprStream
• d_current : SAT::CNF_Formula
• d_currentRecursiveSimplifier : CVC3::TheoryCore
• d_dag : CVC3::ExprStream
• d_dagBuilt : CVC3::ExprStream
• d_dagMap : CVC3::ExprStream
• d_dagPrinting : CVC3::ExprManager
• d_dagPtr : CVC3::ExprStream
• d_dagStack : CVC3::ExprStream
• d_data : CVC3::CDOmap< Key, Data, HashFcn > , CDOmap< Expr, FreeConst > , CVC3::Parser , CVC3::CDO< T > , CVC3::CLFlag , CVC3::ContextObjChain , CVC3::SmartCDO< T > , CVC3::CDOmapOrdered< Key, Data > , CDOmap< Key, Data, HashFcn > , CDOmap< Key, Data, HashFcn > new , CDOmap< Key, Data, HashFcn > new true CDOmap< Key, Data, HashFcn > , CDOmapOrdered< Key, Data > , CDOmapOrdered< Key, Data > new CDOmapOrdered< Key, Data > , CDO< T > , Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey > , CDO< Theorem > , SmartCDO< T >
• d_dataSize : CVC3::MemoryManagerChunks
• d_datatypes : CVC3::TheoryDatatype
• d_decider : CVC3::SearchSat , MiniSat::Solver , SAT::DPLLT
• d_decisionEngine : CVC3::SearchEngineFast , CVC3::SearchSimple
• d_default_params : MiniSat::Solver
• d_delay : CVC3::SmartCDO< T >::RefCDO< U > , RefCDO< U >
• d_deleted : CVC3::VariableManager , CVC3::ClauseValue
• d_depth : CVC3::ExprStream
• d_derivation : MiniSat::Solver
• d_dir : CVC3::ClauseValue
• d_disableGC : CVC3::ExprManager , CVC3::VariableManager
• d_diseq : CVC3::TheoryArithNew , CVC3::TheoryArithOld , CVC3::TheoryBitvector
• d_diseqIdx : CVC3::TheoryArithNew , CVC3::TheoryArithOld , CVC3::TheoryBitvector
• d_dpllt : CVC3::SearchSat
• d_dplltReady : CVC3::SearchSat
• d_dpSplitters : CVC3::SearchImplBase
• d_dump : CVC3::Translator , CVC3::VCL
• d_dumpExprs : CVC3::Translator
• d_dumpFileOpen : CVC3::Translator
• d_dumpName : CVC3::Debug
• d_dynamicFlags : CVC3::ExprValue
• d_e : CVC3::Expr::iterator::Proxy
• d_edges : CVC3::TheoryArithNew::VarOrderGraph , CVC3::TheoryArithOld::VarOrderGraph
• d_elist : CVC3::NotifyList
• d_em : CVC3::ExprManager::HashEV , CVC3::ExprManagerNotifyObj , CVC3::Translator , CVC3::ExprStream , CVC3::VCL , CVC3::TheoremManager , CVC3::TheoremProducer , CVC3::Theory , CVC3::ExprValue
• d_emptyClause : MiniSat::Derivation
• d_emptyVec : CVC3::ExprManager
• d_endChunk : CVC3::ContextMemoryManager , CVC3::MemoryManagerChunks
• d_endChunkStack : CVC3::ContextMemoryManager
• d_enqueueCNFCache : CVC3::SearchImplBase
• d_eq : CVC3::TheoryBitvector
• d_eq_list : CVC3::TheoryQuant
• d_eq_pos : CVC3::TheoryQuant
• d_eqBlastIdx : CVC3::TheoryBitvector
• d_eqIdx : CVC3::TheoryBitvector
• d_eqs : CVC3::TheoryQuant
• d_eqs_pos : CVC3::TheoryQuant
• d_equal : Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >
• d_expand : CVC3::TheoremValue
• d_expandFlags : CVC3::TheoremManager
• d_expensive_ccmin : MiniSat::Solver
• d_expr : CVC3::Expr , CVC3::Type , CVC3::Op , CVC3::VariableValue , CVC3::Theorem , CVC3::DecisionEngineCaching::CacheEntry , CVC3::DecisionEngineMBTF::CacheEntry
• d_expResult : CVC3::Translator
• d_exprLastUpdatedPos : CVC3::TheoryQuant
• d_exprSet : CVC3::ExprManager
• d_exprTrans : CVC3::TheoryCore
• d_extractKey : Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >
• d_factQueue : CVC3::SearchEngineFast
• d_facts : CVC3::TheoryDatatype
• d_false : CVC3::ExprManager
• d_find : CVC3::ExprValue
• d_first : iterator , CDMap< Expr, bool > , CDMap< Expr, CDList< dynTrig > , iterator , CVC3::CDMap< Key, Data, HashFcn > , CDMap< Key, Data, HashFcn > , CDMapOrdered< Key, Data > , CVC3::CDMapOrdered< Key, Data > , iterator , CDMap< Expr, Theorem > , iterator
• d_flag : CVC3::StatFlag , CVC3::TheoremManager , CVC3::ScopeWatcher , CVC3::DebugFlag , CVC3::ExprValue , CVC3::TheoremValue
• d_flagCounter : CVC3::ExprManager
• d_flags : CVC3::TheoryCore , CVC3::CDFlags , CVC3::Statistics , CVC3::TheoremManager , CVC3::VCL , CVC3::Debug
• d_formula : SAT::CNF_Formula_Impl , SAT::CD_CNF_Formula
• d_freeConstDB : CVC3::TheoryArithNew , CVC3::TheoryArithOld
• d_freeList : CVC3::MemoryManagerChunks
• d_fullTrigs : CVC3::TheoryQuant
• d_funApplications : CVC3::TheoryUF
• d_funApplicationsIdx : CVC3::TheoryUF
• d_globals : CVC3::TheoryCore
• d_goal : CVC3::SearchSimple
• d_graph : CVC3::TheoryArithNew , CVC3::TheoryArithOld
• d_hash : CVC3::ExprValue , Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >
• d_hash_table : Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::iterator , Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::const_iterator
• d_hasMoreBVs : CVC3::TheoryQuant
• d_hasTriggers : CVC3::TheoryQuant
• d_height : CVC3::DecisionEngineCaching , CVC3::DecisionEngineMBTF
• d_help : CVC3::CLFlag
• d_hole : CVC3::TheoremProducer
• d_id : CVC3::Context , SAT::Clause
• d_idCounter : CVC3::ExprStream
• d_idx : CVC3::VCL::UserAssertion , CVC3::ExprSkolem
• d_idxUserAssump : CVC3::SearchSat
• d_ifLiftOption : CVC3::SearchImplBase
• d_ignoreCnfVarsOption : CVC3::SearchImplBase
• d_impliedLiterals : CVC3::TheoryCore
• d_impliedLiteralsIdx : CVC3::TheoryCore
• d_inAddFact : CVC3::TheoryCore
• d_inCheckSAT : CVC3::SearchEngineFast
• d_inCheckSat : CVC3::SearchSat
• d_inCheckSATCore : CVC3::TheoryCore
• d_incomplete : CVC3::TheoryCore
• d_inconsistent : CVC3::TheoryCore
• d_incThm : CVC3::TheoryCore
• d_indent : CVC3::ExprManager , CVC3::ExprStream
• d_indentLast : CVC3::ExprStream
• d_indentReg : CVC3::ExprStream
• d_indentStack : CVC3::ExprStream
• d_indentTransient : CVC3::ExprManager
• d_index : CVC3::ExprManager , SAT::Var , SAT::Lit , CVC3::ExprValue , CVC3::DecisionEngineCaching , CVC3::DecisionEngineMBTF
• d_index1 : CVC3::TheoryBitvector , CVC3::TheoryArithNew
• d_indexChunkList : CVC3::ContextMemoryManager
• d_indexChunkListStack : CVC3::ContextMemoryManager
• d_indexExpr : CVC3::TheoryQuant
• d_indexScore : CVC3::TheoryQuant
• d_inEnd : CVC3::TheoryQuant
• d_ineq : CVC3::TheoryArithNew::Ineq , CVC3::TheoryArithOld::Ineq
• d_inequalitiesLeftDB : CVC3::TheoryArithNew , CVC3::TheoryArithOld
• d_inequalitiesRightDB : CVC3::TheoryArithNew , CVC3::TheoryArithOld
• d_inferences : MiniSat::Derivation
• d_initMaxScore : CVC3::TheoryQuant
• d_inMap : CVC3::CDOmap< Key, Data, HashFcn > , CVC3::CDOmapOrdered< Key, Data > , CDOmapOrdered< Key, Data > , CDOmap< Key, Data, HashFcn > , CDOmap< Expr, FreeConst > , CDOmap< Key, Data, HashFcn > new , CDOmap< Key, Data, HashFcn > new true CDOmap< Key, Data, HashFcn > , CDOmapOrdered< Key, Data > , CDOmapOrdered< Key, Data > new CDOmapOrdered< Key, Data >
• d_inModelCreation : CVC3::TheoryArithNew , CVC3::TheoryArithOld
• d_inputClauses : MiniSat::Derivation
• d_inputLang : CVC3::ExprManager
• d_inRebuild : CVC3::ExprManager
• d_inRegisterAtom : CVC3::TheoryCore
• d_inSearch : MiniSat::Solver
• d_instCount : CVC3::TheoryQuant
• d_instHistory : CVC3::TheoryQuant
• d_instHistoryGlobal : CVC3::TheoryQuant
• d_insts : CVC3::TheoryQuant
• d_instThisRound : CVC3::TheoryQuant
• d_intAssumptions : CVC3::SearchSat
• d_intConstUsed : CVC3::Translator
• d_intIntArray : CVC3::Translator
• d_intIntRealArray : CVC3::Translator
• d_intRealArray : CVC3::Translator
• d_intType : CVC3::TheoryArith
• d_intUsed : CVC3::Translator
• d_isAssump : CVC3::TheoremValue
• d_it : CVC3::Expr::iterator , CVC3::CDMap< Key, Data, HashFcn >::iterator , CVC3::Assumptions::iterator , CVC3::CDMap< Key, Data, HashFcn >::orderedIterator , CVC3::ExprMap< Data >::iterator , CVC3::ExprHashMap< Data >::iterator , CVC3::CDMapOrdered< Key, Data >::orderedIterator , CVC3::CDMapOrdered< Key, Data >::iterator
• d_iteLiftArith : CVC3::Translator
• d_iteMap : SAT::CNF_Manager
• d_key : CDOmap< Expr, FreeConst > , CDOmap< Key, Data, HashFcn > new , CVC3::CDOmapOrdered< Key, Data > , CDOmapOrdered< Key, Data > new CDOmapOrdered< Key, Data > , CDOmapOrdered< Key, Data > , CVC3::CDOmap< Key, Data, HashFcn > , CDOmap< Key, Data, HashFcn > , CDOmapOrdered< Key, Data > , CDOmap< Key, Data, HashFcn > new true CDOmap< Key, Data, HashFcn >
• d_kind : CVC3::Op , CVC3::ExprValue
• d_kindMap : CVC3::ExprManager
• d_kindMapByName : CVC3::ExprManager
• d_labels : CVC3::TheoryDatatype
• d_lang : CVC3::ExprStream
• d_langUsed : CVC3::Translator
• d_lastArrayPos : CVC3::TheoryQuant
• d_lastCheck : CVC3::SearchSat
• d_lastClosure : CVC3::VCL
• d_lastConflictClause : CVC3::SearchEngineFast
• d_lastConflictScope : CVC3::SearchEngineFast
• d_lastCounterExample : CVC3::SearchImplBase
• d_lastDagSize : CVC3::ExprStream
• d_lastPartLevel : CVC3::TheoryQuant
• d_lastPartPredsPos : CVC3::TheoryQuant
• d_lastPartTermsPos : CVC3::TheoryQuant
• d_lastPredsPos : CVC3::TheoryQuant
• d_lastQuery : CVC3::VCL
• d_lastQueryTCC : CVC3::VCL
• d_lastRegisteredVar : CVC3::SearchSat
• d_lastTermsPos : CVC3::TheoryQuant
• d_lastUsefulGtermsPos : CVC3::TheoryQuant
• d_lastValid : CVC3::SearchImplBase , CVC3::SearchSat
• d_learnts : MiniSat::Solver
• d_lemmas : CVC3::SearchSat
• d_lemmasNext : CVC3::SearchSat
• d_level : CVC3::Scope , MiniSat::Solver
• d_lhs : CVC3::RWTheoremValue
• d_lhsMinusRhsFlag : CVC3::TheoryBitvector
• d_liftReadIte : CVC3::TheoryArray
• d_lineWidth : CVC3::ExprManager , CVC3::ExprStream
• d_list : CDList< dynTrig > , vector< Expr > , CDList< size_t > , CDList< size_t > size_t , CVC3::CDList< T > , CDList< T > , CDList< Ineq > , CDList< Theorem > , CDList< Expr > , const_iterator
• d_lit : CVC3::SearchImplBase::Splitter , CVC3::SearchSat::LitPriorityPair
• d_literals : CVC3::SearchEngineFast , CVC3::ClauseValue
• d_literalSet : CVC3::SearchEngineFast
• d_litFlags : CVC3::TheoremManager
• d_lits : CVC3::Circuit , SAT::Clause , SAT::CNF_Formula_Impl
• d_litsAlive : CVC3::SearchEngineFast
• d_litsByScores : CVC3::SearchEngineFast
• d_litsMaxScorePos : CVC3::SearchEngineFast
• d_litSortCount : CVC3::SearchEngineFast
• d_map : iterator , ExprMap< Theorem > , ExprMap< Rational > , ExprMap< int > , ExprMap< CDList< Ineq > , iterator , ExprMap< unsigned > , ExprMap< Polarity > , iterator , ExprMap< ExprMap< vector< dynTrig > , iterator , CDMap< Expr, bool > , CDMap< Key, Data, HashFcn > , iterator , CDMap< Expr, CDList< dynTrig > , CVC3::CLFlags , iterator , CVC3::ExprMap< Data > , CVC3::ExprHashMap< Data > , ExprMap< vector< dynTrig > , iterator , CVC3::VCCmd , CVC3::CDMap< Key, Data, HashFcn > , iterator , CVC3::CDMapOrdered< Key, Data > , iterator , ExprMap< bool > , iterator , ExprMap< Expr > , iterator , CDMapOrdered< Key, Data > , iterator , ExprHashMap< Expr > , iterator , CDMap< Expr, Theorem > , iterator
• d_master : CVC3::ContextObjChain
• d_maxInst : CVC3::TheoryQuant
• d_maxLength : CVC3::TheoryBitvector
• d_maxNaiveCall : CVC3::TheoryQuant
• d_maxQuantInst : CVC3::TheoryQuant
• d_minimizeClauses : SAT::CNF_Manager
• d_mm : CVC3::ExprManager , CVC3::VariableManager , CVC3::TheoremManager
• d_mmFlag : CVC3::ExprManager
• d_MMIndex : CVC3::BVConstExpr
• d_mng : SAT::DPLLTBasic
• d_mngStack : SAT::DPLLTBasic
• d_modified : CVC3::CLFlag
• d_msg : CVC3::Exception
• d_mtrigs_bvorder : CVC3::TheoryQuant
• d_mtrigs_inst : CVC3::TheoryQuant
• d_multitrigs_maps : CVC3::TheoryQuant
• d_multTriggers : CVC3::TheoryQuant
• d_multTrigs : CVC3::TheoryQuant
• d_mybvs : CVC3::TheoryQuant
• d_n : CVC3::Rational
• d_name : CVC3::ExprBoundVar , CVC3::ExprVar , CVC3::SearchEngineFast , CVC3::SearchSat , CVC3::SearchSimple , CVC3::ContextObj , CVC3::Context , CVC3::Theory , CVC3::ExprSymbol
• d_name_of_cur_ctxt : CVC3::VCCmd
• d_neg : CVC3::VariableValue
• d_negAdded : CVC3::VariableValue
• d_negative : CVC3::Literal
• d_negCount : CVC3::VariableValue
• d_negCountPrev : CVC3::VariableValue
• d_negScore : CVC3::VariableValue
• d_negwp : CVC3::VariableValue
• d_newDagMap : CVC3::ExprStream
• d_next : CDOmapOrdered< Key, Data > , CDOmap< Key, Data, HashFcn > new , CDOmap< Expr, FreeConst > , CDOmapOrdered< Key, Data > , CVC3::CDOmapOrdered< Key, Data > , CVC3::CDOmap< Key, Data, HashFcn > , CDOmap< Key, Data, HashFcn > , Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::BucketNode , CDOmapOrdered< Key, Data > new CDOmapOrdered< Key, Data > , CDOmap< Key, Data, HashFcn > new true CDOmap< Key, Data, HashFcn >
• d_nextFree : CVC3::ContextMemoryManager , CVC3::MemoryManagerChunks
• d_nextFreeStack : CVC3::ContextMemoryManager
• d_nextIdx : CVC3::VCL
• d_nextImpliedLiteral : CVC3::SearchSat
• d_nodag : CVC3::ExprStream
• d_node : Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::const_iterator , Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::iterator
• d_nonLiterals : CVC3::SearchEngineFast , CVC3::SearchSimple
• d_nonLiteralsSaved : CVC3::SearchEngineFast
• d_nonlitQueryEnd : CVC3::SearchEngineFast
• d_nonlitQueryStart : CVC3::SearchEngineFast
• d_notifyList : CVC3::ExprValue
• d_notifyObj : CVC3::TheoryCore , CVC3::ExprManager , CVC3::SmartCDO< T >::RefCDO< U > , CVC3::VariableManager , RefCDO< U >
• d_notifyObjList : CVC3::Context
• d_nullExpr : CVC3::ExprManager
• d_numVars : SAT::CD_CNF_Formula , SAT::CNF_Formula_Impl
• d_offset_multi_trig : CVC3::TheoryQuant
• d_ok : MiniSat::Solver
• d_opExpr : CVC3::ExprApplyTmp , CVC3::ExprApply
• d_order : MiniSat::Solver
• d_origFormulaOption : CVC3::SearchImplBase
• d_os : CVC3::Debug , CVC3::Statistics , CVC3::ExprStream
• d_osdump : CVC3::Translator
• d_osdumpFile : CVC3::Translator
• d_osDumpTrace : CVC3::Debug
• d_outputLang : CVC3::ExprManager
• d_pair : CVC3::CDMapOrdered< Key, Data >::orderedIterator::Proxy , CVC3::CDMap< Key, Data, HashFcn >::iterator::Proxy , CVC3::CDMap< Key, Data, HashFcn >::orderedIterator::Proxy , CVC3::ExprMap< Data >::iterator::Proxy , CVC3::ExprHashMap< Data >::iterator::Proxy , CVC3::CDMapOrdered< Key, Data >::iterator::Proxy
• d_parent_list : CVC3::TheoryQuant
• d_parseCache : CVC3::TheoryCore
• d_parser : CVC3::VCCmd
• d_partCalled : CVC3::TheoryQuant
• d_partTriggers : CVC3::TheoryQuant
• d_partTrigs : CVC3::TheoryQuant
• d_pendingClauses : MiniSat::Solver
• d_pendingLemmas : CVC3::SearchSat
• d_pendingLemmasNext : CVC3::SearchSat
• d_pendingLemmasSize : CVC3::SearchSat
• d_pfOp : CVC3::TheoremProducer
• d_pointerHash : CVC3::ExprManager
• d_popLemmas : MiniSat::Solver
• d_popRequests : MiniSat::Solver
• d_postponed : CVC3::ExprManager
• d_postponeGC : CVC3::ExprManager , CVC3::VariableManager
• d_predicates : CVC3::TheoryCore
• d_prettyPrinter : CVC3::ExprManager
• d_prev : CDOmap< Expr, FreeConst > , CDOmapOrdered< Key, Data > new CDOmapOrdered< Key, Data > , CDOmap< Key, Data, HashFcn > , CDOmap< Key, Data, HashFcn > new , CVC3::CDOmap< Key, Data, HashFcn > , CVC3::CDOmapOrdered< Key, Data > , CDOmapOrdered< Key, Data > , CDOmap< Key, Data, HashFcn > new true CDOmap< Key, Data, HashFcn >
• d_prevAStackSize : SAT::DPLLTBasic
• d_prevScope : CVC3::Scope
• d_prevStackSize : SAT::DPLLTBasic
• d_printDepth : CVC3::ExprManager
• d_printer : CVC3::TheoryCore
• d_printStats : SAT::DPLLTBasic , SAT::DPLLTMiniSat
• d_priority : CVC3::SearchSat::LitPriorityPair
• d_prioritySet : CVC3::SearchSat
• d_prioritySetBottomEntries : CVC3::SearchSat
• d_prioritySetBottomEntriesSize : CVC3::SearchSat
• d_prioritySetBottomEntriesSizeStack : CVC3::SearchSat
• d_prioritySetEntries : CVC3::SearchSat
• d_prioritySetEntriesSize : CVC3::SearchSat
• d_prioritySetStart : CVC3::SearchSat
• d_processIndex : CVC3::TheoryDatatypeLazy
• d_processQueue : CVC3::TheoryDatatypeLazy
• d_processQueueKind : CVC3::TheoryDatatypeLazy
• d_proof : CVC3::Proof , CVC3::TheoremValue
• d_pushes : MiniSat::Solver
• d_pushIDs : MiniSat::Solver
• d_pushLevel : SAT::DPLLTBasic
• d_pushNegationFlag : CVC3::TheoryBitvector
• d_pushNegCache : CVC3::ExprTransform , CVC3::TheoryBitvector
• d_qhead : MiniSat::Solver , MiniSat::PushEntry
• d_quant : CVC3::ExprSkolem
• d_quantLevel : CVC3::TheoremValue
• d_queue : CVC3::TheoryCore
• d_queueSE : CVC3::TheoryCore
• d_r : CVC3::TheoryArithNew::FreeConst , CVC3::TheoryArithOld::FreeConst , CVC3::ExprRational
• d_rank : CVC3::DecisionEngineCaching::CacheEntry , CVC3::DecisionEngineMBTF::CacheEntry
• d_rawUnivs : CVC3::TheoryQuant
• d_rawUnivsSavedPos : CVC3::TheoryQuant
• d_reach : CVC3::TheoryDatatype
• d_reads : CVC3::TheoryArray
• d_ready : SAT::DPLLTBasic
• d_readyPrev : SAT::DPLLTBasic
• d_real2int : CVC3::Translator
• d_realType : CVC3::TheoryArith
• d_realUsed : CVC3::Translator
• d_reason : MiniSat::Solver
• d_rebuildCache : CVC3::ExprManager
• d_ref : CVC3::SmartCDO< T >::RefCDO< U >::RefNotifyObj
• d_refcount : CVC3::ClauseValue
• d_refCount : RefCDO< U > , CVC3::SmartCDO< T >::RefCDO< U >
• d_refcount : CVC3::VariableValue , CVC3::ExprValue , CVC3::TheoremValue
• d_refcountOwner : CVC3::ClauseValue
• d_reflFlags : CVC3::TheoremManager
• d_registeredVars : MiniSat::Solver
• d_removedClauses : MiniSat::Derivation
• d_renameThms : CVC3::TheoryArray
• d_rep : CVC3::ExprNode
• d_replaceITECache : CVC3::SearchImplBase
• d_resourceLimit : CVC3::TheoryCore
• d_restore : CVC3::ContextObjChain , CVC3::ContextObj
• d_restoreChain : CVC3::Scope
• d_restoreChainNext : CVC3::ContextObjChain
• d_restoreChainPrev : CVC3::ContextObjChain
• d_restorePoints : CVC3::SearchEngineFast::ConflictClauseManager
• d_restorer : CVC3::SearchSat
• d_rewriteFlag : CVC3::TheoryBitvector
• d_rhs : CVC3::TheoryArithNew::Ineq , CVC3::TheoryArithOld::Ineq , CVC3::RWTheoremValue
• d_rootLevel : MiniSat::Solver
• d_rules : SAT::CNF_Manager , CVC3::TheoryArithNew , CVC3::SearchEngine , CVC3::TheoryQuant , CVC3::TheorySimulate , CVC3::VariableManager , CVC3::TheoryRecords , CVC3::TheoryDatatype , CVC3::TheoryBitvector , CVC3::TheoryUF , CVC3::TheoryArithNew , CVC3::TheoryCore , CVC3::TheoryArray , CVC3::TheoremManager , CVC3::ExprTransform , CVC3::TheoryArithOld
• d_rwBitBlastFlag : CVC3::TheoryBitvector
• d_rwmm : CVC3::TheoremManager
• d_same_head_expr : CVC3::TheoryQuant
• d_sat : CVC3::ClauseValue
• d_satisfied : SAT::Clause
• d_savedCache : CVC3::TheoryQuant
• d_savedMap : CVC3::TheoryQuant
• d_savedTerms : CVC3::TheoryQuant
• d_savedTermsPos : CVC3::TheoryQuant
• d_scope : CVC3::ClauseValue , CVC3::VariableValue , CVC3::ContextObj
• d_scopeLevel : CVC3::TheoremValue
• d_score : CVC3::VariableValue
• d_se : CVC3::SearchEngineFast::ConflictClauseManager , CVC3::VCL , CVC3::CoreSatAPI_implBase , CVC3::DecisionEngine
• d_selectorMap : CVC3::TheoryDatatype
• d_sharedSubterms : CVC3::TheoryBitvector
• d_sharedSubtermsList : CVC3::TheoryBitvector
• d_sharedTerms : CVC3::TheoryArithNew , CVC3::TheoryArithOld
• d_sharedTermsList : CVC3::TheoryArithNew
• d_sharedVars : CVC3::TheoryArithOld , CVC3::TheoryArithNew
• d_sig : CVC3::ExprNode
• d_simpCache : CVC3::ExprValue
• d_simpCacheTag : CVC3::ExprValue
• d_simpCacheTagCurrent : CVC3::ExprManager
• d_simpDB_assigns : MiniSat::Solver
• d_simpDB_props : MiniSat::Solver
• d_simplifiedModelVars : CVC3::TheoryCore
• d_simplifiedThm : CVC3::SearchEngineFast , CVC3::SearchSimple
• d_simplifiedThmQueue : CVC3::TheoryQuant
• d_simplifyInPlace : CVC3::TheoryCore
• d_simpRD_learnts : MiniSat::Solver
• d_simpStack : CVC3::TheoryCore
• d_size : CDList< Ineq > , CDList< T > , CDList< size_t > , CDList< Expr > , const_iterator , vector< Expr > , CDList< Theorem > , CDList< size_t > size_t , CDList< dynTrig > , CVC3::CDList< T > , Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >
• d_skolem_axioms : CVC3::CommonTheoremProducer
• d_skolemized_thms : CVC3::CommonTheoremProducer
• d_skolemVars : CVC3::CommonTheoremProducer
• d_smartSplits : CVC3::TheoryDatatype
• d_solver : CVC3::TheoryCore
• d_solvers : SAT::DPLLTMiniSat
• d_splitterAsserted : CVC3::TheoryDatatype
• d_splitterCount : CVC3::SearchEngineFast , CVC3::DecisionEngine
• d_splitters : CVC3::DecisionEngine , CVC3::TheoryDatatype
• d_splittersIndex : CVC3::TheoryDatatype
• d_ss : CVC3::SearchSat::Restorer , CVC3::SearchSatCNFCallback , CVC3::SearchSatDecider , CVC3::SearchSatCoreSatAPI , CVC3::SearchSatTheoryAPI
• d_stackLevel : CVC3::VCL
• d_staleDB : CVC3::TheoryBitvector
• d_start : MiniSat::Inference
• d_startLevel : CVC3::DecisionEngineCaching , CVC3::DecisionEngineMBTF
• d_statistics : SAT::CNF_Manager , CVC3::VCL , CVC3::TheoryCore
• d_stats : MiniSat::Solver
• d_steps : MiniSat::Inference
• d_str : CVC3::ExprString
• d_strict : CVC3::TheoryArithNew::FreeConst , CVC3::TheoryArithOld::FreeConst
• d_subTermsMap : CVC3::TheoryQuant
• d_t : CVC3::Assumptions::iterator::Proxy
• d_table : iterator , const_iterator , iterator , const_iterator , iterator i CDOmap< Key, Data, HashFcn > , iterator , Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey > , Hash::hash_set< _Key, _HashFcn, _EqualKey >
• d_tcc : CVC3::VCL::UserAssertion
• d_tccCache : CVC3::TheoryCore
• d_tccs : CVC3::TheoryBitvector
• d_tccsIdx : CVC3::TheoryBitvector
• d_tempBinds : CVC3::TheoryQuant
• d_terms : CVC3::TheoryCore
• d_termTheorems : CVC3::TheoryCore
• d_testerMap : CVC3::TheoryDatatype
• d_thead : MiniSat::PushEntry , MiniSat::Solver
• d_theorems : CVC3::SearchSat
• d_theories : CVC3::TheoryCore , CVC3::VCL
• d_theoryAPI : SAT::DPLLT , CVC3::SearchSat , MiniSat::Solver
• d_theoryArith : CVC3::VCL , CVC3::ArithTheoremProducer , CVC3::Translator , CVC3::ArithTheoremProducerOld
• d_theoryArray : CVC3::VCL , CVC3::Translator
• d_theoryBitvector : CVC3::Translator , CVC3::BitvectorTheoremProducer , CVC3::VCL
• d_theoryCore : CVC3::Translator , CVC3::Theory , CVC3::VCL , CVC3::TheoryCore::CoreNotifyObj
• d_theoryDatatype : CVC3::Translator , CVC3::VCL , CVC3::DatatypeTheoremProducer
• d_theoryExplanations : MiniSat::Solver
• d_theoryMap : CVC3::TheoryCore
• d_theoryQuant : CVC3::QuantTheoremProducer , CVC3::Translator , CVC3::VCL
• d_theoryRecords : CVC3::Translator , CVC3::VCL , CVC3::RecordsTheoremProducer
• d_theorySimulate : CVC3::VCL , CVC3::Translator
• d_theoryUF : CVC3::UFTheoremProducer , CVC3::VCL , CVC3::Translator
• d_theoryUsed : CVC3::Theory
• d_thm : CVC3::VariableValue , CVC3::ExprTheorem , CVC3::Theorem3 , CVC3::Circuit , CVC3::Theorem , CVC3::VCL::UserAssertion , CVC3::ClauseValue , CVC3::TheoremValue
• d_time : CVC3::DebugTimer
• d_timers : CVC3::Debug
• d_tlist : CVC3::NotifyList
• d_tm : CVC3::ExprManager , CVC3::TheoremProducer , CVC3::TheoremValue , CVC3::VCL , CVC3::TheoryCore
• d_tmpFile : CVC3::Translator
• d_topLevel : CVC3::DecisionEngineMBTF , CVC3::DecisionEngineCaching
• d_topLevelLock : CVC3::DecisionEngineCaching , CVC3::DecisionEngineMBTF
• d_topScope : CVC3::Context
• d_tp : CVC3::CLFlag
• d_traceFlags : CVC3::Debug
• d_traceOptions : CVC3::Debug
• d_trail : MiniSat::Solver
• d_trail_lim : MiniSat::Solver
• d_trail_pos : MiniSat::Solver , lastToFirst_lt
• d_trailSize : MiniSat::PushEntry
• d_trans2_found : CVC3::TheoryQuant
• d_trans2_num : CVC3::TheoryQuant
• d_trans_back : CVC3::TheoryQuant
• d_trans_forw : CVC3::TheoryQuant
• d_trans_found : CVC3::TheoryQuant
• d_trans_num : CVC3::TheoryQuant
• d_transClosureMap : CVC3::TheoryUF
• d_translate : CVC3::TheoryQuant , CVC3::Translator
• d_translateQueueFlags : SAT::CNF_Manager
• d_translateQueueThms : SAT::CNF_Manager
• d_translateQueueVars : SAT::CNF_Manager
• d_translator : CVC3::VCL , CVC3::TheoryCore
• d_trash : iterator , CDMap< Key, Data, HashFcn > , CVC3::CDMap< Key, Data, HashFcn > , iterator , CDMapOrdered< Key, Data > , iterator , CVC3::CDMapOrdered< Key, Data > , CDMap< Expr, CDList< dynTrig > , iterator , CDMap< Expr, Theorem > , CDMap< Expr, bool >
• d_true : CVC3::ExprManager
• d_trust : CVC3::DecisionEngineMBTF::CacheEntry , CVC3::DecisionEngineCaching::CacheEntry
• d_type : CVC3::ExprValue
• d_typeComplete : CVC3::TheoryDatatypeLazy
• d_typeComputer : CVC3::TheoryCore , CVC3::ExprManager
• d_typeExprMap : CVC3::TheoryQuant
• d_typeKinds : CVC3::ExprManager
• d_typePredsCache : CVC3::TheoryBitvector
• d_UFIDL_ok : CVC3::Translator
• d_uid : CVC3::ExprBoundVar , CVC3::ParserTemp
• d_unit : SAT::Clause
• d_unitClauses : MiniSat::Derivation
• d_unitConflictClauses : CVC3::SearchEngineFast
• d_unitPropCount : CVC3::SearchEngineFast
• d_univs : CVC3::TheoryQuant
• d_univsContextPos : CVC3::TheoryQuant
• d_univsPartSavedPos : CVC3::TheoryQuant
• d_univsPosFull : CVC3::TheoryQuant
• d_univsQueue : CVC3::TheoryQuant
• d_univsSavedPos : CVC3::TheoryQuant
• d_unknown : CVC3::Translator
• d_unreportedLits : CVC3::SearchEngineFast
• d_unreportedLitsHandled : CVC3::SearchEngineFast
• d_update_data : CVC3::TheoryCore
• d_update_thms : CVC3::TheoryCore
• d_useAtomSem : CVC3::TheoryQuant
• d_useEnqueueFact : CVC3::SearchEngineFast
• d_useEqu : CVC3::TheoryQuant
• d_useExprScore : CVC3::TheoryQuant
• d_usefulGterms : CVC3::TheoryQuant
• d_useFullTrig : CVC3::TheoryQuant
• d_useInstAll : CVC3::TheoryQuant
• d_useInstEnd : CVC3::TheoryQuant
• d_useInstGCache : CVC3::TheoryQuant
• d_useInstLCache : CVC3::TheoryQuant
• d_useInstTrue : CVC3::TheoryQuant
• d_useLazyInst : CVC3::TheoryQuant
• d_useMult : CVC3::TheoryQuant
• d_useMultTrig : CVC3::TheoryQuant
• d_useNew : CVC3::TheoryQuant
• d_usePart : CVC3::TheoryQuant
• d_usePartTrig : CVC3::TheoryQuant
• d_usePolarity : CVC3::TheoryQuant
• d_usePullVar : CVC3::TheoryQuant
• d_userAssertions : CVC3::VCL
• d_userAssumptions : CVC3::SearchSat
• d_useSemMatch : CVC3::TheoryQuant
• d_useTrans : CVC3::TheoryQuant
• d_useTrans2 : CVC3::TheoryQuant
• d_useTrigLoop : CVC3::TheoryQuant
• d_useTrigNew : CVC3::TheoryQuant
• d_val : CVC3::Variable , CVC3::VariableValue
• d_value : Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::BucketNode
• d_var : CVC3::Literal
• d_var_decay : MiniSat::Solver
• d_var_inc : MiniSat::Solver
• d_varAssignments : CVC3::TheoryCore
• d_varInfo : SAT::CNF_Manager
• d_varModelMap : CVC3::TheoryCore
• d_vars : CVC3::ExprClosure , CVC3::SearchSat , CVC3::TheoryCore
• d_varSet : CVC3::VariableManager
• d_varsUndoList : CVC3::SearchSat
• d_varsUndoListSize : CVC3::SearchSat
• d_vc : CVC3::VCCmd , SAT::CNF_Manager
• d_vector : CVC3::Assumptions
• d_visited : CVC3::DecisionEngine
• d_vm : CVC3::SearchImplBase , CVC3::VariableValue , CVC3::VariableManagerNotifyObj
• d_watches : MiniSat::Solver
• d_withAssump : CVC3::TheoremManager
• d_withIndentation : CVC3::ExprManager
• d_withProof : CVC3::TheoremManager
• d_wp : CVC3::VariableValue , CVC3::ClauseValue
• d_zeroVar : CVC3::Translator
• data : MiniSat::vec< T > , MiniSat::Clause , vec< T >
• db_simpl : MiniSat::SolverStats
• debug : MiniSat::SolverStats
• decision_strategy : CSolverParameters
• decisions : MiniSat::SolverStats
• del_clauses : MiniSat::SolverStats
• del_lemmas : MiniSat::SolverStats
• dependenciesMap : CVC3::TheoryArithNew
• done : CVC3::ParserTemp

---