#include <cnf.h>
Definition at line 75 of file cnf.h.
typedef std::vector<Lit>::const_iterator SAT::Clause::const_iterator |
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().
bool SAT::Clause::isSatisfied | ( | ) | const [inline] |
bool SAT::Clause::isUnit | ( | ) | const [inline] |
Definition at line 97 of file cnf.h.
References d_unit.
Referenced by SAT::CNF_Formula::operator+=().
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] |
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().
int SAT::Clause::d_id [private] |
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] |
std::vector<Lit> SAT::Clause::d_lits [private] |