- d -

• dagFlag() : CVC3::ExprStream
• dagPrinting() : CVC3::ExprManager
• darkGrayShadow2ab() : CVC3::ArithProofRules , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld
• darkGrayShadow2ba() : CVC3::ArithProofRules , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld
• darkShadow() : CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::TheoryArith , CVC3::ArithTheoremProducerOld
• dataType() : CVC3::TheoryDatatype , CVC3::VCL , CVC3::TheoryDatatype , CVC3::ValidityChecker , CVC3::VCL
• 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::TheoryQuant
• 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::DatatypeProofRules , CVC3::DatatypeTheoremProducer
• decRefcount() : CVC3::ExprValue
• DeleteClause() : SatSolver
• deleted() : CVC3::Clause
• deleteData() : CVC3::MemoryManager , CVC3::MemoryManagerChunks , CVC3::ContextMemoryManager , CVC3::MemoryManagerMalloc
• deleteLast() : SAT::CNF_Formula_Impl , SAT::CD_CNF_Formula
• deleteNotifyObj() : CVC3::Context
• deleteParser() : CVC3::Parser
• delNewTrigs() : CVC3::TheoryQuant
• depth() : CVC3::ExprStream
• Derivation() : MiniSat::Derivation
• deriveClosure() : CVC3::VCL
• deriveGomoryCut() : CVC3::TheoryArithNew
• deriveTheorem() : CVC3::Literal , CVC3::Variable
• deriveThmRec() : CVC3::Variable
• destroy() : CVC3::VCL
• dfs() : CVC3::TheoryArithNew::VarOrderGraph , CVC3::TheoryArithOld::VarOrderGraph , CVC3::TheoryArith3::VarOrderGraph
• DifferenceLogicGraph() : CVC3::TheoryArithOld::DifferenceLogicGraph
• dir() : CVC3::Clause
• DisableClauseDeletion() : SatSolver
• diseqToIneq() : CVC3::ArithProofRules , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld
• display() : CVC3::CLFlag
• distinctExpr() : CVC3::VCL , CVC3::ValidityChecker
• distributive_rule() : CVC3::BitvectorProofRules , CVC3::BitvectorTheoremProducer
• divideEqnNonConst() : CVC3::ArithProofRules , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld
• divideExpr() : CVC3::ValidityChecker , CVC3::VCL
• doackermann() : CVC3::ExprTransform
• dobryant() : CVC3::ExprTransform
• done() : CVC3::Parser
• doPops() : MiniSat::Solver
• doSolve() : CVC3::TheoryArithNew , CVC3::TheoryArithOld , CVC3::TheoryArith3
• DPLLT() : SAT::DPLLT
• DPLLTBasic() : SAT::DPLLTBasic
• DPLLTMiniSat() : SAT::DPLLTMiniSat
• dummyTheorem() : CVC3::DatatypeProofRules , CVC3::CoreProofRules , CVC3::ArithTheoremProducerOld , CVC3::DatatypeTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducer , CVC3::CoreTheoremProducer , CVC3::ArithProofRules
• dump() : CVC3::Translator
• dumpAssertion() : CVC3::Translator
• dumpQuery() : CVC3::Translator
• dumpQueryResult() : CVC3::Translator
• dynTrig() : CVC3::dynTrig

---