CVC3
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


Detailed Description

Definition at line 52 of file cnf.h.


Constructor & Destructor Documentation

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

Definition at line 56 of file cnf.h.

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

Definition at line 57 of file cnf.h.


Member Function Documentation

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

Definition at line 54 of file cnf.h.

Referenced by getTrue(), and reset().

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

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

References d_index.

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

References d_index.

Referenced by MiniSat::cvcToMiniSat(), and CVC3::SearchSat::findSplitterRec().

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

Definition at line 68 of file cnf.h.

References CVC3::abs(), and 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 70 of file cnf.h.

Referenced by CVC3::operator<(), and SAT::CNF_Formula_Impl::registerUnit().

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

Definition at line 75 of file cnf.h.

References d_index, and mkLit().

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


Friends And Related Function Documentation

Lit operator! ( const Lit lit) [friend]

Definition at line 76 of file cnf.h.


Member Data Documentation

int SAT::Lit::d_index [private]

Definition at line 53 of file cnf.h.

Referenced by getFalse(), isFalse(), isInverted(), isNull(), isPositive(), isTrue(), isVar(), and reset().


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