CVC3::Variable Class Reference

#include <variable.h>

Collaboration diagram for CVC3::Variable:

Public Member Functions
	Variable ()
	Variable (VariableManager *vm, const Expr &e)
	Variable (const Variable &l)
	~Variable ()
Variable &	operator= (const Variable &l)
bool	isNull () const
const Expr &	getExpr () const
const Expr &	getNegExpr () const
int	getValue () const
int	getScope () const
const Theorem &	getTheorem () const
const Clause &	getAntecedent () const
int	getAntecedentIdx () const
const Theorem &	getAssumpThm () 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
VariableValue *	d_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

(

)

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(), getTheorem(), CVC3::Clause::getTheorem(), getValue(), IF_DEBUG, isNull(), CVC3::VariableValue::setValue(), toString(), CVC3::Theorem::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:

• variable.h
• variable.cpp