CVC3::Variable Class Reference

#include <variable.h>

Collaboration diagram for CVC3::Variable:

Collaboration graph
[legend]

List of all members.

Public Member Functions

Private Member Functions

Private Attributes

Friends


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


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

Generated on Thu Oct 15 22:23:40 2009 for CVC3 by  doxygen 1.5.8