CVC3  2.4.1
Public Member Functions | Private Member Functions | Private Attributes | List of all members
SAT::CD_CNF_Formula Class Reference

#include <cnf.h>

Inheritance diagram for SAT::CD_CNF_Formula:
SAT::CNF_Formula

Public Member Functions

 CD_CNF_Formula (CVC3::Context *context)
 
 ~CD_CNF_Formula ()
 
bool empty () const
 
const Clauseoperator[] (int i) const
 
const_iterator begin () const
 
const_iterator end () const
 
unsigned numVars () const
 
unsigned numClauses () const
 
void deleteLast ()
 
void newClause ()
 
void registerUnit ()
 
- Public Member Functions inherited from SAT::CNF_Formula
 CNF_Formula ()
 
virtual ~CNF_Formula ()
 
void addLiteral (Lit l, bool invert=false)
 
ClausegetCurrentClause ()
 
void print () const
 
const CNF_Formulaoperator+= (const CNF_Formula &cnf)
 
const CNF_Formulaoperator+= (const Clause &c)
 

Private Member Functions

void setNumVars (unsigned numVars)
 

Private Attributes

CVC3::CDList< Claused_formula
 
CVC3::CDO< unsigned > d_numVars
 

Additional Inherited Members

- Public Types inherited from SAT::CNF_Formula
typedef std::deque< Clause >
::const_iterator 
const_iterator
 
- Protected Member Functions inherited from SAT::CNF_Formula
void copy (const CNF_Formula &cnf)
 
- Protected Attributes inherited from SAT::CNF_Formula
Claused_current
 

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)
inlineprivatevirtual

Implements SAT::CNF_Formula.

Definition at line 175 of file cnf.h.

References d_numVars, and numVars().

bool SAT::CD_CNF_Formula::empty ( ) const
inlinevirtual

Implements SAT::CNF_Formula.

Definition at line 181 of file cnf.h.

References d_formula.

const Clause& SAT::CD_CNF_Formula::operator[] ( int  i) const
inlinevirtual

Implements SAT::CNF_Formula.

Definition at line 182 of file cnf.h.

References d_formula.

const_iterator SAT::CD_CNF_Formula::begin ( ) const
inlinevirtual

Implements SAT::CNF_Formula.

Definition at line 183 of file cnf.h.

References d_formula.

const_iterator SAT::CD_CNF_Formula::end ( ) const
inlinevirtual

Implements SAT::CNF_Formula.

Definition at line 184 of file cnf.h.

References d_formula.

unsigned SAT::CD_CNF_Formula::numVars ( ) const
inlinevirtual

Implements SAT::CNF_Formula.

Definition at line 185 of file cnf.h.

References d_numVars, and CVC3::CDO< T >::get().

Referenced by setNumVars().

unsigned SAT::CD_CNF_Formula::numClauses ( ) const
inlinevirtual

Implements SAT::CNF_Formula.

Definition at line 186 of file cnf.h.

References d_formula.

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

void SAT::CD_CNF_Formula::deleteLast ( )
inline

Definition at line 187 of file cnf.h.

References d_formula.

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

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