CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
Class List
Class Index
Class Hierarchy
Class Members
SAT
DPLLTBasic
SAT::DPLLTBasic Member List
This is the complete list of members for
SAT::DPLLTBasic
, including all inherited members.
addAssertion
(const CNF_Formula &cnf)
SAT::DPLLTBasic
virtual
addNewClause
(const Clause &c)
SAT::DPLLTBasic
addNewClauses
(CNF_Formula_Impl &cnf)
SAT::DPLLTBasic
checkSat
(const CNF_Formula &cnf)
SAT::DPLLTBasic
virtual
CONSISTENT
enum value
SAT::DPLLT
ConsistentResult
enum name
SAT::DPLLT
continueCheck
(const CNF_Formula &cnf)
SAT::DPLLTBasic
virtual
createManager
()
SAT::DPLLTBasic
private
cvc2SAT
(Lit l)
SAT::DPLLTBasic
inline
d_assertions
SAT::DPLLTBasic
private
d_assertionsStack
SAT::DPLLTBasic
private
d_cm
SAT::DPLLTBasic
private
d_cnf
SAT::DPLLTBasic
private
d_cnfStack
SAT::DPLLTBasic
private
d_decider
SAT::DPLLT
protected
d_mng
SAT::DPLLTBasic
private
d_mngStack
SAT::DPLLTBasic
private
d_prevAStackSize
SAT::DPLLTBasic
private
d_prevStackSize
SAT::DPLLTBasic
private
d_printStats
SAT::DPLLTBasic
private
d_pushLevel
SAT::DPLLTBasic
private
d_ready
SAT::DPLLTBasic
private
d_readyPrev
SAT::DPLLTBasic
private
d_theoryAPI
SAT::DPLLT
protected
decider
()
SAT::DPLLT
inline
DPLLT
(TheoryAPI *theoryAPI, Decider *decider)
SAT::DPLLT
inline
DPLLTBasic
(TheoryAPI *theoryAPI, Decider *decider, CVC3::ContextManager *cm, bool printStats=false)
SAT::DPLLTBasic
generate_CDB
(CNF_Formula_Impl &cnf)
SAT::DPLLTBasic
private
getCurAssignments
()
SAT::DPLLTBasic
virtual
getCurClauses
()
SAT::DPLLTBasic
virtual
getSatProof
(CNF_Manager *, CVC3::TheoryCore *)
SAT::DPLLTBasic
virtual
getValue
(Var v)
SAT::DPLLTBasic
inline
virtual
handle_result
(SatSolver::SATStatus outcome)
SAT::DPLLTBasic
private
INCONSISTENT
enum value
SAT::DPLLT
MAYBE_CONSISTENT
enum value
SAT::DPLLT
pop
()
SAT::DPLLTBasic
virtual
push
()
SAT::DPLLTBasic
virtual
SAT2cvc
(SatSolver::Lit l)
SAT::DPLLTBasic
inline
satSolver
()
SAT::DPLLTBasic
inline
setDecider
(Decider *decider)
SAT::DPLLT
inline
theoryAPI
()
SAT::DPLLT
inline
verify_solution
()
SAT::DPLLTBasic
private
~DPLLT
()
SAT::DPLLT
inline
virtual
~DPLLTBasic
()
SAT::DPLLTBasic
virtual
Generated on Mon Sep 15 2014 15:01:11 for CVC3 by
1.8.7