SAT::Clause Class Reference

#include <cnf.h>

List of all members.

Public Types

• typedef std::vector< Lit
  >::const_iterator const_iterator

Public Member Functions

• Clause ()
• const_iterator begin () const
• const_iterator end () const
• void clear ()
• unsigned size () const
• void addLiteral (Lit l)
• unsigned getMaxVar () const
• int getId () const
• bool isSatisfied () const
• bool isUnit () const
• bool isNull () const
• void setId (int id)
• void setSatisfied ()
• void setUnit ()
• void print () const

Private Attributes

• int d_id:30
• int d_satisfied:1
• int d_unit:1
• std::vector< Lit > d_lits

---

Detailed Description

Definition at line 75 of file cnf.h.

---

Member Typedef Documentation

typedef std::vector<Lit>::const_iterator SAT::Clause::const_iterator

Definition at line 86 of file cnf.h.

---

Constructor & Destructor Documentation

SAT::Clause::Clause

(

)

[inline]

Definition at line 84 of file cnf.h.

---

Member Function Documentation

const_iterator SAT::Clause::begin

(

)

const [inline]

Definition at line 87 of file cnf.h.

References d_lits.

Referenced by SAT::DPLLTBasic::addNewClause(), MiniSat::cvcToMiniSat(), getMaxVar(), SAT::CNF_Formula::operator+=(), print(), and SAT::CNF_Formula_Impl::registerUnit().

const_iterator SAT::Clause::end

(

)

const [inline]

Definition at line 88 of file cnf.h.

References d_lits.

Referenced by SAT::DPLLTBasic::addNewClause(), MiniSat::cvcToMiniSat(), getMaxVar(), SAT::CNF_Formula::operator+=(), and print().

void SAT::Clause::clear

(

)

[inline]

Definition at line 90 of file cnf.h.

References d_id, d_lits, d_satisfied, and d_unit.

Referenced by SAT::DPLLTBasic::addNewClauses(), SAT::DPLLTBasic::generate_CDB(), MiniSat::Solver::push(), and MiniSat::Solver::search().

unsigned SAT::Clause::size

(

)

const [inline]

Definition at line 91 of file cnf.h.

References d_lits.

Referenced by SAT::DPLLTBasic::addNewClause(), SAT::CNF_Manager::convertLemma(), CVC3::SearchSat::getExplanation(), SAT::CD_CNF_Formula::registerUnit(), and SAT::CNF_Formula_Impl::registerUnit().

void SAT::Clause::addLiteral

(

Lit

l

)

[inline]

Definition at line 92 of file cnf.h.

References d_lits, and d_satisfied.

Referenced by SAT::CNF_Formula::addLiteral(), and SAT::CNF_Manager::convertLemma().

unsigned SAT::Clause::getMaxVar

(

)

const

Definition at line 30 of file cnf.cpp.

References begin(), DebugAssert, end(), and MiniSat::max().

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

int SAT::Clause::getId

(

)

const [inline]

Definition at line 95 of file cnf.h.

References d_id.

bool SAT::Clause::isSatisfied

(

)

const [inline]

Definition at line 96 of file cnf.h.

References d_satisfied.

Referenced by print().

bool SAT::Clause::isUnit

(

)

const [inline]

Definition at line 97 of file cnf.h.

References d_unit.

Referenced by SAT::CNF_Formula::operator+=().

bool SAT::Clause::isNull

(

)

const [inline]

Definition at line 98 of file cnf.h.

References d_lits.

void SAT::Clause::setId

(

int

id

)

[inline]

Definition at line 99 of file cnf.h.

References d_id, and FatalAssert.

Referenced by SAT::CNF_Manager::addAssumption(), SAT::CNF_Manager::addLemma(), SAT::CNF_Manager::convertLemma(), and SAT::CNF_Manager::translateExpr().

void SAT::Clause::setSatisfied

(

)

[inline]

Definition at line 101 of file cnf.h.

References d_satisfied.

void SAT::Clause::setUnit

(

)

[inline]

Definition at line 102 of file cnf.h.

References d_unit.

Referenced by SAT::CNF_Manager::convertLemma(), SAT::CD_CNF_Formula::registerUnit(), and SAT::CNF_Formula_Impl::registerUnit().

void SAT::Clause::print

(

)

const

Definition at line 42 of file cnf.cpp.

References begin(), end(), std::endl(), and isSatisfied().

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

---

Member Data Documentation

int SAT::Clause::d_id [private]

If d_id is 0 then the clause is a translation clause and its theorem can be figured out lazily. Otherwise, d_id gives the index into d_theorems for the theorem justifying this clause.

Definition at line 79 of file cnf.h.

Referenced by clear(), getId(), and setId().

int SAT::Clause::d_satisfied [private]

Definition at line 80 of file cnf.h.

Referenced by addLiteral(), clear(), isSatisfied(), and setSatisfied().

int SAT::Clause::d_unit [private]

Definition at line 81 of file cnf.h.

Referenced by clear(), isUnit(), and setUnit().

std::vector<Lit> SAT::Clause::d_lits [private]

Definition at line 82 of file cnf.h.

Referenced by addLiteral(), begin(), clear(), end(), isNull(), and size().

---

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

• cnf.h
• cnf.cpp

---