CVC3
2.4.1
|
#include <minisat_types.h>
Public Member Functions | |
Clause (bool learnt, const std::vector< Lit > &ps, CVC3::Theorem theorem, int id, int pushID) | |
int | size () const |
bool | learnt () const |
Lit | operator[] (int i) const |
Lit & | operator[] (int i) |
int | id () const |
int | pushID () const |
float | activity () const |
void | setActivity (float activity) |
void | toLit (std::vector< Lit > &literals) const |
CVC3::Theorem | getTheorem () const |
std::string | toString () const |
bool | contains (Lit l) |
Static Public Member Functions | |
static int | ClauseIDNull () |
static Clause * | Decision () |
static Clause * | TheoryImplication () |
Private Attributes | |
unsigned int | d_size_learnt |
int | d_id |
int | d_pushID |
float | d_activity |
CVC3::Theorem | d_theorem |
Lit | d_data [1] |
Static Private Attributes | |
static Clause * | s_decision = NULL |
static Clause * | s_theoryImplication = NULL |
Friends | |
Clause * | Clause_new (const std::vector< Lit > &ps, CVC3::Theorem theorem, int id) |
Clause * | Lemma_new (const std::vector< Lit > &ps, int id, int pushID) |
Definition at line 101 of file minisat_types.h.
|
inline |
Definition at line 119 of file minisat_types.h.
|
inline |
Definition at line 133 of file minisat_types.h.
Referenced by MiniSat::Solver::addClause(), MiniSat::Solver::allClausesSatisfied(), MiniSat::Solver::analyze(), MiniSat::Solver::analyze_minimize(), MiniSat::Solver::checkClause(), MiniSat::Solver::checkTrail(), MiniSat::Solver::checkWatched(), MiniSat::Derivation::computeRootReason(), contains(), MiniSat::Derivation::finish(), MiniSat::Solver::getConflictLevel(), MiniSat::Solver::getImplicationLevel(), MiniSat::Solver::insertClause(), MiniSat::Solver::insertLemma(), MiniSat::Solver::isPermSatisfied(), MiniSat::Solver::isReason(), reduceDB_lt::operator()(), MiniSat::Derivation::pop(), MiniSat::Solver::pop(), MiniSat::Solver::printDIMACS(), MiniSat::Solver::propagate(), MiniSat::Solver::push(), MiniSat::Derivation::registerClause(), MiniSat::Solver::remove(), MiniSat::Solver::resolveTheoryImplication(), MiniSat::Solver::setPushID(), MiniSat::Solver::simplifyDB(), toString(), and MiniSat::Solver::updateConflict().
|
inline |
Definition at line 134 of file minisat_types.h.
Referenced by activity(), MiniSat::Solver::addClause(), Clause(), MiniSat::Solver::insertClause(), MiniSat::Solver::remove(), and setActivity().
|
inline |
Definition at line 135 of file minisat_types.h.
|
inline |
Definition at line 136 of file minisat_types.h.
|
inline |
Definition at line 138 of file minisat_types.h.
References d_id.
Referenced by MiniSat::Inference::add(), MiniSat::Solver::addClause(), MiniSat::Solver::analyze(), MiniSat::Derivation::checkDerivation(), Clause(), MiniSat::Derivation::computeRootReason(), MiniSat::Derivation::createProof(), MiniSat::Derivation::finish(), MiniSat::Derivation::pop(), MiniSat::Derivation::printDerivation(), MiniSat::Solver::push(), and MiniSat::Derivation::registerClause().
|
inline |
Definition at line 143 of file minisat_types.h.
References d_pushID.
Referenced by MiniSat::Solver::analyze(), Clause(), MiniSat::Solver::isPermSatisfied(), MiniSat::Derivation::pop(), MiniSat::Solver::pop(), MiniSat::Solver::push(), MiniSat::Solver::setPushID(), and MiniSat::Solver::simplifyDB().
|
inline |
Definition at line 144 of file minisat_types.h.
References d_activity, DebugAssert, and learnt().
Referenced by MiniSat::Solver::claBumpActivity(), MiniSat::Solver::insertLemma(), reduceDB_lt::operator()(), and setActivity().
|
inline |
Definition at line 148 of file minisat_types.h.
References activity(), DebugAssert, and learnt().
Referenced by MiniSat::Solver::claBumpActivity(), and MiniSat::Solver::insertLemma().
void MiniSat::Clause::toLit | ( | std::vector< Lit > & | literals | ) | const |
Definition at line 72 of file minisat_types.cpp.
Referenced by MiniSat::Solver::insertLemma(), and MiniSat::Solver::toString().
|
inline |
Definition at line 153 of file minisat_types.h.
References d_theorem.
Referenced by MiniSat::Solver::addClause(), and MiniSat::Derivation::createProof().
|
inlinestatic |
Definition at line 155 of file minisat_types.h.
|
static |
Definition at line 54 of file minisat_types.cpp.
References MiniSat::Clause_new().
Referenced by MiniSat::Solver::analyze(), MiniSat::Solver::analyze_minimize(), MiniSat::Solver::analyze_removable(), MiniSat::Solver::assume(), MiniSat::Solver::checkTrail(), MiniSat::Derivation::computeRootReason(), MiniSat::Solver::printDIMACS(), MiniSat::Solver::printState(), MiniSat::Solver::protocolPropagation(), and MiniSat::Solver::setPushID().
|
static |
Definition at line 63 of file minisat_types.cpp.
References MiniSat::Clause_new().
Referenced by MiniSat::Solver::analyze(), MiniSat::Solver::analyze_removable(), MiniSat::Solver::checkTrail(), MiniSat::Solver::getReason(), MiniSat::Solver::push(), MiniSat::Solver::resolveTheoryImplication(), MiniSat::Solver::search(), and MiniSat::Solver::setPushID().
|
inline |
Definition at line 163 of file minisat_types.h.
References size(), and MiniSat::Lit::toString().
Referenced by MiniSat::Derivation::printDerivation().
|
inline |
Definition at line 174 of file minisat_types.h.
References size().
|
friend |
Definition at line 44 of file minisat_types.cpp.
Definition at line 49 of file minisat_types.cpp.
|
private |
Definition at line 102 of file minisat_types.h.
|
private |
Definition at line 103 of file minisat_types.h.
Referenced by id().
|
private |
Definition at line 104 of file minisat_types.h.
Referenced by pushID().
|
private |
Definition at line 105 of file minisat_types.h.
Referenced by activity().
|
private |
Definition at line 107 of file minisat_types.h.
Referenced by getTheorem().
|
private |
Definition at line 108 of file minisat_types.h.
|
staticprivate |
Definition at line 110 of file minisat_types.h.
|
staticprivate |
Definition at line 111 of file minisat_types.h.