SAT::Lit Class Reference

#include <cnf.h>

List of all members.

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)

---

Detailed Description

Definition at line 38 of file cnf.h.

---

Constructor & Destructor Documentation

SAT::Lit::Lit (   )  [inline]

Definition at line 42 of file cnf.h.

SAT::Lit::Lit (  Var  v, bool  positive = true )  [inline]

Definition at line 43 of file cnf.h. References d_index, and SAT::Var::isNull().

---

Member Function Documentation

static Lit SAT::Lit::mkLit (  int  index  )  [inline, static, private]

Definition at line 40 of file cnf.h. References d_index. Referenced by getFalse(), and getTrue().

static Lit SAT::Lit::getTrue (   )  [inline, static]

Definition at line 47 of file cnf.h. References mkLit(). Referenced by SAT::CNF_Manager::getCNFLit(), and SAT::CNF_Manager::translateExprRec().

static Lit SAT::Lit::getFalse (   )  [inline, static]

Definition at line 48 of file cnf.h. References mkLit(). Referenced by SAT::CNF_Manager::getCNFLit(), and SAT::CNF_Manager::translateExprRec().

bool SAT::Lit::isNull (   )  const [inline]

Definition at line 50 of file cnf.h. References d_index. Referenced by SAT::CNF_Manager::concreteLit(), SAT::CNF_Manager::convertLemma(), SAT::DPLLTBasic::cvcl2SAT(), CVCL::SearchSat::getImplication(), SATDecisionHook(), SATDeductionHook(), and SAT::CNF_Manager::translateExprRec().

bool SAT::Lit::isPositive (   )  const [inline]

Definition at line 51 of file cnf.h. References d_index. Referenced by CVCL::SearchSat::assertLit(), SAT::CNF_Manager::concreteLit(), and SAT::DPLLTBasic::cvcl2SAT().

bool SAT::Lit::isInverted (   )  const [inline]

Definition at line 52 of file cnf.h. References d_index. Referenced by CVCL::SearchSat::findSplitterRec(), and CVCL::SearchSat::getValue().

bool SAT::Lit::isFalse (   )  const [inline]

Definition at line 53 of file cnf.h. References d_index. Referenced by CVCL::SearchSat::findSplitterRec(), and CVCL::SearchSat::getValue().

bool SAT::Lit::isTrue (   )  const [inline]

Definition at line 54 of file cnf.h. References d_index. Referenced by CVCL::SearchSat::findSplitterRec(), and CVCL::SearchSat::getValue().

bool SAT::Lit::isVar (   )  const [inline]

Definition at line 55 of file cnf.h. References CVCL::abs(), and d_index. Referenced by SAT::CNF_Formula::addLiteral(), CVCL::SearchSat::findSplitterRec(), CVCL::SearchSat::getValue(), getVar(), SAT::CNF_Manager::numFanins(), SAT::CNF_Manager::numFanouts(), and SAT::CNF_Manager::translateExprRec().

int SAT::Lit::getID (   )  const [inline]

Definition at line 56 of file cnf.h. References d_index. Referenced by SAT::CNF_Formula_Impl::registerUnit().

Var SAT::Lit::getVar (   )  const [inline]

Definition at line 57 of file cnf.h. References CVCL::abs(), d_index, and isVar(). Referenced by SAT::CNF_Formula::addLiteral(), CVCL::SearchSat::assertLit(), SAT::CNF_Manager::concreteLit(), SAT::DPLLTBasic::cvcl2SAT(), CVCL::SearchSat::findSplitterRec(), SAT::CNF_Manager::getFanin(), SAT::CNF_Manager::getFanout(), CVCL::SearchSat::getValue(), SAT::CNF_Manager::numFanins(), SAT::CNF_Manager::numFanouts(), SAT::CNF_Manager::translateExpr(), and SAT::CNF_Manager::translateExprRec().

void SAT::Lit::reset (   )  [inline]

Definition at line 61 of file cnf.h. References d_index. Referenced by CVCL::SearchSat::getImplication().

---

Friends And Related Function Documentation

Lit operator! (  const Lit &  lit  )  [friend]

Definition at line 62 of file cnf.h.

---

Member Data Documentation

int SAT::Lit::d_index [private]

Definition at line 39 of file cnf.h. Referenced by getID(), getVar(), isFalse(), isInverted(), isNull(), isPositive(), isTrue(), isVar(), Lit(), mkLit(), and reset().

---

The documentation for this class was generated from the following file:

• cnf.h

---