MiniSat::Lit Class Reference

#include <minisat_types.h>

List of all members.

Public Member Functions

• Lit ()
• Lit (Var var, bool sgn)
• Lit operator~ () const
• bool sign () const
• int var () const
• int index () const
• Lit unsign () const
• bool operator== (const Lit q) const
• bool operator!= (const Lit q) const
• bool operator< (const Lit q) const
• uint hash () const
• std::string toString () const
• int toDimacs () const

Static Public Member Functions

• static Lit toLit (int i)
• static Lit id (Lit p, bool sgn)

Private Member Functions

• Lit (int index)

Private Attributes

• int x

---

Detailed Description

Definition at line 58 of file minisat_types.h.

---

Constructor & Destructor Documentation

MiniSat::Lit::Lit

(

int

index

)

[inline, explicit, private]

Definition at line 61 of file minisat_types.h.

MiniSat::Lit::Lit

(

)

[inline]

Definition at line 63 of file minisat_types.h.

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

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

Definition at line 64 of file minisat_types.h.

---

Member Function Documentation

Lit MiniSat::Lit::operator~

(

void

)

const [inline]

Definition at line 65 of file minisat_types.h.

References Lit(), and x.

bool MiniSat::Lit::sign

(

)

const [inline]

Definition at line 67 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 68 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 69 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 70 of file minisat_types.h.

References Lit().

Lit MiniSat::Lit::unsign

(

)

const [inline]

Definition at line 71 of file minisat_types.h.

References Lit(), and x.

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

Definition at line 72 of file minisat_types.h.

References Lit(), and x.

bool MiniSat::Lit::operator==

(

const Lit

q

)

const [inline]

Definition at line 74 of file minisat_types.h.

References index().

Referenced by operator!=().

bool MiniSat::Lit::operator!=

(

const Lit

q

)

const [inline]

Definition at line 75 of file minisat_types.h.

References operator==().

bool MiniSat::Lit::operator<

(

const Lit

q

)

const [inline]

Definition at line 77 of file minisat_types.h.

References index().

uint MiniSat::Lit::hash

(

)

const [inline]

Definition at line 79 of file minisat_types.h.

References x.

std::string MiniSat::Lit::toString

(

)

const [inline]

Definition at line 81 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 91 of file minisat_types.h.

References sign(), and var().

---

Member Data Documentation

int MiniSat::Lit::x [private]

Definition at line 59 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:

• minisat_types.h

---