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.

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:

• cnf.h
• cnf.cpp

---