#include <cnf.h>

Inheritance diagram for SAT::CD_CNF_Formula:

Public Member Functions

CD_CNF_Formula (CVC3::Context *context)
~CD_CNF_Formula ()
bool empty () const
const Clause & operator[] (int i) const
const_iterator begin () const
const_iterator end () const
unsigned numVars () const
unsigned numClauses () const
void deleteLast ()
void newClause ()
void registerUnit ()

Private Member Functions

void setNumVars (unsigned numVars)

Private Attributes

CVC3::CDList< Clause > d_formula
CVC3::CDO< unsigned > d_numVars

Constructor & Destructor Documentation

SAT::CD_CNF_Formula::CD_CNF_Formula ( CVC3::Context * context ) [inline]

Definition at line 177 of file cnf.h.

SAT::CD_CNF_Formula::~CD_CNF_Formula ( ) [inline]

Definition at line 179 of file cnf.h.

Member Function Documentation

void SAT::CD_CNF_Formula::setNumVars ( unsigned numVars ) [inline, private, virtual]

Implements SAT::CNF_Formula.

Definition at line 175 of file cnf.h.

References d_numVars, and numVars().

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]

Implements SAT::CNF_Formula.

Definition at line 182 of file cnf.h.

References d_formula.

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.

Definition at line 183 of file cnf.cpp.

void CD_CNF_Formula::registerUnit ( ) [virtual]

Implements SAT::CNF_Formula.

Definition at line 190 of file cnf.cpp.

References DebugAssert.

Member Data Documentation

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().

The documentation for this class was generated from the following files: