SAT::CD_CNF_Formula Class Reference

#include <cnf.h>

Inheritance diagram for SAT::CD_CNF_Formula:

[legend]

Collaboration diagram for SAT::CD_CNF_Formula:

[legend]

List of all members.

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

Detailed Description

Definition at line 171 of file cnf.h.

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.

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]

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

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 CVC3::SearchSat::check(), CVC3::SearchSat::checkConsistent(), SAT::DPLLTBasic::checkSat(), SAT::DPLLTBasic::continueCheck(), and CVC3::SearchSat::getNewClauses().

void SAT::CD_CNF_Formula::deleteLast ( ) [inline]

Definition at line 187 of file cnf.h.

References d_formula, and CVC3::CDList< T >::pop_back().

Referenced by CVC3::SearchSat::getNewClauses().

void CD_CNF_Formula::newClause ( ) [virtual]

Implements SAT::CNF_Formula.

Definition at line 183 of file cnf.cpp.

References SAT::CNF_Formula::d_current, d_formula, and CVC3::CDList< T >::push_back().

void CD_CNF_Formula::registerUnit ( ) [virtual]

Implements SAT::CNF_Formula.

Definition at line 190 of file cnf.cpp.

References SAT::CNF_Formula::d_current, DebugAssert, SAT::Clause::setUnit(), and SAT::Clause::size().

Member Data Documentation

CVC3::CDList<Clause> SAT::CD_CNF_Formula::d_formula [private]

Definition at line 172 of file cnf.h.

Referenced by begin(), deleteLast(), empty(), end(), newClause(), 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().

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