SAT::Clause Class Reference

#include <cnf.h>

Collaboration diagram for SAT::Clause:

[legend]

List of all members.

Public Types

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

Public Member Functions

• Clause ()
• Clause (const Clause &clause)
• const_iterator begin () const
• const_iterator end () const
• void clear ()
• unsigned size () const
• void addLiteral (Lit l)
• unsigned getMaxVar () const
• bool isSatisfied () const
• bool isUnit () const
• bool isNull () const
• void setSatisfied ()
• void setUnit ()
• void print () const
• void setClauseTheorem (CVC3::Theorem thm)
• CVC3::Theorem getClauseTheorem () const

Private Attributes

• int d_satisfied:1
• int d_unit:1
• std::vector< Lit > d_lits
• CVC3::Theorem d_reason

---

Detailed Description

Definition at line 78 of file cnf.h.

---

Member Typedef Documentation

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

Definition at line 90 of file cnf.h.

---

Constructor & Destructor Documentation

SAT::Clause::Clause

(

)

[inline]

Definition at line 86 of file cnf.h.

SAT::Clause::Clause

(

const Clause &

clause

)

[inline]

Definition at line 88 of file cnf.h.

---

Member Function Documentation

const_iterator SAT::Clause::begin

(

)

const [inline]

Definition at line 93 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 94 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 96 of file cnf.h.

References d_lits, d_satisfied, and d_unit.

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

unsigned SAT::Clause::size

(

)

const [inline]

Definition at line 97 of file cnf.h.

References d_lits.

Referenced by SAT::DPLLTBasic::addNewClause(), SAT::CD_CNF_Formula::registerUnit(), and SAT::CNF_Formula_Impl::registerUnit().

void SAT::Clause::addLiteral

(

Lit

l

)

[inline]

Definition at line 98 of file cnf.h.

References d_lits, and d_satisfied.

Referenced by SAT::CNF_Formula::addLiteral().

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

bool SAT::Clause::isSatisfied

(

)

const [inline]

Definition at line 100 of file cnf.h.

References d_satisfied.

Referenced by print().

bool SAT::Clause::isUnit

(

)

const [inline]

Definition at line 101 of file cnf.h.

References d_unit.

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

bool SAT::Clause::isNull

(

)

const [inline]

Definition at line 102 of file cnf.h.

References d_lits.

void SAT::Clause::setSatisfied

(

)

[inline]

Definition at line 103 of file cnf.h.

References d_satisfied.

void SAT::Clause::setUnit

(

)

[inline]

Definition at line 104 of file cnf.h.

References d_unit.

Referenced by 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().

void SAT::Clause::setClauseTheorem

(

CVC3::Theorem

thm

)

[inline]

Definition at line 106 of file cnf.h.

References d_reason.

Referenced by SAT::CNF_Manager::addAssumption(), SAT::CNF_Manager::addLemma(), SAT::CNF_Manager::convertLemma(), SAT::CNF_Formula::copy(), SAT::CNF_Formula::operator+=(), SAT::CNF_Manager::translateExpr(), and SAT::CNF_Manager::translateExprRec().

CVC3::Theorem SAT::Clause::getClauseTheorem

(

)

const [inline]

Definition at line 108 of file cnf.h.

References d_reason.

Referenced by MiniSat::Solver::addClause(), MiniSat::Solver::cvcToMiniSat(), and SAT::CNF_Formula::operator+=().

---

Member Data Documentation

int SAT::Clause::d_satisfied [private]

Definition at line 79 of file cnf.h.

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

int SAT::Clause::d_unit [private]

Definition at line 80 of file cnf.h.

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

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

Definition at line 81 of file cnf.h.

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

CVC3::Theorem SAT::Clause::d_reason [private]

Definition at line 82 of file cnf.h.

Referenced by getClauseTheorem(), and setClauseTheorem().

---

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

• cnf.h
• cnf.cpp