CVC3
Public Member Functions | Static Public Member Functions | Static Private Member Functions | Private Attributes | Friends | List of all members
SAT::Lit Class Reference

#include <cnf.h>

Collaboration diagram for SAT::Lit:
Collaboration graph

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 
)
inlineexplicit

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)
inlinestaticprivate

Definition at line 53 of file cnf.h.

References d_index.

Referenced by getFalse(), and getTrue().

static Lit SAT::Lit::getTrue ( )
inlinestatic

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 ( )
inlinestatic

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
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 CVC3::operator<(), and SAT::CNF_Formula_Impl::registerUnit().

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 getID(), getVar(), isFalse(), isInverted(), isNull(), isPositive(), isTrue(), isVar(), Lit(), mkLit(), and reset().


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