CVC3: SAT::CNF_Formula_Impl Class Reference

CVC3

#include <cnf.h>

Inherits SAT::CNF_Formula.

Collaboration diagram for SAT::CNF_Formula_Impl:

Collaboration graph

Public Member Functions
	CNF_Formula_Impl ()

	CNF_Formula_Impl (const CNF_Formula &cnf)

	~CNF_Formula_Impl ()

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

void	simplify ()

void	reset ()

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
std::hash_map< int, bool >	d_lits

std::deque< Clause >	d_formula

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

Constructor & Destructor Documentation

SAT::CNF_Formula_Impl::CNF_Formula_Impl ( )

inline

Definition at line 152 of file cnf.h.

SAT::CNF_Formula_Impl::CNF_Formula_Impl ( const CNF_Formula & cnf )

inline

Definition at line 153 of file cnf.h.

References SAT::CNF_Formula::copy().

SAT::CNF_Formula_Impl::~CNF_Formula_Impl ( )

inline

Definition at line 154 of file cnf.h.

Member Function Documentation

void SAT::CNF_Formula_Impl::setNumVars ( unsigned numVars )

inlineprivatevirtual

Implements SAT::CNF_Formula.

Definition at line 150 of file cnf.h.

References d_numVars, and numVars().

bool SAT::CNF_Formula_Impl::empty ( ) const

inlinevirtual

Implements SAT::CNF_Formula.

Definition at line 156 of file cnf.h.

References d_formula.

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

inlinevirtual

Implements SAT::CNF_Formula.

Definition at line 157 of file cnf.h.

References d_formula.

const_iterator SAT::CNF_Formula_Impl::begin ( ) const

inlinevirtual

Implements SAT::CNF_Formula.

Definition at line 158 of file cnf.h.

References d_formula.

Referenced by SAT::DPLLTBasic::addNewClauses(), and SAT::DPLLTBasic::generate_CDB().

const_iterator SAT::CNF_Formula_Impl::end ( ) const

inlinevirtual

Implements SAT::CNF_Formula.

Definition at line 159 of file cnf.h.

References d_formula.

Referenced by SAT::DPLLTBasic::addNewClauses(), and SAT::DPLLTBasic::generate_CDB().

unsigned SAT::CNF_Formula_Impl::numVars ( ) const

inlinevirtual

Implements SAT::CNF_Formula.

Definition at line 160 of file cnf.h.

References d_numVars.

Referenced by SAT::DPLLTBasic::addNewClauses(), SAT::DPLLTBasic::generate_CDB(), and setNumVars().

unsigned SAT::CNF_Formula_Impl::numClauses ( ) const

inlinevirtual

Implements SAT::CNF_Formula.

Definition at line 161 of file cnf.h.

References d_formula.

void SAT::CNF_Formula_Impl::deleteLast ( )

inline

Definition at line 162 of file cnf.h.

References d_formula, and DebugAssert.

Referenced by CVC3::SearchSat::newUserAssumptionIntHelper().

void CNF_Formula_Impl::newClause ( )

virtual

Implements SAT::CNF_Formula.

Definition at line 137 of file cnf.cpp.

Referenced by SAT::DPLLTBasic::checkSat().

void CNF_Formula_Impl::registerUnit ( )

virtual

Implements SAT::CNF_Formula.

Definition at line 144 of file cnf.cpp.

References DebugAssert, and SAT::Lit::getID().

void CNF_Formula_Impl::simplify ( )

Definition at line 153 of file cnf.cpp.

References Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::end(), and Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::find().

Referenced by SAT::DPLLTBasic::addNewClauses(), and SAT::DPLLTBasic::generate_CDB().

void CNF_Formula_Impl::reset ( )

Definition at line 174 of file cnf.cpp.

Referenced by MiniSat::Solver::push(), SATDeductionHook(), and MiniSat::Solver::search().

Member Data Documentation

std::hash_map<int, bool> SAT::CNF_Formula_Impl::d_lits

private

Definition at line 146 of file cnf.h.

std::deque<Clause> SAT::CNF_Formula_Impl::d_formula

private

Definition at line 147 of file cnf.h.

Referenced by begin(), deleteLast(), empty(), end(), numClauses(), and operator[]().

unsigned SAT::CNF_Formula_Impl::d_numVars

private

Definition at line 148 of file cnf.h.

Referenced by numVars(), and setNumVars().

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