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 51 of file cnf.h.

---

Constructor & Destructor Documentation

SAT::Lit::Lit

(

)

[inline]

Definition at line 55 of file cnf.h.

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

Definition at line 56 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 53 of file cnf.h.

References d_index.

Referenced by getFalse(), and getTrue().

static Lit SAT::Lit::getTrue

(

)

[inline, static]

Definition at line 60 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 61 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 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().

bool SAT::Lit::isPositive

(

)

const [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().

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 SAT::CNF_Formula::addLiteral(), CVC3::SearchSat::findSplitterRec(), CVC3::SearchSat::getValue(), getVar(), and SAT::CNF_Manager::translateExprRec().

int SAT::Lit::getID

(

)

const [inline]

Definition at line 69 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 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().

void SAT::Lit::reset

(

)

[inline]

Definition at line 74 of file cnf.h.

References d_index.

Referenced by CVC3::SearchSat::getImplication().

---

Friends And Related Function Documentation

Lit operator!

(

const Lit &

lit

)

[friend]

Definition at line 75 of file cnf.h.

---

Member Data Documentation

int SAT::Lit::d_index [private]

Definition at line 52 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