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 (CVCL::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 newClause ()
• void registerUnit ()

Private Member Functions

• void setNumVars (unsigned numVars)

Private Attributes

• CVCL::CDList< Clause > d_formula
• CVCL::CDO< unsigned > d_numVars

---

Detailed Description

Definition at line 155 of file cnf.h.

---

Constructor & Destructor Documentation

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

Definition at line 161 of file cnf.h.

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

Definition at line 163 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 159 of file cnf.h. References d_numVars.

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

Implements SAT::CNF_Formula. Definition at line 165 of file cnf.h. References d_formula, and CVCL::CDList< T >::empty().

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

Implements SAT::CNF_Formula. Definition at line 166 of file cnf.h. References d_formula.

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

Implements SAT::CNF_Formula. Definition at line 167 of file cnf.h. References CVCL::CDList< T >::begin(), and d_formula.

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

Implements SAT::CNF_Formula. Definition at line 168 of file cnf.h. References d_formula, and CVCL::CDList< T >::end().

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

Implements SAT::CNF_Formula. Definition at line 169 of file cnf.h. References d_numVars, and CVCL::CDO< T >::get(). Referenced by CVCL::SearchSat::addLemma().

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

Implements SAT::CNF_Formula. Definition at line 170 of file cnf.h. References d_formula, and CVCL::CDList< T >::size(). Referenced by CVCL::SearchSat::check(), and CVCL::SearchSat::getNewClauses().

void CD_CNF_Formula::newClause (   )  [virtual]

Implements SAT::CNF_Formula. Definition at line 157 of file cnf.cpp. References SAT::CNF_Formula::d_current, d_formula, and CVCL::CDList< T >::push_back().

void CD_CNF_Formula::registerUnit (   )  [virtual]

Implements SAT::CNF_Formula. Definition at line 164 of file cnf.cpp. References SAT::CNF_Formula::d_current, SAT::Clause::setUnit(), and SAT::Clause::size().

---

Member Data Documentation

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

Definition at line 156 of file cnf.h. Referenced by begin(), empty(), end(), newClause(), numClauses(), and operator[]().

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

Definition at line 157 of file cnf.h. Referenced by numVars(), and setNumVars().

---

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

• cnf.h
• cnf.cpp

---