Public Types | Public Member Functions | Private Attributes

SAT::Clause Class Reference

#include <cnf.h>

List of all members.

Public Types

Public Member Functions

Private Attributes


Detailed Description

Definition at line 75 of file cnf.h.


Member Typedef Documentation

Definition at line 87 of file cnf.h.


Constructor & Destructor Documentation

SAT::Clause::Clause (  )  [inline]

Definition at line 83 of file cnf.h.

SAT::Clause::Clause ( const Clause clause  )  [inline]

Definition at line 85 of file cnf.h.


Member Function Documentation

const_iterator SAT::Clause::begin (  )  const [inline]
const_iterator SAT::Clause::end (  )  const [inline]
void SAT::Clause::clear (  )  [inline]

Definition at line 93 of file cnf.h.

References d_lits.

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

unsigned SAT::Clause::size (  )  const [inline]
void SAT::Clause::addLiteral ( Lit  l  )  [inline]

Definition at line 95 of file cnf.h.

References d_lits, d_satisfied, and d_unit.

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

unsigned SAT::Clause::getMaxVar (  )  const

Definition at line 30 of file cnf.cpp.

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

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

bool SAT::Clause::isSatisfied (  )  const [inline]

Definition at line 97 of file cnf.h.

References d_lits.

Referenced by print().

bool SAT::Clause::isUnit (  )  const [inline]

Definition at line 98 of file cnf.h.

References d_lits, and d_satisfied.

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

bool SAT::Clause::isNull (  )  const [inline]

Definition at line 99 of file cnf.h.

void SAT::Clause::setSatisfied (  )  [inline]

Definition at line 100 of file cnf.h.

References d_satisfied.

void SAT::Clause::setUnit (  )  [inline]

Definition at line 101 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(), and isSatisfied().

void SAT::Clause::setClauseTheorem ( CVC3::Theorem  thm  )  [inline]
CVC3::Theorem SAT::Clause::getClauseTheorem (  )  const [inline]

Member Data Documentation

int SAT::Clause::d_satisfied [private]

Definition at line 76 of file cnf.h.

Referenced by addLiteral(), isUnit(), setClauseTheorem(), and setSatisfied().

int SAT::Clause::d_unit [private]

Definition at line 77 of file cnf.h.

Referenced by addLiteral(), and setUnit().

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

Definition at line 78 of file cnf.h.

Referenced by addLiteral(), clear(), isSatisfied(), isUnit(), and size().

Definition at line 79 of file cnf.h.


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