CVC3
2.4.1
|
#include <minisat_types.h>
MiniSat::Lit::Lit | ( | int | index | ) | [inline, explicit, private] |
Definition at line 62 of file minisat_types.h.
MiniSat::Lit::Lit | ( | ) | [inline] |
Definition at line 64 of file minisat_types.h.
Referenced by operator~(), toLit(), unsign(), and id().
MiniSat::Lit::Lit | ( | Var | var, |
bool | sgn | ||
) | [inline, explicit] |
Definition at line 65 of file minisat_types.h.
Lit MiniSat::Lit::operator~ | ( | void | ) | const [inline] |
Definition at line 66 of file minisat_types.h.
bool MiniSat::Lit::sign | ( | ) | const [inline] |
Definition at line 68 of file minisat_types.h.
References x.
Referenced by MiniSat::Solver::enqueue(), MiniSat::Solver::checkTrail(), MiniSat::miniSatToCVC(), MiniSat::Solver::getValue(), toString(), and toDimacs().
int MiniSat::Lit::var | ( | ) | const [inline] |
Definition at line 69 of file minisat_types.h.
References x.
Referenced by MiniSat::Solver::printDIMACS(), MiniSat::Solver::getReason(), MiniSat::Solver::resolveTheoryImplication(), MiniSat::Solver::analyze(), lastToFirst_lt::operator()(), MiniSat::Solver::analyze_minimize(), MiniSat::Solver::analyze_removable(), MiniSat::Solver::enqueue(), MiniSat::Solver::protocolPropagation(), MiniSat::Solver::checkTrail(), MiniSat::miniSatToCVC(), MiniSat::Solver::getPushID(), MiniSat::Solver::varBumpActivity(), MiniSat::Solver::getValue(), MiniSat::Solver::getLevel(), MiniSat::Solver::setLevel(), toString(), and toDimacs().
int MiniSat::Lit::index | ( | ) | const [inline] |
Definition at line 70 of file minisat_types.h.
References x.
Referenced by MiniSat::Derivation::computeRootReason(), MiniSat::Solver::protocolPropagation(), MiniSat::Solver::search(), MiniSat::Solver::push(), MiniSat::Solver::getWatches(), operator==(), and operator<().
static Lit MiniSat::Lit::toLit | ( | int | i | ) | [inline, static] |
Definition at line 71 of file minisat_types.h.
References Lit().
Lit MiniSat::Lit::unsign | ( | ) | const [inline] |
Definition at line 72 of file minisat_types.h.
Definition at line 73 of file minisat_types.h.
bool MiniSat::Lit::operator== | ( | const Lit | q | ) | const [inline] |
bool MiniSat::Lit::operator!= | ( | const Lit | q | ) | const [inline] |
Definition at line 76 of file minisat_types.h.
References operator==().
bool MiniSat::Lit::operator< | ( | const Lit | q | ) | const [inline] |
Definition at line 78 of file minisat_types.h.
References index().
unsigned int MiniSat::Lit::hash | ( | ) | const [inline] |
Definition at line 80 of file minisat_types.h.
References x.
std::string MiniSat::Lit::toString | ( | ) | const [inline] |
Definition at line 82 of file minisat_types.h.
Referenced by MiniSat::Solver::toString(), and MiniSat::Clause::toString().
int MiniSat::Lit::toDimacs | ( | ) | const [inline] |
Definition at line 92 of file minisat_types.h.
int MiniSat::Lit::x [private] |
Definition at line 60 of file minisat_types.h.
Referenced by operator~(), sign(), var(), index(), unsign(), id(), and hash().