CVC3
2.4.1
|
#include <cnf.h>
SAT::CD_CNF_Formula::CD_CNF_Formula | ( | CVC3::Context * | context | ) | [inline] |
SAT::CD_CNF_Formula::~CD_CNF_Formula | ( | ) | [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< T >::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 CVC3::CDList< T >::begin(), and d_formula.
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< T >::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< T >::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< T >::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< T >::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 begin(), deleteLast(), empty(), end(), numClauses(), and operator[]().
CVC3::CDO<unsigned> SAT::CD_CNF_Formula::d_numVars [private] |
Definition at line 173 of file cnf.h.
Referenced by numVars(), and setNumVars().