CVC3
2.4.1
|
#include <cnf.h>
Public Types | |
typedef std::vector< Lit > ::const_iterator | const_iterator |
Public Member Functions | |
Clause () | |
Clause (const Clause &clause) | |
const_iterator | begin () const |
const_iterator | end () const |
void | clear () |
unsigned | size () const |
void | addLiteral (Lit l) |
unsigned | getMaxVar () const |
bool | isSatisfied () const |
bool | isUnit () const |
bool | isNull () const |
void | setSatisfied () |
void | setUnit () |
void | print () const |
void | setClauseTheorem (CVC3::Theorem thm) |
CVC3::Theorem | getClauseTheorem () const |
Private Attributes | |
int | d_satisfied:1 |
int | d_unit:1 |
std::vector< Lit > | d_lits |
CVC3::Theorem | d_reason |
typedef std::vector<Lit>::const_iterator SAT::Clause::const_iterator |
|
inline |
Definition at line 93 of file cnf.h.
References d_lits.
Referenced by SAT::DPLLTBasic::addNewClause(), MiniSat::cvcToMiniSat(), and SAT::CNF_Formula::operator+=().
|
inline |
Definition at line 94 of file cnf.h.
References d_lits.
Referenced by SAT::DPLLTBasic::addNewClause(), MiniSat::cvcToMiniSat(), and SAT::CNF_Formula::operator+=().
|
inline |
Definition at line 96 of file cnf.h.
References d_lits, d_satisfied, and d_unit.
|
inline |
Definition at line 97 of file cnf.h.
References d_lits.
Referenced by SAT::DPLLTBasic::addNewClause().
|
inline |
Definition at line 98 of file cnf.h.
References d_lits, and d_satisfied.
Referenced by SAT::CNF_Formula::addLiteral().
unsigned SAT::Clause::getMaxVar | ( | ) | const |
Definition at line 30 of file cnf.cpp.
References DebugAssert, and CVC3::max().
Referenced by SAT::DPLLTBasic::addNewClause().
|
inline |
Definition at line 100 of file cnf.h.
References d_satisfied.
|
inline |
Definition at line 101 of file cnf.h.
References d_unit.
Referenced by SAT::CNF_Formula::operator+=().
|
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().
Referenced by SAT::CNF_Formula::print().
|
inline |
Definition at line 106 of file cnf.h.
References d_reason.
Referenced by SAT::CNF_Manager::addAssumption(), SAT::CNF_Manager::addLemma(), SAT::CNF_Manager::convertLemma(), SAT::CNF_Manager::translateExpr(), and SAT::CNF_Manager::translateExprRec().
|
inline |
Definition at line 108 of file cnf.h.
References d_reason.
Referenced by MiniSat::Solver::addClause(), MiniSat::Solver::cvcToMiniSat(), and SAT::CNF_Formula::operator+=().
|
private |
Definition at line 79 of file cnf.h.
Referenced by addLiteral(), clear(), isSatisfied(), and setSatisfied().
|
private |
|
private |
|
private |
Definition at line 82 of file cnf.h.
Referenced by getClauseTheorem(), and setClauseTheorem().