MiniSat::Lit Class Reference

#include <minisat_types.h>

List of all members.

Public Member Functions

Static Public Member Functions

Private Member Functions

Private Attributes


Detailed Description

Definition at line 59 of file minisat_types.h.


Constructor & Destructor Documentation

MiniSat::Lit::Lit ( int  index  )  [inline, explicit, private]

Definition at line 62 of file minisat_types.h.

MiniSat::Lit::Lit (  )  [inline]

Definition at line 64 of file minisat_types.h.

Referenced by id(), operator~(), toLit(), and unsign().

MiniSat::Lit::Lit ( Var  var,
bool  sgn 
) [inline, explicit]

Definition at line 65 of file minisat_types.h.


Member Function Documentation

Lit MiniSat::Lit::operator~ ( void   )  const [inline]

Definition at line 66 of file minisat_types.h.

References Lit(), and x.

bool MiniSat::Lit::sign (  )  const [inline]

Definition at line 68 of file minisat_types.h.

References x.

Referenced by MiniSat::Solver::enqueue(), MiniSat::Solver::getValue(), MiniSat::miniSatToCVC(), toDimacs(), and toString().

int MiniSat::Lit::var (  )  const [inline]

Definition at line 69 of file minisat_types.h.

References x.

Referenced by MiniSat::Solver::analyze(), MiniSat::Solver::analyze_removable(), MiniSat::Solver::enqueue(), MiniSat::Solver::getLevel(), MiniSat::Solver::getPushID(), MiniSat::Solver::getReason(), MiniSat::Solver::getValue(), MiniSat::miniSatToCVC(), lastToFirst_lt::operator()(), MiniSat::Solver::protocolPropagation(), MiniSat::Solver::resolveTheoryImplication(), MiniSat::Solver::setLevel(), toDimacs(), toString(), and MiniSat::Solver::varBumpActivity().

int MiniSat::Lit::index (  )  const [inline]

Definition at line 70 of file minisat_types.h.

References x.

Referenced by MiniSat::Derivation::computeRootReason(), MiniSat::Solver::getWatches(), operator<(), operator==(), MiniSat::Solver::protocolPropagation(), and MiniSat::Solver::search().

static Lit MiniSat::Lit::toLit ( int  i  )  [inline, static]

Definition at line 71 of file minisat_types.h.

References Lit().

Lit MiniSat::Lit::unsign (  )  const [inline]

Definition at line 72 of file minisat_types.h.

References Lit(), and x.

static Lit MiniSat::Lit::id ( Lit  p,
bool  sgn 
) [inline, static]

Definition at line 73 of file minisat_types.h.

References Lit(), and x.

bool MiniSat::Lit::operator== ( const Lit  q  )  const [inline]

Definition at line 75 of file minisat_types.h.

References index().

Referenced by operator!=().

bool MiniSat::Lit::operator!= ( const Lit  q  )  const [inline]

Definition at line 76 of file minisat_types.h.

References operator==().

bool MiniSat::Lit::operator< ( const Lit  q  )  const [inline]

Definition at line 78 of file minisat_types.h.

References index().

unsigned int MiniSat::Lit::hash (  )  const [inline]

Definition at line 80 of file minisat_types.h.

References x.

std::string MiniSat::Lit::toString (  )  const [inline]

Definition at line 82 of file minisat_types.h.

References sign(), and var().

Referenced by MiniSat::Clause::toString(), and MiniSat::Solver::toString().

int MiniSat::Lit::toDimacs (  )  const [inline]

Definition at line 92 of file minisat_types.h.

References sign(), and var().


Member Data Documentation

int MiniSat::Lit::x [private]

Definition at line 60 of file minisat_types.h.

Referenced by hash(), id(), index(), operator~(), sign(), unsign(), and var().


The documentation for this class was generated from the following file:
Generated on Wed Nov 18 16:18:46 2009 for CVC3 by  doxygen 1.5.2