#include <cnf.h>
Definition at line 48 of file cnf.h.
SAT::Lit::Lit | ( | Var | v, | |
bool | positive = true | |||
) | [inline, explicit] |
static Lit SAT::Lit::mkLit | ( | int | index | ) | [inline, static, private] |
Definition at line 50 of file cnf.h.
Referenced by isNull(), and isPositive().
static Lit SAT::Lit::getTrue | ( | ) | [inline, static] |
Definition at line 57 of file cnf.h.
Referenced by SAT::CNF_Manager::getCNFLit(), and SAT::CNF_Manager::translateExprRec().
static Lit SAT::Lit::getFalse | ( | ) | [inline, static] |
Definition at line 58 of file cnf.h.
Referenced by SAT::CNF_Manager::getCNFLit(), and SAT::CNF_Manager::translateExprRec().
bool SAT::Lit::isNull | ( | ) | const [inline] |
Definition at line 60 of file cnf.h.
References mkLit().
Referenced by SAT::CNF_Manager::concreteLit(), SAT::CNF_Manager::convertLemma(), CVC3::SearchSat::getImplication(), CVC3::SearchSat::getValue(), MiniSat::Solver::push(), SATDecisionHook(), SATDeductionHook(), MiniSat::Solver::search(), and SAT::CNF_Manager::translateExprRec().
bool SAT::Lit::isPositive | ( | ) | const [inline] |
Definition at line 61 of file cnf.h.
References mkLit().
Referenced by CVC3::SearchSat::assertLit(), CVC3::SearchSat::check(), SAT::CNF_Manager::concreteLit(), MiniSat::cvcToMiniSat(), and CVC3::SearchSat::getValue().
bool SAT::Lit::isInverted | ( | ) | const [inline] |
Definition at line 62 of file cnf.h.
Referenced by CVC3::SearchSat::findSplitterRec(), and CVC3::SearchSat::getValue().
bool SAT::Lit::isFalse | ( | ) | const [inline] |
Definition at line 63 of file cnf.h.
References d_index.
Referenced by MiniSat::cvcToMiniSat(), and CVC3::SearchSat::findSplitterRec().
bool SAT::Lit::isTrue | ( | ) | const [inline] |
Definition at line 64 of file cnf.h.
References d_index.
Referenced by MiniSat::cvcToMiniSat(), CVC3::SearchSat::findSplitterRec(), and CVC3::SearchSat::getValue().
bool SAT::Lit::isVar | ( | ) | const [inline] |
Definition at line 65 of file cnf.h.
References d_index.
Referenced by CVC3::SearchSat::findSplitterRec(), SAT::CNF_Formula::getCurrentClause(), CVC3::SearchSat::getValue(), and SAT::CNF_Manager::translateExprRec().
int SAT::Lit::getID | ( | ) | const [inline] |
Definition at line 66 of file cnf.h.
References d_index.
Referenced by CVC3::operator<(), and SAT::CNF_Formula_Impl::registerUnit().
Var SAT::Lit::getVar | ( | ) | const [inline] |
Definition at line 67 of file cnf.h.
References d_index.
Referenced by CVC3::SearchSat::assertLit(), CVC3::SearchSat::check(), SAT::CNF_Manager::concreteLit(), MiniSat::cvcToMiniSat(), CVC3::SearchSat::findSplitterRec(), SAT::CNF_Formula::getCurrentClause(), CVC3::SearchSat::getValue(), SAT::CNF_Manager::translateExpr(), and SAT::CNF_Manager::translateExprRec().
void SAT::Lit::reset | ( | ) | [inline] |
Definition at line 71 of file cnf.h.
Referenced by CVC3::SearchSat::getImplication().
int SAT::Lit::d_index [private] |