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

#include <variable.h>

Public Member Functions

 Variable ()
 Variable (VariableManager *vm, const Expr &e)
 Variable (const Variable &l)
 ~Variable ()
Variableoperator= (const Variable &l)
bool isNull () const
const ExprgetExpr () const
const ExprgetNegExpr () const
int getValue () const
int getScope () const
const TheoremgetTheorem () const
const ClausegetAntecedent () const
int getAntecedentIdx () const
const TheoremgetAssumpThm () 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

VariableValued_val

Friends

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

Detailed Description

Definition at line 39 of file variable.h.

Constructor & Destructor Documentation

CVC3::Variable::Variable ( )
inline

Definition at line 46 of file variable.h.

CVC3::Variable::Variable ( VariableManager vm,
const Expr e 
)

Definition at line 37 of file variable.cpp.

References CVC3::VariableValue::d_refcount, and d_val.

CVC3::Variable::Variable ( const Variable l)

Definition at line 43 of file variable.cpp.

References CVC3::VariableValue::d_refcount, d_val, and isNull().

CVC3::Variable::~Variable ( )

Member Function Documentation

Theorem CVC3::Variable::deriveThmRec ( bool  checkAssump) const
private
Variable & CVC3::Variable::operator= ( const Variable l)
bool CVC3::Variable::isNull ( ) const
inline
const Expr & CVC3::Variable::getExpr ( ) const

Definition at line 68 of file variable.cpp.

References d_val, CVC3::VariableValue::getExpr(), and isNull().

Referenced by deriveThmRec(), CVC3::Literal::getExpr(), and CVC3::printLit().

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

Definition at line 75 of file variable.cpp.

References d_val, CVC3::VariableValue::getNegExpr(), and isNull().

Referenced by CVC3::Literal::getExpr().

int CVC3::Variable::getValue ( ) const

Definition at line 83 of file variable.cpp.

References d_val, CVC3::VariableValue::getValue(), and isNull().

Referenced by deriveThmRec(), and CVC3::Literal::getValue().

int CVC3::Variable::getScope ( ) const

Definition at line 90 of file variable.cpp.

References d_val, CVC3::VariableValue::getScope(), and isNull().

Referenced by deriveThmRec(), and CVC3::Literal::getScope().

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

Definition at line 96 of file variable.cpp.

References d_val, CVC3::VariableValue::getTheorem(), and isNull().

Referenced by deriveThmRec(), and CVC3::Literal::getTheorem().

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

Definition at line 103 of file variable.cpp.

References d_val, CVC3::VariableValue::getAntecedent(), and isNull().

Referenced by deriveThmRec().

int CVC3::Variable::getAntecedentIdx ( ) const

Definition at line 110 of file variable.cpp.

References d_val, CVC3::VariableValue::getAntecedentIdx(), and isNull().

Referenced by deriveThmRec().

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

Definition at line 116 of file variable.cpp.

References d_val, CVC3::VariableValue::getAssumpThm(), and isNull().

Referenced by deriveThmRec().

void CVC3::Variable::setValue ( int  val,
const Clause c,
int  idx 
)

Definition at line 126 of file variable.cpp.

References d_val, DebugAssert, isNull(), and CVC3::VariableValue::setValue().

Referenced by CVC3::Literal::setValue().

void CVC3::Variable::setValue ( const Theorem thm)
void CVC3::Variable::setValue ( const Theorem thm,
int  scope 
)

Definition at line 140 of file variable.cpp.

References d_val, DebugAssert, isNull(), and CVC3::VariableValue::setValue().

void CVC3::Variable::setAssumpThm ( const Theorem a,
int  scope 
)

Definition at line 146 of file variable.cpp.

References d_val, DebugAssert, isNull(), and CVC3::VariableValue::setAssumpThm().

Theorem CVC3::Variable::deriveTheorem ( ) const

Definition at line 156 of file variable.cpp.

References deriveThmRec().

Referenced by CVC3::Literal::deriveTheorem().

unsigned & CVC3::Variable::count ( bool  neg)
inline

Definition at line 342 of file variable.h.

References CVC3::VariableValue::count(), and d_val.

Referenced by CVC3::Literal::count().

unsigned & CVC3::Variable::countPrev ( bool  neg)
inline

Definition at line 343 of file variable.h.

References CVC3::VariableValue::countPrev(), and d_val.

Referenced by CVC3::Literal::countPrev().

int & CVC3::Variable::score ( bool  neg)
inline

Definition at line 345 of file variable.h.

References d_val, and CVC3::VariableValue::score().

Referenced by CVC3::Literal::score().

bool & CVC3::Variable::added ( bool  neg)
inline

Definition at line 346 of file variable.h.

References CVC3::VariableValue::added(), and d_val.

Referenced by CVC3::Literal::added().

unsigned CVC3::Variable::count ( bool  neg) const
inline

Definition at line 348 of file variable.h.

References CVC3::VariableValue::count(), and d_val.

unsigned CVC3::Variable::countPrev ( bool  neg) const
inline

Definition at line 349 of file variable.h.

References CVC3::VariableValue::countPrev(), and d_val.

int CVC3::Variable::score ( bool  neg) const
inline

Definition at line 351 of file variable.h.

References d_val, and CVC3::VariableValue::score().

bool CVC3::Variable::added ( bool  neg) const
inline

Definition at line 352 of file variable.h.

References CVC3::VariableValue::added(), and d_val.

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

Definition at line 354 of file variable.h.

References CVC3::VariableValue::d_negwp, d_val, and CVC3::VariableValue::d_wp.

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

string CVC3::Variable::toString ( ) const

Definition at line 195 of file variable.cpp.

Referenced by deriveThmRec().

Friends And Related Function Documentation

bool operator== ( const Variable l1,
const Variable l2 
)
friend

Definition at line 112 of file variable.h.

std::ostream& operator<< ( std::ostream &  os,
const Variable l 
)
friend

Definition at line 202 of file variable.cpp.

Member Data Documentation

VariableValue* CVC3::Variable::d_val
private

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