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

- d -

• d_abInstCount : CVC3::TheoryQuant
• d_active : CVC3::TheoremManager
• d_activity : MiniSat::Clause , MiniSat::Solver
• d_added : CVC3::VariableValue
• d_addInequalities_str : LFSCObj
• 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_and_final_s : LFSCObj
• d_and_mid_s : LFSCObj
• d_andE_str : LFSCObj
• 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_assm : LFSCAssume
• d_assump : CVC3::VariableValue , CVC3::RegTheoremValue , CVC3::RWTheoremValue
• d_assump_map : LFSCObj
• d_assump_str : LFSCObj
• d_assumptions : CVC3::SearchImplBase
• d_ax : CVC3::Translator
• d_basic_subst_op0_str : LFSCObj
• d_basic_subst_op1_str : LFSCObj
• d_basic_subst_op_str : LFSCObj
• d_basicModelVars : CVC3::TheoryCore
• d_batchedAssertions : CVC3::VCL
• d_batchedAssertionsIdx : CVC3::VCL
• d_bb_index : CVC3::TheoryBitvector
• d_beginningOfLine : CVC3::ExprStream
• d_benchName : CVC3::Translator
• 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 , LFSCPfLet , recCompleteInster
• d_bool : CVC3::ExprManager
• d_bool_res_str : LFSCObj
• 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_c : TReturn
• d_cache : CVC3::TheoryArith3::VarOrderGraph , CVC3::TheoryArithNew::VarOrderGraph , CVC3::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_canon_invert_divide_str : LFSCObj
• d_canon_mult_str : LFSCObj
• d_canon_plus_str : LFSCObj
• d_category : CVC3::Translator
• d_cdmap : CVC3::CDOmap< Key, Data, HashFcn > , CVC3::CDOmapOrdered< Key, Data >
• d_cdo : CVC3::SmartCDO< T >::RefCDO< U >
• d_checkProofs : CVC3::TheoremProducer
• d_children : CVC3::ExprNode , CVC3::ExprNodeTmp , LFSCBoolRes , LFSCLraAdd , LFSCLraSub
• 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_cnf_add_unit_str : LFSCObj
• d_cnf_convert_str : LFSCObj
• d_CNF_str : LFSCObj
• d_cnfCache : CVC3::SearchImplBase
• d_cnfCallback : SAT::CNF_Manager , CVC3::SearchSat
• d_CNFITE_str : LFSCObj
• d_cnfManager : CVC3::SearchSat
• d_cnfOption : CVC3::SearchImplBase
• d_cnfStack : SAT::DPLLTBasic
• d_cnfVars : SAT::CNF_Manager , CVC3::SearchImplBase
• d_col : CVC3::ExprStream , LFSCBoolRes
• d_combineAssump : CVC3::Translator
• d_common_pf_rules : LFSCPrinter
• 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::Ineq , CVC3::TheoryArithNew::Ineq , CVC3::TheoryArithOld::Ineq
• d_const_predicate_str : LFSCObj
• 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_cycle_conflict_str : LFSCObj
• 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 >::RefCDO< U >
• 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::iterator::Proxy , LFSCProofExpr
• d_edges : CVC3::TheoryArith3::VarOrderGraph , CVC3::TheoryArithNew::VarOrderGraph , CVC3::TheoryArithOld::VarOrderGraph
• d_elementType : CVC3::Translator
• d_elist : CVC3::NotifyList
• d_em : CVC3::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_eq_symm_str : LFSCObj
• d_eq_trans_str : LFSCObj
• 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::CacheEntry , CVC3::DecisionEngineMBTF::CacheEntry
• d_expr_pol : CVC3::CompleteInstPreProcessor
• d_expResult : CVC3::Translator
• d_exprLastUpdatedPos : CVC3::TheoryQuant
• d_exprs : recCompleteInster
• 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_flip_inequality_str : LFSCObj
• d_formula : SAT::CNF_Formula_Impl , SAT::CD_CNF_Formula
• d_formulas : LFSCObj
• d_formulas_printed : LFSCObj
• 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 >::iterator , Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::const_iterator
• d_hasMoreBVs : CVC3::TheoryQuant
• d_hasRt : TReturn
• 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::UserAssertion
• d_idxUserAssump : CVC3::SearchSat
• d_if_lift_rule_str : LFSCObj
• d_iff_false_elim_str : LFSCObj
• d_iff_false_str : LFSCObj
• d_iff_mp_str : LFSCObj
• d_iff_not_false_str : LFSCObj
• d_iff_s : LFSCObj
• d_iff_symm_str : LFSCObj
• d_iff_trans_str : LFSCObj
• d_iff_true_elim_str : LFSCObj
• d_iff_true_str : LFSCObj
• d_ifLiftOption : CVC3::SearchImplBase
• d_ignoreCnfVarsOption : CVC3::SearchImplBase
• d_imp_mp_str : LFSCObj
• d_imp_s : LFSCObj
• d_impl_mp_str : LFSCObj
• d_impliedLiterals : CVC3::TheoryCore
• d_impliedLiteralsIdx : CVC3::TheoryCore
• d_implyEqualities_str : LFSCObj
• d_implyNegatedInequality_str : LFSCObj
• d_implyWeakerInequality_str : LFSCObj
• d_implyWeakerInequalityDiffLogic_str : LFSCObj
• 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::Ineq , CVC3::TheoryArithNew::Ineq , CVC3::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_int_const_eq_str : LFSCObj
• 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_isTh : LFSCPfLet
• d_it : CVC3::Assumptions::iterator , CVC3::CDMap< Key, Data, HashFcn >::iterator , CVC3::CDMap< Key, Data, HashFcn >::orderedIterator , CVC3::CDMapOrdered< Key, Data >::iterator , CVC3::CDMapOrdered< Key, Data >::orderedIterator , CVC3::Expr::iterator , CVC3::ExprMap< Data >::const_iterator , CVC3::ExprMap< Data >::iterator , CVC3::ExprHashMap< Data >::const_iterator , CVC3::ExprHashMap< Data >::iterator
• d_ite_s : LFSCObj
• 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_L : TReturn
• d_L_used : TReturn
• 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_learned_clause_str : LFSCObj
• d_learnts : MiniSat::Solver
• d_left : SAT::SatProofNode
• d_lemmas : CVC3::SearchSat
• d_lemmasNext : CVC3::SearchSat
• d_lessThan_To_LE_rhs_rwr_str : LFSCObj
• d_letPf : LFSCPfLet
• d_letPfRpl : LFSCPfLet
• d_level : CVC3::Scope , MiniSat::Solver
• d_lfsc_pf : TReturn
• d_lhs : CVC3::RWTheoremValue
• d_liftReadIte : CVC3::TheoryArray
• d_lineWidth : CVC3::ExprManager , CVC3::ExprStream
• d_list : CVC3::CDList< T >
• d_lit : CVC3::SearchImplBase::Splitter , CVC3::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::CDMap< Key, Data, HashFcn > , CVC3::CDMapOrdered< Key, Data > , CVC3::CLFlags , CVC3::ExprMap< Data > , CVC3::ExprHashMap< Data > , CVC3::VCCmd
• 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_minisat_proof_str : LFSCObj
• d_minus_to_plus_str : LFSCObj
• 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_mult_eqn_str : LFSCObj
• d_mult_ineqn_str : LFSCObj
• d_multitrigs_maps : CVC3::TheoryQuant
• d_multTriggers : CVC3::TheoryQuant
• d_multTrigs : CVC3::TheoryQuant
• d_mybvs : CVC3::TheoryQuant
• d_n : CVC3::Rational , CVC3::Unsigned
• d_name : CVC3::Context , CVC3::ExprVar , CVC3::ExprSymbol , CVC3::ExprBoundVar , CVC3::SearchEngineFast , CVC3::SearchSat , CVC3::SearchSimple , CVC3::Theory
• d_name_of_cur_ctxt : CVC3::VCCmd
• d_neg : CVC3::VariableValue
• d_negAdded : CVC3::VariableValue
• d_negated_inequality_str : LFSCObj
• 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::CDOmap< Key, Data, HashFcn > , CVC3::CDOmapOrdered< Key, Data > , Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::BucketNode
• 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 >::iterator , Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::const_iterator
• d_nodes : SAT::SatProof
• d_nonLiterals : CVC3::SearchEngineFast , CVC3::SearchSimple
• d_nonLiteralsSaved : CVC3::SearchEngineFast
• d_nonlitQueryEnd : CVC3::SearchEngineFast
• d_nonlitQueryStart : CVC3::SearchEngineFast
• d_not_not_elim_str : LFSCObj
• d_not_to_iff_str : LFSCObj
• d_notifyEq : CVC3::TheoryCore
• d_notifyList : CVC3::ExprValue
• d_notifyObj : CVC3::ExprManager , CVC3::SmartCDO< T >::RefCDO< U > , CVC3::TheoryCore , CVC3::VariableManager
• d_notifyObjList : CVC3::Context
• d_nullExpr : CVC3::ExprManager , SAT::CNF_Manager
• d_numVars : SAT::CNF_Formula_Impl , SAT::CD_CNF_Formula
• d_offset_multi_trig : CVC3::TheoryQuant
• d_ok : MiniSat::PushEntry , MiniSat::Solver
• d_op : LFSCLraPoly , LFSCLraAxiom , LFSCLraMulC , LFSCLraContra
• d_op1 : LFSCLraAdd , LFSCLraSub
• d_op2 : LFSCLraAdd , LFSCLraSub
• d_opExpr : CVC3::ExprApplyTmp , CVC3::ExprApply
• d_optimized_subst_op_str : LFSCObj
• d_or_final_s : LFSCObj
• d_or_mid_s : LFSCObj
• 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::ExprHashMap< Data >::const_iterator::Proxy , CVC3::CDMap< Key, Data, HashFcn >::iterator::Proxy , CVC3::CDMap< Key, Data, HashFcn >::orderedIterator::Proxy , CVC3::CDMapOrdered< Key, Data >::iterator::Proxy , CVC3::CDMapOrdered< Key, Data >::orderedIterator::Proxy , CVC3::ExprMap< Data >::const_iterator::Proxy , CVC3::ExprMap< Data >::iterator::Proxy , CVC3::ExprHashMap< Data >::iterator::Proxy
• d_parent_list : CVC3::TheoryQuant
• d_parseCache : CVC3::TheoryCore
• d_parseCacheOther : CVC3::TheoryCore
• d_parseCacheTop : CVC3::TheoryCore
• d_parser : CVC3::VCCmd
• d_partCalled : CVC3::TheoryQuant
• d_partTriggers : CVC3::TheoryQuant
• d_partTrigs : CVC3::TheoryQuant
• d_pathLenghtThres : CVC3::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_pf : LFSCLraPoly , LFSCClausify , LFSCAssume , LFSCLraMulC , LFSCLraContra , LFSCProofGeneric
• d_pf_expr : LFSCObj
• d_pfOp : CVC3::TheoremProducer
• d_plus_predicate_str : LFSCObj
• d_pn : LFSCObj
• d_pn_form : LFSCObj
• 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_print_map : LFSCPrinter
• d_print_visited_map : LFSCPrinter
• 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 : SAT::DPLLTMiniSat , CVC3::Proof , SAT::SatProofNode , CVC3::TheoremValue
• d_provesY : TReturn
• d_pushes : MiniSat::Solver
• d_pushID : MiniSat::Clause
• d_pushIDs : MiniSat::Solver
• d_pushLevel : SAT::DPLLTBasic
• d_pushNegCache : CVC3::TheoryBitvector , CVC3::ExprTransform
• d_pv : LFSCPfLet
• d_pvRpl : LFSCPfLet
• 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 : LFSCLraMulC , CVC3::TheoryArith3::FreeConst , CVC3::ExprRational , CVC3::TheoryArithNew::FreeConst , CVC3::TheoryArithOld::FreeConst , LFSCLraAxiom
• 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_real_shadow_eq_str : LFSCObj
• d_real_shadow_str : LFSCObj
• d_realType : CVC3::TheoryArith
• d_realUsed : CVC3::Translator
• d_reason : SAT::Clause , MiniSat::Solver
• d_rebuildCache : CVC3::ExprManager
• d_ref : CVC3::SmartCDO< T >::RefCDO< U >::RefNotifyObj
• d_refcount : CVC3::ClauseValue , CVC3::ExprValue , CVC3::TheoremValue
• d_refCount : CVC3::SmartCDO< T >::RefCDO< U >
• d_refcount : CVC3::VariableValue
• d_refcountOwner : CVC3::ClauseValue
• d_refl_str : LFSCObj
• 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_replaceSymbols : CVC3::Translator
• 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_result : recCompleteInster
• d_rewrite_and_str : LFSCObj
• d_rewrite_eq_refl_str : LFSCObj
• d_rewrite_eq_symm_str : LFSCObj
• d_rewrite_iff_str : LFSCObj
• d_rewrite_iff_symm_str : LFSCObj
• d_rewrite_implies_str : LFSCObj
• d_rewrite_ite_same_str : LFSCObj
• d_rewrite_not_false_str : LFSCObj
• d_rewrite_not_not_str : LFSCObj
• d_rewrite_not_true_str : LFSCObj
• d_rewrite_or_str : LFSCObj
• d_rhs : CVC3::TheoryArithNew::Ineq , CVC3::TheoryArithOld::Ineq , CVC3::RWTheoremValue , CVC3::TheoryArith3::Ineq
• d_right : SAT::SatProofNode
• d_right_minus_left_str : LFSCObj
• d_root : SAT::SatProof
• d_rootLevel : MiniSat::Solver
• d_rules : CVC3::ExprTransform , CVC3::SearchEngine , CVC3::TheoremManager , CVC3::TheoryArithNew , CVC3::TheoryArithOld , CVC3::TheoryArray , CVC3::TheoryCore , CVC3::TheoryDatatype , CVC3::TheoryQuant , CVC3::TheoryRecords , CVC3::TheorySimulate , CVC3::TheoryUF , CVC3::VariableManager , LFSCObj , CVC3::TheoryArith3 , CVC3::TheoryBitvector , SAT::CNF_Manager
• 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::ContextObj , CVC3::VariableValue
• 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_sharedIdx1 : CVC3::TheoryArray , CVC3::TheoryUF
• d_sharedIdx2 : CVC3::TheoryUF , CVC3::TheoryArray
• d_sharedSubterms : CVC3::TheoryBitvector , CVC3::TheoryArray
• d_sharedSubtermsList : CVC3::TheoryArray , CVC3::TheoryBitvector
• d_sharedTerms : CVC3::TheoryArithNew , CVC3::TheoryArith3 , CVC3::TheoryArithOld
• d_sharedTermsList : CVC3::TheoryArithOld
• d_sharedTermsMap : CVC3::TheoryUF
• 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::SearchSimple , CVC3::SearchEngineFast
• 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_source : CVC3::Translator
• d_splitSign : CVC3::TheoryArithOld
• d_splitterAsserted : CVC3::TheoryDatatype
• d_splitterCount : CVC3::SearchEngineFast , CVC3::DecisionEngine
• d_splitters : CVC3::DecisionEngine , CVC3::TheoryDatatype
• d_splittersIndex : CVC3::TheoryDatatype
• d_ss : CVC3::SearchSatCNFCallback , CVC3::SearchSatTheoryAPI , CVC3::SearchSat::Restorer , CVC3::SearchSatCoreSatAPI , CVC3::SearchSatDecider
• d_stackLevel : CVC3::VCL
• d_start : MiniSat::Inference
• d_startLevel : CVC3::DecisionEngineCaching , CVC3::DecisionEngineMBTF
• d_statistics : CVC3::TheoryCore , SAT::CNF_Manager , CVC3::VCL
• d_stats : MiniSat::Solver
• d_status : CVC3::Translator
• d_steps : MiniSat::Inference
• d_str : LFSCProofGeneric , CVC3::ExprString
• d_strict : CVC3::TheoryArithNew::FreeConst , CVC3::TheoryArith3::FreeConst , CVC3::TheoryArithOld::FreeConst
• d_subTermsMap : CVC3::TheoryQuant
• d_t : CVC3::Assumptions::iterator::Proxy
• d_table : Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey > , Hash::hash_set< _Key, _HashFcn, _EqualKey >
• d_tcc : CVC3::VCL::UserAssertion
• d_tccCache : CVC3::TheoryCore
• d_tempBinds : CVC3::TheoryQuant
• d_terms : LFSCObj , CVC3::TheoryCore
• d_termTheorems : CVC3::TheoryCore
• d_testerMap : CVC3::TheoryDatatype
• d_th_trans : LFSCConvert
• d_th_trans_lam : LFSCConvert
• d_th_trans_map : LFSCConvert
• d_thead : MiniSat::PushEntry , MiniSat::Solver
• d_theorem : MiniSat::Clause , SAT::SatProofNode
• d_theorems : CVC3::SearchSat
• d_theories : CVC3::TheoryCore , CVC3::VCL
• d_theoryAPI : CVC3::SearchSat , SAT::DPLLT , MiniSat::Solver
• d_theoryArith : CVC3::ExprTransform , CVC3::Translator , CVC3::ArithTheoremProducer3 , CVC3::VCL , CVC3::ArithTheoremProducerOld , CVC3::ArithTheoremProducer
• d_theoryArray : CVC3::ArrayTheoremProducer , CVC3::Translator , CVC3::VCL
• d_theoryBitvector : CVC3::Translator , CVC3::VCL , CVC3::BitvectorTheoremProducer
• d_theoryCore : CVC3::CompleteInstPreProcessor , CVC3::VCL , CVC3::Theory , CVC3::TheoryCore::CoreNotifyObj , CVC3::Translator
• d_theoryDatatype : CVC3::VCL , CVC3::Translator , CVC3::DatatypeTheoremProducer
• d_theoryExplanations : MiniSat::Solver
• d_theoryMap : CVC3::TheoryCore
• d_theoryQuant : CVC3::Translator , CVC3::QuantTheoremProducer , CVC3::VCL
• d_theoryRecords : CVC3::VCL , CVC3::Translator , CVC3::RecordsTheoremProducer
• d_theorySimulate : CVC3::VCL , CVC3::Translator
• d_theoryUF : CVC3::Translator , CVC3::UFTheoremProducer , CVC3::VCL
• d_theoryUsed : CVC3::Theory
• d_thm : CVC3::VariableValue , CVC3::TheoremValue , CVC3::Theorem , CVC3::Circuit , CVC3::Theorem3 , CVC3::ClauseValue , CVC3::VCL::UserAssertion
• d_thmCount : CVC3::TheoryQuant
• d_timeBase : CVC3::TheoryCore
• d_timeLimit : CVC3::TheoryCore
• d_tlist : CVC3::NotifyList
• d_tm : CVC3::TheoremProducer , CVC3::VCL , CVC3::TheoremValue , CVC3::ExprManager , CVC3::TheoryCore
• d_tmpFile : CVC3::Translator
• d_topLevel : CVC3::DecisionEngineMBTF , CVC3::DecisionEngineCaching
• d_topLevelLock : CVC3::DecisionEngineMBTF , CVC3::DecisionEngineCaching
• 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 : 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::Translator , CVC3::TheoryQuant
• d_translateQueueFlags : SAT::CNF_Manager
• d_translateQueueThms : SAT::CNF_Manager
• d_translateQueueVars : SAT::CNF_Manager
• d_translator : CVC3::TheoryCore , CVC3::VCL
• 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::CacheEntry , CVC3::DecisionEngineMBTF::CacheEntry
• d_trusted : LFSCObj
• d_type : LFSCAssume , 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::ExprBoundVar , CVC3::ParserTemp
• d_uminus_to_mult_str : LFSCObj
• 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_user_assumptions : LFSCPrinter
• 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::Variable , CVC3::VariableValue
• d_value : Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::BucketNode
• d_var : LFSCBoolRes , LFSCLem , CVC3::Literal , LFSCClausify , LFSCAssume , LFSCLraPoly
• d_var_decay : MiniSat::Solver
• d_var_inc : MiniSat::Solver
• d_var_intro_str : LFSCObj
• d_varAssignments : CVC3::TheoryCore
• d_varInfo : SAT::CNF_Manager
• d_varModelMap : CVC3::TheoryCore
• d_vars : CVC3::SearchSat , CVC3::ExprClosure , 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::ClauseValue , CVC3::VariableValue
• d_zeroVar : CVC3::Translator
• dagFlag() : CVC3::ExprStream
• dagPrinting() : CVC3::ExprManager
• darkGrayShadow2ab() : CVC3::ArithProofRules , CVC3::ArithTheoremProducerOld , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducer
• darkGrayShadow2ba() : CVC3::ArithTheoremProducer3 , CVC3::ArithProofRules , CVC3::ArithTheoremProducerOld , CVC3::ArithTheoremProducer
• darkShadow() : CVC3::TheoryArith , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducerOld , CVC3::ArithTheoremProducer3
• Data : Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >
• data : MiniSat::vec< T >
• data_const_iter : Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >
• data_iter : Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >
• data_type : Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >
• dataType() : CVC3::VCL , CVC3::TheoryDatatype , CVC3::ValidityChecker , CVC3::VCL , CVC3::TheoryDatatype , CVC3::ValidityChecker , CVC3::VCL
• datatypeConsExpr() : CVC3::ValidityChecker , CVC3::TheoryDatatype , CVC3::VCL
• datatypeSelExpr() : CVC3::ValidityChecker , CVC3::VCL , CVC3::TheoryDatatype
• datatypeTestExpr() : CVC3::ValidityChecker , CVC3::VCL , CVC3::TheoryDatatype
• DatatypeTheoremProducer() : CVC3::DatatypeTheoremProducer
• Datum : MiniSat::vec< T >
• db_simpl : MiniSat::SolverStats
• debug() : CVC3::TheoryQuant , MiniSat::SolverStats
• debug_conv : LFSCObj
• debug_str : LFSCProofGeneric
• debug_var : LFSCObj
• decide_next_branch() : CSolver
• Decider() : SAT::DPLLT::Decider
• decider() : SAT::DPLLT
• Decision() : MiniSat::Clause
• decision_strategy : CSolverParameters
• DecisionEngine : CVC3::SearchImplBase , CVC3::DecisionEngine
• DecisionEngineCaching() : CVC3::DecisionEngineCaching
• DecisionEngineDFS() : CVC3::DecisionEngineDFS
• DecisionEngineMBTF() : CVC3::DecisionEngineMBTF
• decisionLevel() : MiniSat::Solver
• decisions : MiniSat::SolverStats
• decompose() : CVC3::DatatypeProofRules , CVC3::DatatypeTheoremProducer
• decRefcount() : CVC3::ExprValue
• deduce() : CSolver
• defaultDivideExpr : CVC3::TheoryQuant
• defaultMinusExpr : CVC3::TheoryQuant
• defaultMultExpr : CVC3::TheoryQuant
• defaultPlusExpr : CVC3::TheoryQuant
• defaultPowExpr : CVC3::TheoryQuant
• defaultReadExpr : CVC3::TheoryQuant
• defaultWriteExpr : CVC3::TheoryQuant
• define_skolem_vars() : LFSCObj
• del_clauses : MiniSat::SolverStats
• del_lemmas : MiniSat::SolverStats
• delete_unrelevant_clauses() : CSolver
• DeleteClause() : SatSolver
• deleted() : CVC3::Clause
• deleteData() : CVC3::MemoryManagerMalloc , CVC3::MemoryManager , CVC3::MemoryManagerChunks , CVC3::ContextMemoryManager
• deleteLast() : SAT::CD_CNF_Formula , SAT::CNF_Formula_Impl
• deleteNotifyObj() : CVC3::Context
• deleteParser() : CVC3::Parser
• delNewTrigs() : CVC3::TheoryQuant
• DependenciesMap : CVC3::TheoryArithNew
• dependenciesMap : CVC3::TheoryArithNew
• depth() : CVC3::ExprStream
• Derivation() : MiniSat::Derivation
• deriveClosure() : CVC3::VCL
• deriveGomoryCut() : CVC3::TheoryArithNew
• deriveTheorem() : CVC3::Variable , CVC3::Literal
• deriveThmRec() : CVC3::Variable
• destroy() : CVC3::VCL
• detail_dump_cl() : CDatabase
• dfs() : CVC3::TheoryArithNew::VarOrderGraph , CVC3::TheoryArithOld::VarOrderGraph , CVC3::TheoryArith3::VarOrderGraph , CVC3::TheoryArithOld::VarOrderGraph
• diff_logic_size : CVC3::TheoryArithOld
• DifferenceLogicGraph() : CVC3::TheoryArithOld::DifferenceLogicGraph
• diffLogicGraph : CVC3::TheoryArithOld
• diffLogicOnly : CVC3::TheoryArithOld
• dir() : CVC3::Clause
• direction() : CLitPoolElement
• DisableClauseDeletion() : Xchaff , SatSolver
• diseqSplitAlready : CVC3::TheoryArithOld
• diseqToIneq() : CVC3::ArithTheoremProducer , CVC3::ArithProofRules , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld
• display() : CVC3::CLFlag
• distinctExpr() : CVC3::ValidityChecker , CVC3::VCL
• distributive_rule() : CVC3::BitvectorTheoremProducer , CVC3::BitvectorProofRules
• divideEqnNonConst() : CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducerOld , CVC3::ArithTheoremProducer3 , CVC3::ArithProofRules
• divideExpr() : CVC3::ValidityChecker , CVC3::VCL
• dlevel() : CSolver , CVariable
• do_bso() : LFSCConvert
• doackermann() : CVC3::ExprTransform
• dobryant() : CVC3::ExprTransform
• done : CVC3::ParserTemp , CVC3::Parser
• dontBuffer : CVC3::TheoryArithOld
• doPops() : MiniSat::Solver
• doSolve() : CVC3::TheoryArith3 , CVC3::TheoryArithNew , CVC3::TheoryArithOld
• DPLLT() : SAT::DPLLT
• DPLLTBasic() : SAT::DPLLTBasic
• DPLLTMiniSat() : SAT::DPLLTMiniSat
• dummyTheorem() : CVC3::ArithTheoremProducerOld , CVC3::DatatypeProofRules , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducer , CVC3::CoreTheoremProducer , CVC3::DatatypeTheoremProducer , CVC3::ArithProofRules , CVC3::CoreProofRules
• dump() : CSolver , CLitPoolElement , CVC3::Translator , CClause , CVariable , CDatabase
• dump_assignment_stack() : CSolver
• dumpAssertion() : CVC3::Translator
• dumpQuery() : CVC3::Translator
• dumpQueryResult() : CVC3::Translator
• DynamicFlagsEnum : CVC3::Expr
• dynTrig() : CVC3::dynTrig