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

#include <cnf.h>

Inheritance diagram for SAT::CNF_Formula_Impl:
SAT::CNF_Formula

Public Member Functions

 CNF_Formula_Impl ()
 CNF_Formula_Impl (const CNF_Formula &cnf)
 ~CNF_Formula_Impl ()
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 ()
void simplify ()
void reset ()
- 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

std::hash_map< int, bool > d_lits
std::deque< Claused_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
virtual void setNumVars (unsigned numVars)=0
void copy (const CNF_Formula &cnf)
- Protected Attributes inherited from SAT::CNF_Formula
Claused_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)
inlineprivate

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