CVC3: Class Members

- d -

d_abInstCount : CVC3::TheoryQuant
d_active : CVC3::TheoremManager
d_activity : MiniSat::Clause , MiniSat::Solver
d_added : CVC3::VariableValue
d_all_good : CVC3::CompleteInstPreProcessor
d_all_index : recCompleteInster
d_all_multTrigsInfo : CVC3::TheoryQuant
d_allIndex : CVC3::CompleteInstPreProcessor
d_allInstCount : CVC3::TheoryQuant
d_allInstCount2 : 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::TheoryArray , CVC3::TheoryUF
d_applyCNFRulesCache : CVC3::SearchImplBase
d_arithUsed : CVC3::Translator
d_arrayConvertMap : CVC3::Translator
d_arrayIndic : CVC3::TheoryQuant
d_arrayTrigs : CVC3::TheoryQuant
d_arrayType : CVC3::Translator
d_assertions : SAT::DPLLTBasic
d_assertionsStack : SAT::DPLLTBasic
d_assigns : MiniSat::Solver
d_assump : CVC3::VariableValue , CVC3::RegTheoremValue , CVC3::RWTheoremValue
d_assump_map : LFSCPrinter
d_assump_str : LFSCPrinter
d_assumptions : CVC3::SearchImplBase
d_ax : CVC3::Translator
d_basicModelVars : CVC3::TheoryCore
d_batchedAssertions : CVC3::VCL
d_batchedAssertionsIdx : CVC3::VCL
d_bb_index : CVC3::TheoryBitvector
d_beginningOfLine : CVC3::ExprStream
d_berkminFlag : CVC3::SearchEngineFast
d_bestByExpr : CVC3::DecisionEngine
d_bindGlobalHistory : CVC3::TheoryQuant
d_bindGlobalThmHistory : CVC3::TheoryQuant
d_bindHistory : CVC3::TheoryQuant
d_bitblast : CVC3::TheoryBitvector
d_bitvecCache : CVC3::TheoryBitvector
d_body : CVC3::ExprClosure , recCompleteInster
d_bool : CVC3::ExprManager
d_bool_res_str : LFSCPrinter
d_booleanRWFlag : CVC3::TheoryBitvector
d_boolExtractCacheFlag : CVC3::TheoryBitvector
d_bottomLevel : CVC3::DecisionEngineCaching , CVC3::DecisionEngineMBTF
d_bottomScope : SAT::CNF_Manager , CVC3::Context , CVC3::SearchImplBase , CVC3::SearchSat
d_boundVarMap : CVC3::TheoryCore
d_boundVarStack : CVC3::TheoryCore
d_budgetLimit : CVC3::ExprTransform
d_buff : recCompleteInster
d_buffer : CVC3::TheoryArith3 , CVC3::TheoryArithNew
d_buffer_0 : CVC3::TheoryArithOld
d_buffer_1 : CVC3::TheoryArithOld
d_buffer_2 : CVC3::TheoryArithOld
d_buffer_3 : CVC3::TheoryArithOld
d_bufferIdx : CVC3::TheoryArith3 , CVC3::TheoryArithNew
d_bufferIdx_0 : CVC3::TheoryArithOld
d_bufferIdx_1 : CVC3::TheoryArithOld
d_bufferIdx_2 : CVC3::TheoryArithOld
d_bufferIdx_3 : CVC3::TheoryArithOld
d_bufferThres : CVC3::TheoryArith3 , 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_bvs : recCompleteInster
d_bvTypePredExprIndex : CVC3::TheoryBitvector
d_bvTypePreds : CVC3::TheoryBitvector
d_bvZero : CVC3::TheoryBitvector , CVC3::BitvectorTheoremProducer
d_cache : CVC3::TheoryArith3::TheoryArith3::VarOrderGraph , CVC3::TheoryArithNew::TheoryArithNew::VarOrderGraph , CVC3::TheoryArithOld::TheoryArithOld::VarOrderGraph , CVC3::DecisionEngineCaching , CVC3::DecisionEngineMBTF
d_cachedValue : CVC3::TheoremValue
d_cachedValues : CVC3::TheoremManager
d_cacheTheorem : CVC3::TheoryQuant
d_cacheThmPos : CVC3::TheoryQuant
d_calledFromParser : CVC3::VCCmd
d_callThisRound : CVC3::TheoryQuant
d_category : CVC3::Translator
d_cdmap : CVC3::CDOmap< Key, Data, HashFcn > , CVC3::CDOmapOrdered< Key, Data >
d_cdo : CVC3::SmartCDO< T >::SmartCDO::RefCDO
d_checkProofs : CVC3::TheoremProducer
d_children : CVC3::ExprNode , CVC3::ExprNodeTmp
d_chunkList : CVC3::MemoryManagerChunks , CVC3::ContextMemoryManager
d_chunkSize : CVC3::MemoryManagerChunks
d_chunkSizeBytes : 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_cm : CVC3::Context , SAT::DPLLTBasic , CVC3::ExprManager , CVC3::TheoremManager , CVC3::TheoryCore , CVC3::VariableManager , CVC3::VCL , CVC3::SearchSatTheoryAPI
d_cmm : CVC3::Scope
d_cmmStack : CVC3::Context
d_cnf : SAT::DPLLTBasic
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 : SAT::CNF_Manager , CVC3::ExprTransform , CVC3::SearchEngine , CVC3::Theory , CVC3::SearchEngineTheoremProducer
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::TheoryArith3::TheoryArith3::Ineq , CVC3::TheoryArithNew::TheoryArithNew::Ineq , CVC3::TheoryArithOld::TheoryArithOld::Ineq
d_constructorMap : CVC3::TheoryDatatype
d_context : CVC3::CDMap< Key, Data, HashFcn > , CVC3::CDMapOrdered< Key, Data > , CVC3::Scope , CVC3::ContextNotifyObj
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_convertToBV : CVC3::Translator
d_convertToDiff : CVC3::Translator
d_core : CVC3::ExprTransform , CVC3::SearchEngine , CVC3::DecisionEngine , CVC3::CoreTheoremProducer , CVC3::PrettyPrinterCore , CVC3::TypeComputerCore
d_coreSatAPI : CVC3::SearchSat , CVC3::TheoryCore
d_coreSatAPI_implBase : CVC3::SearchImplBase
d_count : CVC3::VariableValue
d_counter : CVC3::StatCounter
d_counters : CVC3::Statistics
d_countLeft : CVC3::TheoryArith3 , CVC3::TheoryArithNew , CVC3::TheoryArithOld
d_countPrev : CVC3::VariableValue
d_countRight : CVC3::TheoryArith3 , CVC3::TheoryArithNew , CVC3::TheoryArithOld
d_createProof : SAT::DPLLTMiniSat
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 > , CVC3::CDOmapOrdered< Key, Data > , CVC3::CDO< T > , CVC3::CLFlag , CVC3::ContextObjChain , Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey > , CVC3::Parser , CVC3::SmartCDO< T > , MiniSat::Clause
d_dataSize : CVC3::MemoryManagerChunks
d_datatypes : CVC3::TheoryDatatype
d_decider : SAT::DPLLT , CVC3::SearchSat , MiniSat::Solver
d_decisionEngine : CVC3::SearchEngineFast , CVC3::SearchSimple
d_default_params : MiniSat::Solver
d_delay : CVC3::SmartCDO< T >::SmartCDO::RefCDO
d_deleted : CVC3::ClauseValue , CVC3::VariableManager
d_depth : CVC3::ExprStream
d_derivation : MiniSat::Solver
d_dir : CVC3::ClauseValue
d_disableGC : CVC3::ExprManager , CVC3::VariableManager
d_diseq : CVC3::TheoryArith3 , CVC3::TheoryArithNew , CVC3::TheoryArithOld
d_diseqIdx : CVC3::TheoryArith3 , CVC3::TheoryArithNew , CVC3::TheoryArithOld
d_display : CVC3::CLFlag
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_dynamicFlags : CVC3::ExprValue
d_e : CVC3::Expr::Expr::iterator::Expr::iterator::Proxy
d_edges : CVC3::TheoryArith3::TheoryArith3::VarOrderGraph , CVC3::TheoryArithNew::TheoryArithNew::VarOrderGraph , CVC3::TheoryArithOld::TheoryArithOld::VarOrderGraph
d_elementType : CVC3::Translator
d_elist : CVC3::NotifyList
d_em : CVC3::ExprManager::ExprManager::HashEV , CVC3::ExprManagerNotifyObj , CVC3::ExprStream , CVC3::ExprValue , CVC3::TheoremManager , CVC3::TheoremProducer , CVC3::Theory , CVC3::Translator , CVC3::VCL
d_emptyClause : MiniSat::Derivation
d_emptyVec : CVC3::ExprManager
d_endChunk : CVC3::MemoryManagerChunks , CVC3::ContextMemoryManager
d_endChunkStack : CVC3::ContextMemoryManager
d_enqueueCNFCache : CVC3::SearchImplBase
d_eq : CVC3::TheoryBitvector
d_eq_index : CVC3::TheoryBitvector
d_eq_list : CVC3::TheoryQuant
d_eq_pos : CVC3::TheoryQuant
d_eqNext : CVC3::ExprValue
d_eqPending : CVC3::TheoryBitvector
d_eqs : CVC3::TheoryQuant
d_eqs_pos : CVC3::TheoryQuant
d_eqsUpdate : CVC3::TheoryQuant
d_equal : Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >
d_equalities : CVC3::Translator
d_expand : CVC3::TheoremValue
d_expandFlags : CVC3::TheoremManager
d_expensive_ccmin : MiniSat::Solver
d_expr : CVC3::Expr , CVC3::Op , CVC3::Theorem , CVC3::Type , CVC3::VariableValue , CVC3::DecisionEngineCaching::DecisionEngineCaching::CacheEntry , CVC3::DecisionEngineMBTF::DecisionEngineMBTF::CacheEntry
d_expr_pol : CVC3::CompleteInstPreProcessor
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 : CVC3::CDMap< Key, Data, HashFcn > , CVC3::CDMapOrdered< Key, Data >
d_flag : CVC3::ScopeWatcher , CVC3::ExprValue , CVC3::StatFlag , CVC3::TheoremManager , CVC3::TheoremValue
d_flagCounter : CVC3::ExprManager
d_flags : CVC3::CDFlags , SAT::CNF_Manager , CVC3::Statistics , CVC3::TheoremManager , CVC3::TheoryCore , CVC3::VCL , CVC3::CNF_TheoremProducer
d_formula : SAT::CNF_Formula_Impl , SAT::CD_CNF_Formula
d_freeConstDB : CVC3::TheoryArith3 , CVC3::TheoryArithNew , CVC3::TheoryArithOld
d_freeList : CVC3::MemoryManagerChunks
d_fullTrigs : CVC3::TheoryQuant
d_funApplications : CVC3::TheoryUF
d_funApplicationsIdx : CVC3::TheoryUF
d_gBindQueue : CVC3::TheoryQuant
d_getConstantStack : CVC3::TheoryDatatype
d_gfactLimit : CVC3::TheoryQuant
d_globals : CVC3::TheoryCore
d_gnd_cache : CVC3::CompleteInstPreProcessor
d_goal : CVC3::SearchSimple
d_graph : CVC3::TheoryArith3 , CVC3::TheoryArithNew , CVC3::TheoryArithOld
d_grayShadowThres : CVC3::TheoryArithOld
d_gUnivQueue : CVC3::TheoryQuant
d_hash : CVC3::ExprValue , Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >
d_hash_table : Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::hash_table::iterator , Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::hash_table::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 , MiniSat::Clause
d_idCounter : CVC3::ExprStream
d_idx : CVC3::ExprSkolem , CVC3::VCL::VCL::UserAssertion
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 , CVC3::TheoryArray
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 : SAT::Var , SAT::Lit , CVC3::ExprManager , CVC3::ExprValue , CVC3::TheoryArray , CVC3::DecisionEngineCaching , CVC3::DecisionEngineMBTF
d_index1 : CVC3::TheoryBitvector
d_index2 : CVC3::TheoryBitvector
d_indexChunkList : CVC3::ContextMemoryManager
d_indexChunkListStack : CVC3::ContextMemoryManager
d_indexExpr : CVC3::TheoryQuant
d_indexScore : CVC3::TheoryQuant
d_indexType : CVC3::Translator
d_inEnd : CVC3::TheoryQuant
d_ineq : CVC3::TheoryArith3::TheoryArith3::Ineq , CVC3::TheoryArithNew::TheoryArithNew::Ineq , CVC3::TheoryArithOld::TheoryArithOld::Ineq
d_inequalitiesLeftDB : CVC3::TheoryArith3 , CVC3::TheoryArithNew , CVC3::TheoryArithOld
d_inequalitiesRightDB : CVC3::TheoryArith3 , CVC3::TheoryArithNew , CVC3::TheoryArithOld
d_inferences : MiniSat::Derivation
d_inGC : CVC3::ExprManager
d_initMaxScore : CVC3::TheoryQuant
d_inMap : CVC3::CDOmap< Key, Data, HashFcn > , CVC3::CDOmapOrdered< Key, Data >
d_inModelCreation : CVC3::TheoryArith3 , CVC3::TheoryArithNew , CVC3::TheoryArithOld
d_inPP : CVC3::TheoryCore
d_inputClauses : MiniSat::Derivation
d_inputLang : 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_inUpdate : CVC3::TheoryCore
d_is_macro_def : CVC3::CompleteInstPreProcessor
d_isAssump : CVC3::TheoremValue
d_isSubst : CVC3::TheoremValue
d_it : CVC3::Assumptions::Assumptions::iterator , CVC3::CDMap< Key, Data, HashFcn >::CDMap::iterator , CVC3::CDMap< Key, Data, HashFcn >::CDMap::orderedIterator , CVC3::CDMapOrdered< Key, Data >::CDMapOrdered::iterator , CVC3::CDMapOrdered< Key, Data >::CDMapOrdered::orderedIterator , CVC3::Expr::Expr::iterator , CVC3::ExprMap< Data >::ExprMap::const_iterator , CVC3::ExprMap< Data >::ExprMap::iterator , CVC3::ExprHashMap< Data >::ExprHashMap::const_iterator , CVC3::ExprHashMap< Data >::ExprHashMap::iterator
d_iteLiftArith : CVC3::Translator
d_iteMap : SAT::CNF_Manager
d_key : CVC3::CDOmap< Key, Data, HashFcn > , CVC3::CDOmapOrdered< Key, Data >
d_kind : CVC3::Op , CVC3::ExprValue
d_kindMap : CVC3::ExprManager
d_kindMapByName : CVC3::ExprManager
d_kinds : CVC3::TheoryArith
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_lastEqsUpdatePos : CVC3::TheoryQuant
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_left : SAT::SatProofNode
d_lemmas : CVC3::SearchSat
d_lemmasNext : CVC3::SearchSat
d_let_map : LFSCPrinter
d_level : CVC3::Scope , MiniSat::Solver
d_lhs : CVC3::RWTheoremValue
d_liftReadIte : CVC3::TheoryArray
d_lineWidth : CVC3::ExprManager , CVC3::ExprStream
d_list : CVC3::CDList< T >
d_lit : CVC3::SearchImplBase::SearchImplBase::Splitter , CVC3::SearchSat::SearchSat::LitPriorityPair , SAT::SatProofNode
d_literals : CVC3::ClauseValue , CVC3::SearchEngineFast
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_macro_def : CVC3::CompleteInstPreProcessor
d_macro_lhs : CVC3::CompleteInstPreProcessor
d_macro_quant : CVC3::CompleteInstPreProcessor
d_manual_triggers : CVC3::ExprClosure
d_map : CVC3::VCCmd , CVC3::ExprHashMap< Data > , CVC3::CDMap< Key, Data, HashFcn > , CVC3::CDMapOrdered< Key, Data > , CVC3::CLFlags , CVC3::ExprMap< Data >
d_master : CVC3::ContextObjChain
d_maxIL : CVC3::TheoryQuant
d_maxILReached : CVC3::TheoryQuant
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::TheoremManager , CVC3::VariableManager
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::Context , CVC3::ExprVar , CVC3::ExprBoundVar , CVC3::SearchEngineFast , CVC3::SearchSat , CVC3::Theory , CVC3::SearchSimple , 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_newPPCache : CVC3::ExprTransform
d_next : CVC3::CDOmapOrdered< Key, Data > , Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::hash_table::BucketNode , CVC3::CDOmap< Key, Data, HashFcn >
d_nextFree : CVC3::MemoryManagerChunks , CVC3::ContextMemoryManager
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 >::hash_table::iterator , Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::hash_table::const_iterator
d_nodes : SAT::SatProof
d_nonLiterals : CVC3::SearchSimple , CVC3::SearchEngineFast
d_nonLiteralsSaved : CVC3::SearchEngineFast
d_nonlitQueryEnd : CVC3::SearchEngineFast
d_nonlitQueryStart : CVC3::SearchEngineFast
d_notifyEq : CVC3::TheoryCore
d_notifyList : CVC3::ExprValue
d_notifyObj : CVC3::ExprManager , CVC3::TheoryCore , CVC3::VariableManager , CVC3::SmartCDO< T >::SmartCDO::RefCDO
d_notifyObjList : CVC3::Context
d_nullExpr : SAT::CNF_Manager , CVC3::ExprManager
d_numVars : SAT::CNF_Formula_Impl , SAT::CD_CNF_Formula
d_offset_multi_trig : CVC3::TheoryQuant
d_ok : MiniSat::PushEntry , MiniSat::Solver
d_opExpr : CVC3::ExprApplyTmp , CVC3::ExprApply
d_order : MiniSat::Solver
d_origFormulaOption : CVC3::SearchImplBase
d_os : CVC3::ExprStream , CVC3::Statistics
d_osdump : CVC3::Translator
d_osdumpFile : CVC3::Translator
d_outputLang : CVC3::ExprManager
d_pair : CVC3::CDMap< Key, Data, HashFcn >::CDMap::iterator::CDMap::iterator::Proxy , CVC3::CDMap< Key, Data, HashFcn >::CDMap::orderedIterator::CDMap::orderedIterator::Proxy , CVC3::CDMapOrdered< Key, Data >::CDMapOrdered::iterator::CDMapOrdered::iterator::Proxy , CVC3::CDMapOrdered< Key, Data >::CDMapOrdered::orderedIterator::CDMapOrdered::orderedIterator::Proxy , CVC3::ExprMap< Data >::ExprMap::iterator::ExprMap::iterator::Proxy , CVC3::ExprHashMap< Data >::ExprHashMap::const_iterator::ExprHashMap::const_iterator::Proxy , CVC3::ExprHashMap< Data >::ExprHashMap::iterator::ExprHashMap::iterator::Proxy , CVC3::ExprMap< Data >::ExprMap::const_iterator::ExprMap::const_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_pathLenghtThres : CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph
d_pending : CVC3::ExprManager
d_pendingClauses : MiniSat::Solver
d_pendingLemmas : CVC3::SearchSat
d_pendingLemmasNext : CVC3::SearchSat
d_pendingLemmasSize : CVC3::SearchSat
d_pendingScopes : 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 : CVC3::CDOmap< Key, Data, HashFcn > , CVC3::CDOmapOrdered< Key, Data >
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::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 : SAT::DPLLTMiniSat , CVC3::Proof , CVC3::TheoremValue , SAT::SatProofNode
d_pushes : MiniSat::Solver
d_pushID : MiniSat::Clause
d_pushIDs : MiniSat::Solver
d_pushLevel : SAT::DPLLTBasic
d_pushNegCache : CVC3::ExprTransform , CVC3::TheoryBitvector
d_qhead : MiniSat::Solver , MiniSat::PushEntry
d_quant : CVC3::ExprSkolem
d_quant_equiv_map : CVC3::CompleteInstPreProcessor
d_quant_rules : CVC3::CompleteInstPreProcessor
d_quantLevel : CVC3::TheoremValue
d_queue : CVC3::TheoryCore
d_queueSE : CVC3::TheoryCore
d_r : CVC3::TheoryArith3::TheoryArith3::FreeConst , CVC3::TheoryArithNew::TheoryArithNew::FreeConst , CVC3::TheoryArithOld::TheoryArithOld::FreeConst , CVC3::ExprRational
d_rank : CVC3::DecisionEngineMBTF::DecisionEngineMBTF::CacheEntry , CVC3::DecisionEngineCaching::DecisionEngineCaching::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 , SAT::Clause
d_rebuildCache : CVC3::ExprManager
d_ref : CVC3::SmartCDO< T >::SmartCDO::RefCDO::SmartCDO::RefCDO::RefNotifyObj
d_refcount : CVC3::ExprValue , CVC3::ClauseValue , CVC3::VariableValue
d_refCount : CVC3::SmartCDO< T >::SmartCDO::RefCDO
d_refcount : 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::SearchEngineFast::ConflictClauseManager
d_restorer : CVC3::SearchSat
d_result : recCompleteInster
d_rhs : CVC3::TheoryArith3::TheoryArith3::Ineq , CVC3::TheoryArithNew::TheoryArithNew::Ineq , CVC3::TheoryArithOld::TheoryArithOld::Ineq , CVC3::RWTheoremValue
d_right : SAT::SatProofNode
d_root : SAT::SatProof
d_rootLevel : MiniSat::Solver
d_rules : CVC3::TheoremManager , CVC3::TheorySimulate , CVC3::TheoryCore , CVC3::TheoryArithNew , CVC3::ExprTransform , CVC3::TheoryRecords , CVC3::TheoryQuant , SAT::CNF_Manager , CVC3::SearchEngine , CVC3::TheoryArith3 , CVC3::TheoryArithOld , CVC3::TheoryDatatype , CVC3::TheoryUF , CVC3::TheoryBitvector , CVC3::TheoryArray , CVC3::VariableManager
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::ContextObj , CVC3::VariableValue , CVC3::ClauseValue
d_scopeLevel : CVC3::TheoremValue
d_score : CVC3::VariableValue
d_se : CVC3::SearchEngineFast::SearchEngineFast::ConflictClauseManager , CVC3::CoreSatAPI_implBase , CVC3::VCL , CVC3::DecisionEngine
d_selectorMap : CVC3::TheoryDatatype
d_sharedSubterms : CVC3::TheoryBitvector , CVC3::TheoryArray
d_sharedSubtermsList : CVC3::TheoryBitvector , CVC3::TheoryArray
d_sharedTerms : CVC3::TheoryArith3 , CVC3::TheoryArithOld , CVC3::TheoryArithNew
d_sharedTermsList : CVC3::TheoryArithOld
d_sharedVars : CVC3::TheoryArithOld , CVC3::TheoryArith3 , 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_size : CVC3::ExprValue , Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey > , CVC3::CDList< T >
d_size_learnt : MiniSat::Clause
d_skolem_axioms : CVC3::CommonTheoremProducer
d_skolemized_thms : CVC3::CommonTheoremProducer
d_skolemVars : CVC3::CommonTheoremProducer
d_smartClauses : CVC3::CNF_TheoremProducer
d_smartSplits : CVC3::TheoryDatatype
d_solver : CVC3::TheoryCore
d_solvers : SAT::DPLLTMiniSat
d_splitSign : CVC3::TheoryArithOld
d_splitterAsserted : CVC3::TheoryDatatype
d_splitterCount : CVC3::SearchEngineFast , CVC3::DecisionEngine
d_splitters : CVC3::TheoryDatatype , CVC3::DecisionEngine
d_splittersIndex : CVC3::TheoryDatatype
d_ss : CVC3::SearchSat::SearchSat::Restorer , CVC3::SearchSatCoreSatAPI , CVC3::SearchSatDecider , CVC3::SearchSatCNFCallback , CVC3::SearchSatTheoryAPI
d_stackLevel : CVC3::VCL
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::TheoryArith3::TheoryArith3::FreeConst , CVC3::TheoryArithNew::TheoryArithNew::FreeConst , CVC3::TheoryArithOld::TheoryArithOld::FreeConst
d_subTermsMap : CVC3::TheoryQuant
d_t : CVC3::Assumptions::Assumptions::iterator::Assumptions::iterator::Proxy
d_table : Hash::hash_set< _Key, _HashFcn, _EqualKey > , Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >
d_tcc : CVC3::VCL::VCL::UserAssertion
d_tccCache : CVC3::TheoryCore
d_tempBinds : CVC3::TheoryQuant
d_terms : CVC3::TheoryCore
d_termTheorems : CVC3::TheoryCore
d_testerMap : CVC3::TheoryDatatype
d_thead : MiniSat::PushEntry , MiniSat::Solver
d_theorem : MiniSat::Clause , SAT::SatProofNode
d_theorems : CVC3::SearchSat
d_theories : CVC3::VCL , CVC3::TheoryCore
d_theoryAPI : SAT::DPLLT , CVC3::SearchSat , MiniSat::Solver
d_theoryArith : CVC3::Translator , CVC3::ExprTransform , CVC3::VCL , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducerOld , CVC3::ArithTheoremProducer3
d_theoryArray : CVC3::Translator , CVC3::VCL , CVC3::ArrayTheoremProducer
d_theoryBitvector : CVC3::BitvectorTheoremProducer , CVC3::VCL , CVC3::Translator
d_theoryCore : CVC3::CompleteInstPreProcessor , CVC3::TheoryCore::TheoryCore::CoreNotifyObj , CVC3::VCL , CVC3::Theory , CVC3::Translator
d_theoryDatatype : CVC3::DatatypeTheoremProducer , CVC3::VCL , CVC3::Translator
d_theoryExplanations : MiniSat::Solver
d_theoryMap : CVC3::TheoryCore
d_theoryQuant : CVC3::Translator , CVC3::VCL , CVC3::QuantTheoremProducer
d_theoryRecords : CVC3::VCL , CVC3::RecordsTheoremProducer , CVC3::Translator
d_theorySimulate : CVC3::Translator , CVC3::VCL
d_theoryUF : CVC3::UFTheoremProducer , CVC3::VCL , CVC3::Translator
d_theoryUsed : CVC3::Theory
d_thm : CVC3::Circuit , CVC3::Theorem , CVC3::TheoremValue , CVC3::VariableValue , CVC3::Theorem3 , CVC3::ClauseValue , CVC3::VCL::VCL::UserAssertion
d_thmCount : CVC3::TheoryQuant
d_timeBase : CVC3::TheoryCore
d_timeLimit : CVC3::TheoryCore
d_tlist : CVC3::NotifyList
d_tm : CVC3::VCL , CVC3::TheoremValue , CVC3::TheoremProducer , CVC3::ExprManager , CVC3::TheoryCore
d_tmpFile : CVC3::Translator
d_topLevel : CVC3::DecisionEngineCaching , CVC3::DecisionEngineMBTF
d_topLevelLock : CVC3::DecisionEngineCaching , CVC3::DecisionEngineMBTF
d_topScope : CVC3::Context
d_totalInstCount : CVC3::TheoryQuant
d_totalThmCount : CVC3::TheoryQuant
d_tp : CVC3::CLFlag
d_trail : MiniSat::Solver
d_trail_lim : MiniSat::Solver
d_trail_pos : lastToFirst_lt , MiniSat::Solver
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_transThm : CVC3::TheoryQuant
d_trash : CVC3::CDMapOrdered< Key, Data > , CVC3::CDMap< Key, Data, HashFcn >
d_true : CVC3::ExprManager
d_trueInstCount : CVC3::TheoryQuant
d_trust : CVC3::DecisionEngineCaching::DecisionEngineCaching::CacheEntry , CVC3::DecisionEngineMBTF::DecisionEngineMBTF::CacheEntry
d_type : CVC3::ExprValue
d_typeComplete : CVC3::TheoryDatatypeLazy
d_typeComputer : CVC3::ExprManager , CVC3::TheoryCore
d_typeExprMap : CVC3::TheoryQuant
d_typeFound : CVC3::QuantTheoremProducer
d_typeKinds : CVC3::ExprManager
d_UFIDL_ok : CVC3::Translator
d_uid : CVC3::ParserTemp , CVC3::ExprBoundVar
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_useCompleteInst : CVC3::TheoryQuant
d_useEnqueueFact : CVC3::SearchEngineFast
d_useEqu : CVC3::TheoryQuant
d_useExprScore : CVC3::TheoryQuant
d_usefulGterms : CVC3::TheoryQuant
d_useFullTrig : CVC3::TheoryQuant
d_useGFact : CVC3::TheoryQuant
d_useInstAll : CVC3::TheoryQuant
d_useInstGCache : CVC3::TheoryQuant
d_useInstLCache : CVC3::TheoryQuant
d_useInstThmCache : CVC3::TheoryQuant
d_useInstTrue : CVC3::TheoryQuant
d_useLazyInst : CVC3::TheoryQuant
d_useManTrig : CVC3::TheoryQuant
d_useMult : CVC3::TheoryQuant
d_useMultTrig : CVC3::TheoryQuant
d_useNaiveInst : CVC3::TheoryQuant
d_useNew : CVC3::TheoryQuant
d_useNewEqu : 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_val : CVC3::VariableValue , CVC3::Variable
d_value : Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::hash_table::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::SearchSat , CVC3::TheoryCore , CVC3::ExprClosure
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 , LFSCPrinter
d_vm : CVC3::VariableValue , CVC3::SearchImplBase , 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 >
db_simpl : MiniSat::SolverStats
debug : MiniSat::SolverStats
decisions : MiniSat::SolverStats
defaultDivideExpr : CVC3::TheoryQuant
defaultMinusExpr : CVC3::TheoryQuant
defaultMultExpr : CVC3::TheoryQuant
defaultPlusExpr : CVC3::TheoryQuant
defaultPowExpr : CVC3::TheoryQuant
defaultReadExpr : CVC3::TheoryQuant
defaultWriteExpr : CVC3::TheoryQuant
del_clauses : MiniSat::SolverStats
del_lemmas : MiniSat::SolverStats
dependenciesMap : CVC3::TheoryArithNew
diff_logic_size : CVC3::TheoryArithOld
diffLogicGraph : CVC3::TheoryArithOld
diffLogicOnly : CVC3::TheoryArithOld
diseqSplitAlready : CVC3::TheoryArithOld
done : CVC3::ParserTemp
dontBuffer : CVC3::TheoryArithOld