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