CVC3  2.4.1
Public Member Functions | Static Public Member Functions | Static Private Member Functions | Private Attributes | Friends
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


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 SAT::Var::isNull(), and d_index.


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 getTrue(), and getFalse().

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]
bool SAT::Lit::isPositive ( ) const [inline]
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]
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]
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 mkLit(), Lit(), isNull(), isPositive(), isInverted(), isFalse(), isTrue(), isVar(), getID(), getVar(), and reset().


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