CVC3: SAT::CD_CNF_Formula Class Reference

CVC3

#include <cnf.h>

Inherits SAT::CNF_Formula.

Collaboration diagram for SAT::CD_CNF_Formula:

Collaboration graph

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

Public Member Functions inherited from SAT::CNF_Formula
	CNF_Formula ()

virtual	~CNF_Formula ()

void	addLiteral (Lit l, bool invert=false)

Clause &	getCurrentClause ()

void	print () const

const CNF_Formula &	operator+= (const CNF_Formula &cnf)

const CNF_Formula &	operator+= (const Clause &c)

Private Member Functions
void	setNumVars (unsigned numVars)

Private Attributes
CVC3::CDList< Clause >	d_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
Clause *	d_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, and CVC3::CDList< T >::empty().

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 CVC3::CDList< T >::begin(), and 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, and CVC3::CDList< T >::end().

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, and CVC3::CDList< T >::size().

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, and CVC3::CDList< T >::pop_back().

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: