- d -

• dagFlag() : CVC3::ExprStream
• dagPrinting() : CVC3::ExprManager
• darkGrayShadow2ab() : CVC3::ArithProofRules , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducerOld
• darkGrayShadow2ba() : CVC3::ArithProofRules , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducerOld
• darkShadow() : CVC3::TheoryArith , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducerOld
• dataType() : CVC3::VCL , CVC3::TheoryDatatype , CVC3::ValidityChecker
• datatypeConsExpr() : CVC3::VCL , CVC3::TheoryDatatype , CVC3::ValidityChecker
• datatypeSelExpr() : CVC3::VCL , CVC3::TheoryDatatype , CVC3::ValidityChecker
• datatypeTestExpr() : CVC3::VCL , CVC3::TheoryDatatype , CVC3::ValidityChecker
• DatatypeTheoremProducer() : CVC3::DatatypeTheoremProducer
• Debug() : CVC3::Debug
• DebugCounter() : CVC3::DebugCounter
• DebugException() : CVC3::DebugException
• DebugFlag() : CVC3::DebugFlag
• DebugTime() : CVC3::DebugTime
• DebugTimer() : CVC3::DebugTimer
• decide_next_branch() : CSolver
• decider() : SAT::DPLLT
• Decider() : SAT::DPLLT::Decider
• Decision() : MiniSat::Clause
• DecisionEngine() : CVC3::DecisionEngine
• DecisionEngineCaching() : CVC3::DecisionEngineCaching
• DecisionEngineDFS() : CVC3::DecisionEngineDFS
• DecisionEngineMBTF() : CVC3::DecisionEngineMBTF
• decisionLevel() : MiniSat::Solver
• decompose() : CVC3::DatatypeTheoremProducer , CVC3::DatatypeProofRules
• decRefcount() : CVC3::ExprValue
• deduce() : CSolver
• delete_unrelevant_clauses() : CSolver
• DeleteClause() : SatSolver
• deleted() : CVC3::Clause
• deleteData() : CVC3::MemoryManager , CVC3::MemoryManagerChunks , CVC3::ContextMemoryManager , CVC3::MemoryManagerMalloc
• deleteLast() : SAT::CD_CNF_Formula , SAT::CNF_Formula_Impl
• deleteNotifyObj() : CVC3::Context
• deleteParser() : CVC3::Parser
• delNewTrigs() : CVC3::TheoryQuant
• depth() : CVC3::ExprStream
• Derivation() : MiniSat::Derivation
• deriveClosure() : CVC3::VCL
• deriveGomoryCut() : CVC3::TheoryArithNew
• deriveTheorem() : CVC3::Variable , CVC3::Literal
• deriveThmRec() : CVC3::Variable
• detail_dump_cl() : CDatabase
• dfs() : CVC3::TheoryArithNew::VarOrderGraph , CVC3::TheoryArithOld::VarOrderGraph
• difference() : CVC3::TheoryCore
• dir() : CVC3::Clause
• direction() : CLitPoolElement
• DisableClauseDeletion() : Xchaff , SatSolver
• diseqToIneq() : CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducerOld , CVC3::ArithProofRules
• divideExpr() : CVC3::VCL , CVC3::ValidityChecker
• dlevel() : CSolver , CVariable
• done() : CVC3::Parser
• doPops() : MiniSat::Solver
• doSolve() : CVC3::TheoryArithNew , CVC3::TheoryArithOld , CVC3::TheoryArithNew
• DPLLT() : SAT::DPLLT
• DPLLTBasic() : SAT::DPLLTBasic
• DPLLTMiniSat() : SAT::DPLLTMiniSat
• dummyTheorem() : CVC3::ArithProofRules , CVC3::DatatypeTheoremProducer , CVC3::DatatypeProofRules , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducerOld
• dump() : CLitPoolElement , CClause , CDatabase , CVariable , CVC3::Translator , CSolver
• dump_assignment_stack() : CSolver
• dumpAssertion() : CVC3::Translator
• dumpQuery() : CVC3::Translator
• dumpQueryResult() : CVC3::Translator
• dumpTrace() : CVC3::VCL , CVC3::Debug
• dynTrig() : CVC3::dynTrig

---