CVC3  2.4.1
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


Member Typedef Documentation

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::CNF_Formula::operator+=(), SAT::DPLLTBasic::addNewClause(), and MiniSat::cvcToMiniSat().

const_iterator SAT::Clause::end ( ) const [inline]

Definition at line 94 of file cnf.h.

References d_lits.

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

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

Definition at line 96 of file cnf.h.

References d_satisfied, d_unit, and d_lits.

unsigned SAT::Clause::size ( ) const [inline]

Definition at line 97 of file cnf.h.

References d_lits.

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

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

Definition at line 98 of file cnf.h.

References d_satisfied, and d_lits.

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

unsigned SAT::Clause::getMaxVar ( ) const

Definition at line 30 of file cnf.cpp.

References CVC3::max(), and DebugAssert.

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

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

Definition at line 100 of file cnf.h.

References d_satisfied.

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.

void SAT::Clause::print ( ) const

Definition at line 42 of file cnf.cpp.

References std::endl().

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

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

int SAT::Clause::d_unit [private]

Definition at line 80 of file cnf.h.

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

Definition at line 81 of file cnf.h.

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

Definition at line 82 of file cnf.h.

Referenced by setClauseTheorem(), and getClauseTheorem().


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