SAT::Lit Class Reference

#include <cnf.h>

List of all members.

Public Member Functions

Static Public Member Functions

Static Private Member Functions

Private Attributes

Friends


Detailed Description

Definition at line 48 of file cnf.h.


Constructor & Destructor Documentation

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

Definition at line 52 of file cnf.h.

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

Definition at line 53 of file cnf.h.

References d_index.


Member Function Documentation

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]
bool SAT::Lit::isPositive (  )  const [inline]
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]
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]
void SAT::Lit::reset (  )  [inline]

Definition at line 71 of file cnf.h.

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


Friends And Related Function Documentation

Lit operator! ( const Lit lit  )  [friend]

Definition at line 72 of file cnf.h.


Member Data Documentation

int SAT::Lit::d_index [private]

Definition at line 49 of file cnf.h.

Referenced by getID(), getVar(), isFalse(), isTrue(), isVar(), and Lit().


The documentation for this class was generated from the following file:
Generated by  doxygen 1.6.2-20100208