CVC3
2.4.1
|
#include <cnf.h>
SAT::CD_CNF_Formula::CD_CNF_Formula | ( | CVC3::Context * | context | ) | [inline] |
void SAT::CD_CNF_Formula::setNumVars | ( | unsigned | numVars | ) | [inline, private, virtual] |
Implements SAT::CNF_Formula.
bool SAT::CD_CNF_Formula::empty | ( | ) | const [inline, virtual] |
Implements SAT::CNF_Formula.
Definition at line 181 of file cnf.h.
References d_formula, and CVC3::CDList::empty().
const Clause& SAT::CD_CNF_Formula::operator[] | ( | int | i | ) | const [inline, virtual] |
const_iterator SAT::CD_CNF_Formula::begin | ( | ) | const [inline, virtual] |
Implements SAT::CNF_Formula.
Definition at line 183 of file cnf.h.
References d_formula, and CVC3::CDList::begin().
const_iterator SAT::CD_CNF_Formula::end | ( | ) | const [inline, virtual] |
Implements SAT::CNF_Formula.
Definition at line 184 of file cnf.h.
References d_formula, and CVC3::CDList::end().
unsigned SAT::CD_CNF_Formula::numVars | ( | ) | const [inline, virtual] |
Implements SAT::CNF_Formula.
Definition at line 185 of file cnf.h.
References d_numVars, and CVC3::CDO::get().
Referenced by setNumVars().
unsigned SAT::CD_CNF_Formula::numClauses | ( | ) | const [inline, virtual] |
Implements SAT::CNF_Formula.
Definition at line 186 of file cnf.h.
References d_formula, and CVC3::CDList::size().
Referenced by SAT::DPLLTBasic::checkSat(), and SAT::DPLLTBasic::continueCheck().
void SAT::CD_CNF_Formula::deleteLast | ( | ) | [inline] |
Definition at line 187 of file cnf.h.
References d_formula, and CVC3::CDList::pop_back().
void CD_CNF_Formula::newClause | ( | ) | [virtual] |
Implements SAT::CNF_Formula.
void CD_CNF_Formula::registerUnit | ( | ) | [virtual] |
CVC3::CDList<Clause> SAT::CD_CNF_Formula::d_formula [private] |
Definition at line 172 of file cnf.h.
Referenced by empty(), operator[](), begin(), end(), numClauses(), and deleteLast().
CVC3::CDO<unsigned> SAT::CD_CNF_Formula::d_numVars [private] |
Definition at line 173 of file cnf.h.
Referenced by setNumVars(), and numVars().