CVCL::Variable Class Reference

#include <variable.h>

Collaboration diagram for CVCL::Variable:

[legend]List of all members.

Public Member Functions

Variable ()
Variable (VariableManager *vm, const Expr &e)
Variable (const Variable &l)
~Variable ()
Variable & operator= (const Variable &l)
bool isNull () const
const Expr & getExpr () const
const Expr & getNegExpr () const
int getValue () const
int getScope () const
const Theorem & getTheorem () const
const Clause & getAntecedent () const
int getAntecedentIdx () const
const Theorem & getAssumpThm () const
void setValue (int val, const Clause &c, int idx)
void setValue (const Theorem &thm)
void setValue (const Theorem &thm, int scope)
void setAssumpThm (const Theorem &a, int scope)
Theorem deriveTheorem () const
unsigned & count (bool neg)
unsigned & countPrev (bool neg)
int & score (bool neg)
bool & added (bool neg)
unsigned count (bool neg) const
unsigned countPrev (bool neg) const
int score (bool neg) const
bool added (bool neg) const
std::vector< std::pair< Clause,
int > > & wp (bool neg) const
std::string toString () const

Private Member Functions

Theorem deriveThmRec (bool checkAssump) const

Private Attributes

VariableValue * d_val

Friends

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

Detailed Description

Definition at line 47 of file variable.h.

Constructor & Destructor Documentation

CVCL::Variable::Variable ( ) [inline]

Definition at line 54 of file variable.h.

CVCL::Variable::Variable ( VariableManager * vm,

const Expr & e

)

Definition at line 45 of file variable.cpp.
References CVCL::VariableValue::d_refcount, and d_val.

CVCL::Variable::Variable ( const Variable & l )

Definition at line 51 of file variable.cpp.
References CVCL::VariableValue::d_refcount, d_val, and isNull().

CVCL::Variable::~Variable ( )

Definition at line 56 of file variable.cpp.
References CVCL::VariableValue::d_refcount, d_val, CVCL::VariableValue::d_vm, CVCL::VariableManager::gc(), and isNull().

Member Function Documentation

Theorem CVCL::Variable::deriveThmRec ( bool checkAssump ) const [private]

Definition at line 170 of file variable.cpp.
References CVCL::SearchEngineRules::conflictRule(), d_val, CVCL::VariableValue::d_vm, getAntecedent(), getAntecedentIdx(), getAssumpThm(), getExpr(), CVCL::Theorem::getExpr(), CVCL::Clause::getLiterals(), CVCL::VariableManager::getRules(), getScope(), CVCL::Clause::getTheorem(), getTheorem(), getValue(), IF_DEBUG(), CVCL::Theorem::isNull(), isNull(), CVCL::VariableValue::setValue(), CVCL::Theorem::toString(), toString(), and CVCL::SearchEngineRules::unitProp().
Referenced by deriveTheorem().

Variable & CVCL::Variable::operator= ( const Variable & l )

Definition at line 65 of file variable.cpp.
References CVCL::VariableValue::d_refcount, d_val, CVCL::VariableValue::d_vm, CVCL::VariableManager::gc(), and isNull().

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

Definition at line 65 of file variable.h.
References d_val.
Referenced by deriveThmRec(), getAntecedent(), getAntecedentIdx(), getAssumpThm(), getExpr(), getNegExpr(), getScope(), getTheorem(), getValue(), CVCL::Literal::isNull(), operator=(), setAssumpThm(), setValue(), Variable(), and ~Variable().

const Expr & CVCL::Variable::getExpr ( ) const

Definition at line 76 of file variable.cpp.
References d_val, CVCL::VariableValue::getExpr(), and isNull().
Referenced by deriveThmRec(), CVCL::Literal::getExpr(), and CVCL::printLit().

const Expr & CVCL::Variable::getNegExpr ( ) const

Definition at line 83 of file variable.cpp.
References d_val, CVCL::VariableValue::getNegExpr(), and isNull().
Referenced by CVCL::Literal::getExpr().

int CVCL::Variable::getValue ( ) const

Definition at line 91 of file variable.cpp.
References d_val, CVCL::VariableValue::getValue(), and isNull().
Referenced by deriveThmRec(), and CVCL::Literal::getValue().

int CVCL::Variable::getScope ( ) const

Definition at line 98 of file variable.cpp.
References d_val, CVCL::VariableValue::getScope(), and isNull().
Referenced by deriveThmRec(), and CVCL::Literal::getScope().

const Theorem & CVCL::Variable::getTheorem ( ) const

