SAT::CNF_Formula_Impl Class Reference

#include <cnf.h>

Inheritance diagram for SAT::CNF_Formula_Impl:

[legend]

Collaboration diagram for SAT::CNF_Formula_Impl:

[legend]

List of all members.

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

Private Member Functions

• void setNumVars (unsigned numVars)

Private Attributes

• std::hash_map< int, bool > d_lits
• std::deque< Clause > d_formula
• unsigned d_numVars

---

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

)

[inline, private, virtual]

Implements SAT::CNF_Formula.

Definition at line 150 of file cnf.h.

References d_numVars.

bool SAT::CNF_Formula_Impl::empty

(

)

const [inline, virtual]

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 [inline, virtual]

Implements SAT::CNF_Formula.

Definition at line 157 of file cnf.h.

References d_formula.

const_iterator SAT::CNF_Formula_Impl::begin

(

)

const [inline, virtual]

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 [inline, virtual]

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 [inline, virtual]

Implements SAT::CNF_Formula.

Definition at line 160 of file cnf.h.

References d_numVars.

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

unsigned SAT::CNF_Formula_Impl::numClauses

(

)

const [inline, virtual]

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.

References SAT::CNF_Formula::d_current, and d_formula.

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

void CNF_Formula_Impl::registerUnit

(

)

[virtual]

Implements SAT::CNF_Formula.

Definition at line 144 of file cnf.cpp.

References SAT::Clause::begin(), SAT::CNF_Formula::d_current, d_lits, DebugAssert, SAT::Lit::getID(), SAT::Clause::setUnit(), and SAT::Clause::size().

void CNF_Formula_Impl::simplify

(

)

Definition at line 153 of file cnf.cpp.

References d_formula, d_lits, 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.

References Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::clear(), SAT::CNF_Formula::d_current, d_formula, d_lits, and d_numVars.

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.

Referenced by registerUnit(), reset(), and simplify().

std::deque<Clause> SAT::CNF_Formula_Impl::d_formula [private]

Definition at line 147 of file cnf.h.

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

unsigned SAT::CNF_Formula_Impl::d_numVars [private]

Definition at line 148 of file cnf.h.

Referenced by numVars(), reset(), and setNumVars().

---

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

• cnf.h
• cnf.cpp