CVC3
2.4.1
|
#include <cnf.h>
SAT::CNF_Formula_Impl::CNF_Formula_Impl | ( | const CNF_Formula & | cnf | ) | [inline] |
Definition at line 153 of file cnf.h.
References SAT::CNF_Formula::copy().
void SAT::CNF_Formula_Impl::setNumVars | ( | unsigned | numVars | ) | [inline, private, virtual] |
Implements SAT::CNF_Formula.
bool SAT::CNF_Formula_Impl::empty | ( | ) | const [inline, virtual] |
const Clause& SAT::CNF_Formula_Impl::operator[] | ( | int | i | ) | const [inline, virtual] |
const_iterator SAT::CNF_Formula_Impl::begin | ( | ) | const [inline, virtual] |
Implements SAT::CNF_Formula.
Definition at line 158 of file cnf.h.
References d_formula.
Referenced by SAT::DPLLTBasic::generate_CDB(), and SAT::DPLLTBasic::addNewClauses().
const_iterator SAT::CNF_Formula_Impl::end | ( | ) | const [inline, virtual] |
Implements SAT::CNF_Formula.
Definition at line 159 of file cnf.h.
References d_formula.
Referenced by SAT::DPLLTBasic::generate_CDB(), and SAT::DPLLTBasic::addNewClauses().
unsigned SAT::CNF_Formula_Impl::numVars | ( | ) | const [inline, virtual] |
Implements SAT::CNF_Formula.
Definition at line 160 of file cnf.h.
References d_numVars.
Referenced by setNumVars(), SAT::DPLLTBasic::generate_CDB(), and SAT::DPLLTBasic::addNewClauses().
unsigned SAT::CNF_Formula_Impl::numClauses | ( | ) | const [inline, virtual] |
void SAT::CNF_Formula_Impl::deleteLast | ( | ) | [inline] |
Definition at line 162 of file cnf.h.
References DebugAssert, and d_formula.
Referenced by CVC3::SearchSat::newUserAssumptionIntHelper().
void CNF_Formula_Impl::newClause | ( | ) | [virtual] |
Implements SAT::CNF_Formula.
Definition at line 137 of file cnf.cpp.
Referenced by SAT::DPLLTBasic::checkSat().
void CNF_Formula_Impl::registerUnit | ( | ) | [virtual] |
Implements SAT::CNF_Formula.
Definition at line 144 of file cnf.cpp.
References DebugAssert, and SAT::Lit::getID().
void CNF_Formula_Impl::simplify | ( | ) |
Definition at line 153 of file cnf.cpp.
References Hash::hash_map::find(), and Hash::hash_map::end().
Referenced by SAT::DPLLTBasic::generate_CDB(), and SAT::DPLLTBasic::addNewClauses().
void CNF_Formula_Impl::reset | ( | ) |
Definition at line 174 of file cnf.cpp.
Referenced by SATDeductionHook(), MiniSat::Solver::search(), and MiniSat::Solver::push().
std::hash_map<int, bool> SAT::CNF_Formula_Impl::d_lits [private] |
std::deque<Clause> SAT::CNF_Formula_Impl::d_formula [private] |
Definition at line 147 of file cnf.h.
Referenced by empty(), operator[](), begin(), end(), numClauses(), and deleteLast().
unsigned SAT::CNF_Formula_Impl::d_numVars [private] |
Definition at line 148 of file cnf.h.
Referenced by setNumVars(), and numVars().