SAT::Clause Class Reference

#include <cnf.h>

Collaboration diagram for SAT::Clause:

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

---

Member Typedef Documentation

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

Definition at line 91 of file cnf.h.

---

Constructor & Destructor Documentation

SAT::Clause::Clause

(

)

[inline]

Definition at line 87 of file cnf.h.

SAT::Clause::Clause

(

const Clause &

clause

)

[inline]

Definition at line 89 of file cnf.h.

---

Member Function Documentation

const_iterator SAT::Clause::begin

(

)

const [inline]

Definition at line 94 of file cnf.h.

References d_lits.

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

const_iterator SAT::Clause::end

(

)

const [inline]

Definition at line 95 of file cnf.h.

References d_lits, d_satisfied, and d_unit.

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

void SAT::Clause::clear

(

)

[inline]

Definition at line 97 of file cnf.h.

References d_lits.

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

unsigned SAT::Clause::size

(

)

const [inline]

Definition at line 98 of file cnf.h.

References d_lits, and d_satisfied.

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

void SAT::Clause::addLiteral

(

Lit

l

)

[inline]

Definition at line 99 of file cnf.h.

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

unsigned SAT::Clause::getMaxVar

(

)

const

Definition at line 30 of file cnf.cpp.

References DebugAssert, and CVC3::max().

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

bool SAT::Clause::isSatisfied

(

)

const [inline]

Definition at line 101 of file cnf.h.

References d_unit.

bool SAT::Clause::isUnit

(

)

const [inline]

Definition at line 102 of file cnf.h.

References d_lits.

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

bool SAT::Clause::isNull

(

)

const [inline]

Definition at line 103 of file cnf.h.

References d_satisfied.

void SAT::Clause::setSatisfied

(

)

[inline]

Definition at line 104 of file cnf.h.

References d_unit.

void SAT::Clause::setUnit

(

)

[inline]

Definition at line 105 of file cnf.h.

void SAT::Clause::print

(

)

const

Definition at line 42 of file cnf.cpp.

References std::endl().

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

void SAT::Clause::setClauseTheorem

(

CVC3::Theorem

thm

)

[inline]

Definition at line 107 of file cnf.h.

References d_reason.

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

CVC3::Theorem SAT::Clause::getClauseTheorem

(

)

const [inline]

Definition at line 109 of file cnf.h.

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

Referenced by end(), isNull(), and size().

int SAT::Clause::d_unit [private]

Definition at line 81 of file cnf.h.

Referenced by end(), isSatisfied(), and setSatisfied().

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

Definition at line 82 of file cnf.h.

Referenced by begin(), clear(), end(), isUnit(), and size().

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

Definition at line 83 of file cnf.h.

Referenced by setClauseTheorem().

---

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

• cnf.h
• cnf.cpp