CVCL::Literal Class Reference

#include <variable.h>

Collaboration diagram for CVCL::Literal:

[legend]List of all members.

Public Member Functions

• Literal (const Variable &v, bool positive=true)
• Literal ()
• Literal (VariableManager *vm, const Expr &e)
• Variable & getVar ()
• const Variable & getVar () const
• bool isPositive () const
• bool isNegative () const
• bool isNull () const
• const Expr & getExpr () const
• int getValue () const
• int getScope () const
• void setValue (const Theorem &thm)
• void setValue (const Theorem &thm, int scope)
• const Theorem & getTheorem () const
• Theorem deriveTheorem () const
• unsigned & count ()
• unsigned & countPrev ()
• int & score ()
• bool & added ()
• unsigned count () const
• unsigned countPrev () const
• int score () const
• bool added () const
• std::vector< std::pair< Clause,
  int > > & wp () const
• std::string toString () const

Private Attributes

• Variable d_var
• bool d_negative

Friends

• std::ostream & operator<< (std::ostream &os, const Literal &l)
• bool operator== (const Literal &l1, const Literal &l2)

---

Detailed Description

Definition at line 128 of file variable.h.

---

Constructor & Destructor Documentation

CVCL::Literal::Literal (  const Variable &  v, bool  positive = true )  [inline]

Definition at line 134 of file variable.h.

CVCL::Literal::Literal (   )  [inline]

Definition at line 137 of file variable.h.

CVCL::Literal::Literal (  VariableManager *  vm, const Expr &  e )  [inline]

Definition at line 140 of file variable.h.

---

Member Function Documentation

Variable& CVCL::Literal::getVar (   )  [inline]

Definition at line 142 of file variable.h. References d_var. Referenced by getScope(), CVCL::operator!(), CVCL::operator<<(), and CVCL::printLit().

const Variable& CVCL::Literal::getVar (   )  const [inline]

Definition at line 143 of file variable.h. References d_var.

bool CVCL::Literal::isPositive (   )  const [inline]

Definition at line 144 of file variable.h. References d_negative.

bool CVCL::Literal::isNegative (   )  const [inline]

Definition at line 145 of file variable.h. References d_negative. Referenced by CVCL::SearchEngineFast::addLiteralFact(), CVCL::operator!(), CVCL::operator<<(), CVCL::printLit(), and CVCL::SearchEngineFast::recordFact().

bool CVCL::Literal::isNull (   )  const [inline]

Definition at line 146 of file variable.h. References d_var, and CVCL::Variable::isNull().

const Expr& CVCL::Literal::getExpr (   )  const [inline]

Definition at line 148 of file variable.h. References d_negative, d_var, CVCL::Variable::getExpr(), and CVCL::Variable::getNegExpr(). Referenced by CVCL::SearchEngineFast::addLiteralFact(), CVCL::SearchEngineFast::bcp(), CVCL::SearchEngineFast::findSplitter(), CVCL::SearchEngineFast::fixConflict(), CVCL::SearchEngineFast::newIntAssumption(), CVCL::SearchEngineFast::propagate(), CVCL::SearchEngineFast::recordFact(), and CVCL::SearchEngineFast::updateLitCounts().

int CVCL::Literal::getValue (   )  const [inline]

Definition at line 152 of file variable.h. References d_negative, d_var, and CVCL::Variable::getValue(). Referenced by CVCL::SearchEngineFast::addLiteralFact(), CVCL::SearchEngineFast::addNonLiteralFact(), CVCL::SearchEngineFast::bcp(), CVCL::SearchEngineFast::findSplitter(), CVCL::SearchEngineFast::newIntAssumption(), CVCL::printLit(), CVCL::SearchEngineFast::propagate(), CVCL::Circuit::propagate(), CVCL::SearchEngineFast::recordFact(), CVCL::SearchEngineFast::split(), CVCL::SearchEngineFast::traceConflict(), and CVCL::SearchEngineFast::unitPropagation().

int CVCL::Literal::getScope (   )  const [inline]

Definition at line 156 of file variable.h. References CVCL::Variable::getScope(), and getVar(). Referenced by CVCL::printLit(), CVCL::SearchEngineFast::recordFact(), and CVCL::SearchEngineFast::traceConflict().

void CVCL::Literal::setValue (  const Theorem &  thm  )  [inline]

Definition at line 161 of file variable.h. References d_var, CVCL::Theorem::getScope(), and CVCL::Variable::setValue(). Referenced by CVCL::SearchEngineFast::addLiteralFact(), CVCL::SearchEngineFast::newIntAssumption(), and CVCL::SearchEngineFast::recordFact().

void CVCL::Literal::setValue (  const Theorem &  thm, int  scope )  [inline]

Definition at line 164 of file variable.h. References d_var, and CVCL::Variable::setValue().

const Theorem& CVCL::Literal::getTheorem (   )  const [inline]

Definition at line 167 of file variable.h. References d_var, and CVCL::Variable::getTheorem(). Referenced by CVCL::Circuit::propagate().

Theorem CVCL::Literal::deriveTheorem (   )  const [inline]

Definition at line 172 of file variable.h. References d_var, and CVCL::Variable::deriveTheorem(). Referenced by CVCL::SearchEngineFast::addLiteralFact(), CVCL::SearchEngineFast::addNonLiteralFact(), CVCL::SearchEngineFast::recordFact(), and CVCL::SearchEngineFast::split().

unsigned& CVCL::Literal::count (   )  [inline]

Definition at line 174 of file variable.h. References CVCL::Variable::count(), d_negative, and d_var. Referenced by CVCL::operator<<(), CVCL::SearchImplBase::Splitter::operator=(), CVCL::SearchImplBase::Splitter::Splitter(), CVCL::SearchEngineFast::updateLitScores(), and CVCL::SearchImplBase::Splitter::~Splitter().

unsigned& CVCL::Literal::countPrev (   )  [inline]

Definition at line 175 of file variable.h. References CVCL::Variable::countPrev(), d_negative, and d_var. Referenced by CVCL::SearchEngineFast::updateLitScores().

int& CVCL::Literal::score (   )  [inline]

Definition at line 176 of file variable.h. References d_negative, d_var, and CVCL::Variable::score(). Referenced by CVCL::SearchEngineFast::addSplitter(), compareLits(), CVCL::SearchEngineFast::findSplitter(), CVCL::operator<<(), and CVCL::SearchEngineFast::updateLitScores().

bool& CVCL::Literal::added (   )  [inline]

Definition at line 177 of file variable.h. References CVCL::Variable::added(), d_negative, and d_var. Referenced by CVCL::SearchEngineFast::addSplitter(), CVCL::SearchEngineFast::updateLitCounts(), and CVCL::SearchEngineFast::updateLitScores().

unsigned CVCL::Literal::count (   )  const [inline]

Definition at line 179 of file variable.h. References CVCL::Variable::count(), d_negative, and d_var.

unsigned CVCL::Literal::countPrev (   )  const [inline]

Definition at line 180 of file variable.h. References CVCL::Variable::countPrev(), d_negative, and d_var.

int CVCL::Literal::score (   )  const [inline]

Definition at line 181 of file variable.h. References d_negative, d_var, and CVCL::Variable::score().

bool CVCL::Literal::added (   )  const [inline]

Definition at line 182 of file variable.h. References CVCL::Variable::added(), d_negative, and d_var.

std::vector<std::pair<Clause, int> >& CVCL::Literal::wp (   )  const [inline]

Definition at line 184 of file variable.h. References d_negative, d_var, and CVCL::Variable::wp(). Referenced by CVCL::SearchEngineFast::wp().

string CVCL::Literal::toString (   )  const

Definition at line 219 of file variable.cpp. Referenced by CVCL::SearchEngineFast::addLiteralFact(), CVCL::SearchEngineFast::bcp(), CVCL::SearchEngineFast::fixConflict(), CVCL::SearchEngineFast::newIntAssumption(), CVCL::SearchEngineFast::split(), CVCL::SearchEngineFast::unitPropagation(), and CVCL::SearchEngineFast::updateLitScores().

---

Friends And Related Function Documentation

std::ostream& operator<< (  std::ostream &  os, const Literal &  l )  [friend]

bool operator== (  const Literal &  l1, const Literal &  l2 )  [friend]

Definition at line 190 of file variable.h.

---

Member Data Documentation

Variable CVCL::Literal::d_var [private]

Definition at line 130 of file variable.h. Referenced by added(), count(), countPrev(), deriveTheorem(), getExpr(), getTheorem(), getValue(), getVar(), isNull(), score(), setValue(), and wp().

bool CVCL::Literal::d_negative [private]

Definition at line 131 of file variable.h. Referenced by added(), count(), countPrev(), getExpr(), getValue(), isNegative(), isPositive(), score(), and wp().

---

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

• variable.h
• variable.cpp

---