Definition at line 104 of file variable.cpp.
References d_val, CVCL::VariableValue::getTheorem(), and isNull().
Referenced by deriveThmRec(), and CVCL::Literal::getTheorem().

const Clause & CVCL::Variable::getAntecedent ( ) const

Definition at line 111 of file variable.cpp.
References d_val, CVCL::VariableValue::getAntecedent(), and isNull().
Referenced by deriveThmRec().

int CVCL::Variable::getAntecedentIdx ( ) const

Definition at line 118 of file variable.cpp.
References d_val, CVCL::VariableValue::getAntecedentIdx(), and isNull().
Referenced by deriveThmRec().

const Theorem & CVCL::Variable::getAssumpThm ( ) const

Definition at line 124 of file variable.cpp.
References d_val, CVCL::VariableValue::getAssumpThm(), and isNull().
Referenced by deriveThmRec().

void CVCL::Variable::setValue ( int val,

const Clause & c,

int idx

)

Definition at line 134 of file variable.cpp.
References d_val, isNull(), and CVCL::VariableValue::setValue().
Referenced by CVCL::Literal::setValue().

void CVCL::Variable::setValue ( const Theorem & thm )

Definition at line 142 of file variable.cpp.
References d_val, CVCL::Theorem::getScope(), isNull(), and CVCL::VariableValue::setValue().

void CVCL::Variable::setValue ( const Theorem & thm,

int scope

)

Definition at line 148 of file variable.cpp.
References d_val, isNull(), and CVCL::VariableValue::setValue().

void CVCL::Variable::setAssumpThm ( const Theorem & a,

int scope

)

Definition at line 154 of file variable.cpp.
References d_val, isNull(), and CVCL::VariableValue::setAssumpThm().

Theorem CVCL::Variable::deriveTheorem ( ) const

Definition at line 164 of file variable.cpp.
References deriveThmRec().
Referenced by CVCL::Literal::deriveTheorem().

unsigned & CVCL::Variable::count ( bool neg ) [inline]

Definition at line 347 of file variable.h.
References CVCL::VariableValue::count(), and d_val.
Referenced by CVCL::Literal::count().

unsigned & CVCL::Variable::countPrev ( bool neg ) [inline]

Definition at line 348 of file variable.h.
References CVCL::VariableValue::countPrev(), and d_val.
Referenced by CVCL::Literal::countPrev().

int & CVCL::Variable::score ( bool neg ) [inline]

Definition at line 350 of file variable.h.
References d_val, and CVCL::VariableValue::score().
Referenced by CVCL::Literal::score().

bool & CVCL::Variable::added ( bool neg ) [inline]

Definition at line 351 of file variable.h.
References CVCL::VariableValue::added(), and d_val.
Referenced by CVCL::Literal::added().

unsigned CVCL::Variable::count ( bool neg ) const [inline]

Definition at line 353 of file variable.h.
References CVCL::VariableValue::count(), and d_val.

unsigned CVCL::Variable::countPrev ( bool neg ) const [inline]

Definition at line 354 of file variable.h.
References CVCL::VariableValue::countPrev(), and d_val.

int CVCL::Variable::score ( bool neg ) const [inline]

Definition at line 356 of file variable.h.
References d_val, and CVCL::VariableValue::score().

bool CVCL::Variable::added ( bool neg ) const [inline]

Definition at line 357 of file variable.h.
References CVCL::VariableValue::added(), and d_val.

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

Definition at line 359 of file variable.h.
References CVCL::VariableValue::d_negwp, d_val, and CVCL::VariableValue::d_wp.
Referenced by CVCL::Literal::wp().

string CVCL::Variable::toString ( ) const

Definition at line 203 of file variable.cpp.
Referenced by deriveThmRec().

Friends And Related Function Documentation

bool operator== ( const Variable & l1,

const Variable & l2

) [friend]

Definition at line 120 of file variable.h.

std::ostream& operator<< ( std::ostream & os,

const Variable & l

) [friend]

Member Data Documentation

VariableValue* CVCL::Variable::d_val [private]

Definition at line 49 of file variable.h.
Referenced by added(), count(), countPrev(), deriveThmRec(), getAntecedent(), getAntecedentIdx(), getAssumpThm(), getExpr(), getNegExpr(), getScope(), getTheorem(), getValue(), isNull(), CVCL::operator<<(), operator=(), score(), setAssumpThm(), setValue(), Variable(), wp(), and ~Variable().

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

Generated on Thu Apr 13 16:57:45 2006 for CVC Lite by

1.4.4