CVC3
Public Member Functions | Private Attributes | Friends | List of all members
CVC3::Literal Class Reference

#include <variable.h>

Collaboration diagram for CVC3::Literal:
Collaboration graph

Public Member Functions

 Literal (const Variable &v, bool positive=true)
 
 Literal ()
 
 Literal (VariableManager *vm, const Expr &e)
 
VariablegetVar ()
 
const VariablegetVar () const
 
bool isPositive () const
 
bool isNegative () const
 
bool isNull () const
 
const ExprgetExpr () const
 
int getValue () const
 
int getScope () const
 
void setValue (const Theorem &thm)
 
void setValue (const Theorem &thm, int scope)
 
const TheoremgetTheorem () 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 120 of file variable.h.

Constructor & Destructor Documentation

CVC3::Literal::Literal ( const Variable v,
bool  positive = true 
)
inline

Definition at line 126 of file variable.h.

CVC3::Literal::Literal ( )
inline

Definition at line 129 of file variable.h.

CVC3::Literal::Literal ( VariableManager vm,
const Expr e 
)
inline

Definition at line 132 of file variable.h.

Member Function Documentation

Variable& CVC3::Literal::getVar ( )
inline

Definition at line 134 of file variable.h.

References d_var.

Referenced by getScope(), CVC3::operator!(), CVC3::operator<<(), and CVC3::printLit().

const Variable& CVC3::Literal::getVar ( ) const
inline

Definition at line 135 of file variable.h.

References d_var.

bool CVC3::Literal::isPositive ( ) const
inline

Definition at line 136 of file variable.h.

References d_negative.

bool CVC3::Literal::isNegative ( ) const
inline
bool CVC3::Literal::isNull ( ) const
inline

Definition at line 138 of file variable.h.

References d_var, and CVC3::Variable::isNull().

const Expr& CVC3::Literal::getExpr ( ) const
inline
int CVC3::Literal::getValue ( ) const
inline
int CVC3::Literal::getScope ( ) const
inline
void CVC3::Literal::setValue ( const Theorem thm)
inline
void CVC3::Literal::setValue ( const Theorem thm,
int  scope 
)
inline

Definition at line 156 of file variable.h.

References d_var, and CVC3::Variable::setValue().

const Theorem& CVC3::Literal::getTheorem ( ) const
inline

Definition at line 159 of file variable.h.

References d_var, and CVC3::Variable::getTheorem().

Referenced by CVC3::Circuit::propagate().

Theorem CVC3::Literal::deriveTheorem ( ) const
inline
unsigned& CVC3::Literal::count ( )
inline
unsigned& CVC3::Literal::countPrev ( )
inline

Definition at line 167 of file variable.h.

References CVC3::Variable::countPrev(), d_negative, and d_var.

int& CVC3::Literal::score ( )
inline
bool& CVC3::Literal::added ( )
inline

Definition at line 169 of file variable.h.

References CVC3::Variable::added(), d_negative, and d_var.

Referenced by CVC3::SearchEngineFast::updateLitCounts().

unsigned CVC3::Literal::count ( ) const
inline

Definition at line 171 of file variable.h.

References CVC3::Variable::count(), d_negative, and d_var.

unsigned CVC3::Literal::countPrev ( ) const
inline

Definition at line 172 of file variable.h.

References CVC3::Variable::countPrev(), d_negative, and d_var.

int CVC3::Literal::score ( ) const
inline

Definition at line 173 of file variable.h.

References d_negative, d_var, and CVC3::Variable::score().

bool CVC3::Literal::added ( ) const
inline

Definition at line 174 of file variable.h.

References CVC3::Variable::added(), d_negative, and d_var.

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

Definition at line 176 of file variable.h.

References d_negative, d_var, and CVC3::Variable::wp().

Referenced by CVC3::SearchEngineFast::wp().

string CVC3::Literal::toString ( ) const

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 182 of file variable.h.

Member Data Documentation

Variable CVC3::Literal::d_var
private
bool CVC3::Literal::d_negative
private

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