#include <minisat_types.h>
Static Public Member Functions |
static Lit | toLit (int i) |
static Lit | id (Lit p, bool sgn) |
Private Member Functions |
| Lit (int index) |
Detailed Description
Definition at line 59 of file minisat_types.h.
Constructor & Destructor Documentation
MiniSat::Lit::Lit |
( |
int |
index | ) |
|
|
inlineexplicitprivate |
MiniSat::Lit::Lit |
( |
Var |
var, |
|
|
bool |
sgn |
|
) |
| |
|
inlineexplicit |
Member Function Documentation
Lit MiniSat::Lit::operator~ |
( |
void |
| ) |
const |
|
inline |
bool MiniSat::Lit::sign |
( |
| ) |
const |
|
inline |
int MiniSat::Lit::var |
( |
| ) |
const |
|
inline |
Definition at line 69 of file minisat_types.h.
References x.
Referenced by MiniSat::Solver::analyze(), MiniSat::Solver::analyze_minimize(), MiniSat::Solver::analyze_removable(), MiniSat::Solver::checkTrail(), MiniSat::Solver::enqueue(), MiniSat::Solver::getLevel(), MiniSat::Solver::getPushID(), MiniSat::Solver::getReason(), MiniSat::Solver::getValue(), MiniSat::miniSatToCVC(), lastToFirst_lt::operator()(), MiniSat::Solver::printDIMACS(), MiniSat::Solver::protocolPropagation(), MiniSat::Solver::resolveTheoryImplication(), MiniSat::Solver::setLevel(), toDimacs(), toString(), and MiniSat::Solver::varBumpActivity().
int MiniSat::Lit::index |
( |
| ) |
const |
|
inline |
static Lit MiniSat::Lit::toLit |
( |
int |
i | ) |
|
|
inlinestatic |
Lit MiniSat::Lit::unsign |
( |
| ) |
const |
|
inline |
static Lit MiniSat::Lit::id |
( |
Lit |
p, |
|
|
bool |
sgn |
|
) |
| |
|
inlinestatic |
bool MiniSat::Lit::operator== |
( |
const Lit |
q | ) |
const |
|
inline |
bool MiniSat::Lit::operator!= |
( |
const Lit |
q | ) |
const |
|
inline |
bool MiniSat::Lit::operator< |
( |
const Lit |
q | ) |
const |
|
inline |
unsigned int MiniSat::Lit::hash |
( |
| ) |
const |
|
inline |
std::string MiniSat::Lit::toString |
( |
| ) |
const |
|
inline |
int MiniSat::Lit::toDimacs |
( |
| ) |
const |
|
inline |
Member Data Documentation
The documentation for this class was generated from the following file: