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 (  ) 

Definition at line 48 of file variable.cpp.

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


Member Function Documentation

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

Definition at line 162 of file variable.cpp.

References CVC3::SearchEngineRules::conflictRule(), d_val, CVC3::VariableValue::d_vm, DebugAssert, getAntecedent(), getAntecedentIdx(), getAssumpThm(), getExpr(), CVC3::Theorem::getExpr(), CVC3::Clause::getLiterals(), CVC3::VariableManager::getRules(), getScope(), CVC3::Clause::getTheorem(), getTheorem(), getValue(), IF_DEBUG, isNull(), CVC3::VariableValue::setValue(), CVC3::Theorem::toString(), toString(), and CVC3::SearchEngineRules::unitProp().

Referenced by deriveTheorem().

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

Definition at line 57 of file variable.cpp.

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

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

Definition at line 57 of file variable.h.

References d_val.

Referenced by deriveThmRec(), getAntecedent(), getAntecedentIdx(), getAssumpThm(), getExpr(), getNegExpr(), getScope(), getTheorem(), getValue(), CVC3::Literal::isNull(), operator=(), setAssumpThm(), setValue(), Variable(), and ~Variable().

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  ) 

Definition at line 134 of file variable.cpp.

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

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]

Definition at line 41 of file variable.h.

Referenced by added(), count(), countPrev(), deriveThmRec(), getAntecedent(), getAntecedentIdx(), getAssumpThm(), getExpr(), getNegExpr(), getScope(), getTheorem(), getValue(), isNull(), CVC3::operator<<(), operator=(), score(), setAssumpThm(), setValue(), Variable(), wp(), and ~Variable().


The documentation for this class was generated from the following files:
Generated on Wed Nov 18 16:17:23 2009 for CVC3 by  doxygen 1.5.2