CVC3
2.4.1
|
#include <cnf.h>
SAT::Lit::Lit | ( | Var | v, |
bool | positive = true |
||
) | [inline, explicit] |
Definition at line 56 of file cnf.h.
References SAT::Var::isNull(), and d_index.
static Lit SAT::Lit::mkLit | ( | int | index | ) | [inline, static, private] |
static Lit SAT::Lit::getTrue | ( | ) | [inline, static] |
Definition at line 60 of file cnf.h.
References mkLit().
Referenced by SAT::CNF_Manager::translateExprRec(), and SAT::CNF_Manager::getCNFLit().
static Lit SAT::Lit::getFalse | ( | ) | [inline, static] |
Definition at line 61 of file cnf.h.
References mkLit().
Referenced by SAT::CNF_Manager::translateExprRec(), and SAT::CNF_Manager::getCNFLit().
bool SAT::Lit::isNull | ( | ) | const [inline] |
Definition at line 63 of file cnf.h.
References d_index.
Referenced by SAT::CNF_Manager::translateExprRec(), SAT::CNF_Manager::convertLemma(), SAT::CNF_Manager::concreteLit(), SATDecisionHook(), SATDeductionHook(), SAT::DPLLTBasic::cvc2SAT(), MiniSat::Solver::search(), MiniSat::Solver::push(), CVC3::SearchSat::getImplication(), and CVC3::SearchSat::getValue().
bool SAT::Lit::isPositive | ( | ) | const [inline] |
Definition at line 64 of file cnf.h.
References d_index.
Referenced by SAT::CNF_Manager::concreteLit(), SAT::DPLLTBasic::cvc2SAT(), MiniSat::cvcToMiniSat(), CVC3::SearchSat::assertLit(), CVC3::SearchSat::check(), and CVC3::SearchSat::getValue().
bool SAT::Lit::isInverted | ( | ) | const [inline] |
Definition at line 65 of file cnf.h.
References d_index.
Referenced by CVC3::SearchSat::findSplitterRec(), and CVC3::SearchSat::getValue().
bool SAT::Lit::isFalse | ( | ) | const [inline] |
Definition at line 66 of file cnf.h.
References d_index.
Referenced by MiniSat::cvcToMiniSat(), and CVC3::SearchSat::findSplitterRec().
bool SAT::Lit::isTrue | ( | ) | const [inline] |
Definition at line 67 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 68 of file cnf.h.
References CVC3::abs(), and d_index.
Referenced by getVar(), SAT::CNF_Formula::addLiteral(), SAT::CNF_Manager::translateExprRec(), CVC3::SearchSat::findSplitterRec(), and CVC3::SearchSat::getValue().
int SAT::Lit::getID | ( | ) | const [inline] |
Definition at line 69 of file cnf.h.
References d_index.
Referenced by SAT::CNF_Formula_Impl::registerUnit(), and CVC3::operator<().
Var SAT::Lit::getVar | ( | ) | const [inline] |
Definition at line 70 of file cnf.h.
References DebugAssert, isVar(), CVC3::abs(), and d_index.
Referenced by SAT::CNF_Formula::addLiteral(), SAT::CNF_Manager::translateExprRec(), SAT::CNF_Manager::translateExpr(), SAT::CNF_Manager::concreteLit(), SAT::DPLLTBasic::cvc2SAT(), MiniSat::cvcToMiniSat(), CVC3::SearchSat::assertLit(), CVC3::SearchSat::findSplitterRec(), CVC3::SearchSat::check(), and CVC3::SearchSat::getValue().
void SAT::Lit::reset | ( | ) | [inline] |
Definition at line 74 of file cnf.h.
References d_index.
Referenced by CVC3::SearchSat::getImplication().
int SAT::Lit::d_index [private] |