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

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:
Generated on Tue Jul 3 14:42:21 2007 for CVC3 by  doxygen 1.5.1