SAT::CD_CNF_Formula Class Reference

#include <cnf.h>

Inheritance diagram for SAT::CD_CNF_Formula:

Inheritance graph
[legend]
Collaboration diagram for SAT::CD_CNF_Formula:

Collaboration graph
[legend]
List of all members.

Public Member Functions

Private Member Functions

Private Attributes


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.

bool SAT::CD_CNF_Formula::empty (  )  const [inline, virtual]

Implements SAT::CNF_Formula.

Definition at line 181 of file cnf.h.

const Clause& SAT::CD_CNF_Formula::operator[] ( int  i  )  const [inline, virtual]

Implements SAT::CNF_Formula.

Definition at line 182 of file cnf.h.

const_iterator SAT::CD_CNF_Formula::begin (  )  const [inline, virtual]

Implements SAT::CNF_Formula.

Definition at line 183 of file cnf.h.

const_iterator SAT::CD_CNF_Formula::end (  )  const [inline, virtual]

Implements SAT::CNF_Formula.

Definition at line 184 of file cnf.h.

unsigned SAT::CD_CNF_Formula::numVars (  )  const [inline, virtual]

Implements SAT::CNF_Formula.

Definition at line 185 of file cnf.h.

unsigned SAT::CD_CNF_Formula::numClauses (  )  const [inline, virtual]

Implements SAT::CNF_Formula.

Definition at line 186 of file cnf.h.

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.

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

CVC3::CDO<unsigned> SAT::CD_CNF_Formula::d_numVars [private]

Definition at line 173 of file cnf.h.


The documentation for this class was generated from the following files:
Generated on Wed Nov 18 16:18:52 2009 for CVC3 by  doxygen 1.5.2