- d -

• dagFlag() : CVC3::ExprStream
• dagPrinting() : CVC3::ExprManager
• darkGrayShadow2ab() : CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithProofRules , CVC3::ArithTheoremProducerOld
• darkGrayShadow2ba() : CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld , CVC3::ArithProofRules
• darkShadow() : CVC3::TheoryArith , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld
• dataType() : CVC3::TheoryDatatype , CVC3::ValidityChecker , CVC3::VCL , CVC3::TheoryDatatype
• datatypeConsExpr() : CVC3::TheoryDatatype , CVC3::ValidityChecker , CVC3::VCL
• datatypeSelExpr() : CVC3::TheoryDatatype , CVC3::ValidityChecker , CVC3::VCL
• datatypeTestExpr() : CVC3::TheoryDatatype , CVC3::ValidityChecker , CVC3::VCL
• DatatypeTheoremProducer() : CVC3::DatatypeTheoremProducer
• debug() : CVC3::TheoryQuant
• decide_next_branch() : CSolver
• Decider() : SAT::DPLLT::Decider
• decider() : SAT::DPLLT
• 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
• deduce() : CSolver
• define_skolem_vars() : LFSCObj
• delete_unrelevant_clauses() : CSolver
• 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::Variable , CVC3::Literal
• deriveThmRec() : CVC3::Variable
• destroy() : CVC3::VCL
• detail_dump_cl() : CDatabase
• dfs() : CVC3::TheoryArith3::VarOrderGraph , CVC3::TheoryArithOld::VarOrderGraph , CVC3::TheoryArithNew::VarOrderGraph
• DifferenceLogicGraph() : CVC3::TheoryArithOld::DifferenceLogicGraph
• dir() : CVC3::Clause
• direction() : CLitPoolElement
• DisableClauseDeletion() : SatSolver , Xchaff
• diseqToIneq() : CVC3::ArithProofRules , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld
• display() : CVC3::CLFlag
• distinctExpr() : CVC3::ValidityChecker , CVC3::VCL
• distributive_rule() : CVC3::BitvectorProofRules , CVC3::BitvectorTheoremProducer
• divideEqnNonConst() : CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducer , CVC3::ArithProofRules , CVC3::ArithTheoremProducerOld
• divideExpr() : CVC3::ValidityChecker , CVC3::VCL
• dlevel() : CVariable , CSolver
• do_bso() : LFSCConvert
• doackermann() : CVC3::ExprTransform
• dobryant() : CVC3::ExprTransform
• done() : CVC3::Parser
• doPops() : MiniSat::Solver
• doSolve() : CVC3::TheoryArith3 , CVC3::TheoryArithNew , CVC3::TheoryArithOld
• DPLLT() : SAT::DPLLT
• DPLLTBasic() : SAT::DPLLTBasic
• DPLLTMiniSat() : SAT::DPLLTMiniSat
• dummyTheorem() : CVC3::DatatypeTheoremProducer , CVC3::ArithProofRules , CVC3::ArithTheoremProducerOld , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducer , CVC3::CoreProofRules , CVC3::CoreTheoremProducer , CVC3::DatatypeProofRules
• dump() : CVC3::Translator , CDatabase , CLitPoolElement , CVariable , CSolver , CClause
• dump_assignment_stack() : CSolver
• dumpAssertion() : CVC3::Translator
• dumpQuery() : CVC3::Translator
• dumpQueryResult() : CVC3::Translator
• dynTrig() : CVC3::dynTrig