CVC3  2.4.1
Public Member Functions | Private Attributes | Friends
CVC3::Literal Class Reference

#include <variable.h>

List of all members.

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: