SAT::CD_CNF_Formula Class Reference

#include <cnf.h>

Inherits SAT::CNF_Formula.

Collaboration diagram for SAT::CD_CNF_Formula:

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 172 of file cnf.h.

---

Constructor & Destructor Documentation

SAT::CD_CNF_Formula::CD_CNF_Formula

(

CVC3::Context *

context

)

[inline]

Definition at line 178 of file cnf.h.

SAT::CD_CNF_Formula::~CD_CNF_Formula

(

)

[inline]

Definition at line 180 of file cnf.h.

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

---

Member Function Documentation

void SAT::CD_CNF_Formula::setNumVars

(

unsigned

numVars

)

[inline, private, virtual]

Implements SAT::CNF_Formula.

Definition at line 176 of file cnf.h.

bool SAT::CD_CNF_Formula::empty

(

)

const [inline, virtual]

Implements SAT::CNF_Formula.

Definition at line 182 of file cnf.h.

References d_formula.

const Clause& SAT::CD_CNF_Formula::operator[]

(

int

i

)

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::begin

(

)

const [inline, virtual]

Implements SAT::CNF_Formula.

Definition at line 184 of file cnf.h.

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

const_iterator SAT::CD_CNF_Formula::end

(

)

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::numVars

(

)

const [inline, virtual]

Implements SAT::CNF_Formula.

Definition at line 186 of file cnf.h.

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

unsigned SAT::CD_CNF_Formula::numClauses

(

)

const [inline, virtual]

Implements SAT::CNF_Formula.

Definition at line 187 of file cnf.h.

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

Referenced by SAT::DPLLTBasic::checkSat(), and SAT::DPLLTBasic::continueCheck().

void SAT::CD_CNF_Formula::deleteLast

(

)

[inline]

Definition at line 188 of file cnf.h.

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 173 of file cnf.h.

Referenced by begin(), empty(), numClauses(), numVars(), operator[](), and ~CD_CNF_Formula().

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

Definition at line 174 of file cnf.h.

Referenced by end().

---

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

• cnf.h
• cnf.cpp