CVC3
2.4.1
|
#include <cnf.h>
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] |
void SAT::Clause::setSatisfied | ( | ) | [inline] |
Definition at line 103 of file cnf.h.
References d_satisfied.
void SAT::Clause::print | ( | ) | const |
Definition at line 42 of file cnf.cpp.
References std::endl().
void SAT::Clause::setClauseTheorem | ( | CVC3::Theorem | thm | ) | [inline] |
Definition at line 106 of file cnf.h.
References d_reason.
Referenced by SAT::CNF_Manager::translateExprRec(), SAT::CNF_Manager::translateExpr(), SAT::CNF_Manager::convertLemma(), SAT::CNF_Manager::addAssumption(), and SAT::CNF_Manager::addLemma().
CVC3::Theorem SAT::Clause::getClauseTheorem | ( | ) | const [inline] |
Definition at line 108 of file cnf.h.
References d_reason.
Referenced by SAT::CNF_Formula::operator+=(), MiniSat::Solver::cvcToMiniSat(), and MiniSat::Solver::addClause().
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] |
std::vector<Lit> SAT::Clause::d_lits [private] |
CVC3::Theorem SAT::Clause::d_reason [private] |
Definition at line 82 of file cnf.h.
Referenced by setClauseTheorem(), and getClauseTheorem().