CVC3
2.4.1
|
#include <variable.h>
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 d_val, and CVC3::VariableValue::d_refcount.
CVC3::Variable::Variable | ( | const Variable & | l | ) |
Definition at line 43 of file variable.cpp.
References isNull(), d_val, and CVC3::VariableValue::d_refcount.
CVC3::Variable::~Variable | ( | ) |
Definition at line 48 of file variable.cpp.
References isNull(), d_val, CVC3::VariableValue::d_refcount, CVC3::VariableValue::d_vm, and CVC3::VariableManager::gc().
Theorem CVC3::Variable::deriveThmRec | ( | bool | checkAssump | ) | const [private] |
Definition at line 162 of file variable.cpp.
References DebugAssert, isNull(), getValue(), toString(), getTheorem(), getAssumpThm(), getAntecedent(), getAntecedentIdx(), CVC3::Clause::getLiterals(), d_val, CVC3::VariableValue::d_vm, CVC3::VariableManager::getRules(), CVC3::SearchEngineRules::unitProp(), CVC3::Clause::getTheorem(), CVC3::SearchEngineRules::conflictRule(), IF_DEBUG, CVC3::Theorem::getExpr(), getExpr(), CVC3::Theorem::toString(), CVC3::VariableValue::setValue(), and getScope().
Referenced by deriveTheorem().
Definition at line 57 of file variable.cpp.
References isNull(), d_val, CVC3::VariableValue::d_refcount, CVC3::VariableValue::d_vm, and CVC3::VariableManager::gc().
bool CVC3::Variable::isNull | ( | ) | const [inline] |
Definition at line 57 of file variable.h.
References d_val.
Referenced by Variable(), ~Variable(), operator=(), getExpr(), getNegExpr(), getValue(), getScope(), getTheorem(), getAntecedent(), getAntecedentIdx(), getAssumpThm(), setValue(), setAssumpThm(), deriveThmRec(), and CVC3::Literal::isNull().
const Expr & CVC3::Variable::getExpr | ( | ) | const |
Definition at line 68 of file variable.cpp.
References isNull(), d_val, and CVC3::VariableValue::getExpr().
Referenced by CVC3::printLit(), deriveThmRec(), and CVC3::Literal::getExpr().
const Expr & CVC3::Variable::getNegExpr | ( | ) | const |
Definition at line 75 of file variable.cpp.
References isNull(), d_val, and CVC3::VariableValue::getNegExpr().
Referenced by CVC3::Literal::getExpr().
int CVC3::Variable::getValue | ( | ) | const |
Definition at line 83 of file variable.cpp.
References isNull(), d_val, and CVC3::VariableValue::getValue().
Referenced by deriveThmRec(), and CVC3::Literal::getValue().
int CVC3::Variable::getScope | ( | ) | const |
Definition at line 90 of file variable.cpp.
References isNull(), d_val, and CVC3::VariableValue::getScope().
Referenced by deriveThmRec(), and CVC3::Literal::getScope().
const Theorem & CVC3::Variable::getTheorem | ( | ) | const |
Definition at line 96 of file variable.cpp.
References isNull(), d_val, and CVC3::VariableValue::getTheorem().
Referenced by deriveThmRec(), and CVC3::Literal::getTheorem().
const Clause & CVC3::Variable::getAntecedent | ( | ) | const |
Definition at line 103 of file variable.cpp.
References isNull(), d_val, and CVC3::VariableValue::getAntecedent().
Referenced by deriveThmRec().
int CVC3::Variable::getAntecedentIdx | ( | ) | const |
Definition at line 110 of file variable.cpp.
References isNull(), d_val, and CVC3::VariableValue::getAntecedentIdx().
Referenced by deriveThmRec().
const Theorem & CVC3::Variable::getAssumpThm | ( | ) | const |
Definition at line 116 of file variable.cpp.
References isNull(), d_val, and CVC3::VariableValue::getAssumpThm().
Referenced by deriveThmRec().
void CVC3::Variable::setValue | ( | int | val, |
const Clause & | c, | ||
int | idx | ||
) |
Definition at line 126 of file variable.cpp.
References DebugAssert, isNull(), d_val, 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 DebugAssert, isNull(), d_val, CVC3::VariableValue::setValue(), and CVC3::Theorem::getScope().
void CVC3::Variable::setValue | ( | const Theorem & | thm, |
int | scope | ||
) |
Definition at line 140 of file variable.cpp.
References DebugAssert, isNull(), d_val, and CVC3::VariableValue::setValue().
void CVC3::Variable::setAssumpThm | ( | const Theorem & | a, |
int | scope | ||
) |
Definition at line 146 of file variable.cpp.
References DebugAssert, isNull(), d_val, 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 d_val, and CVC3::VariableValue::count().
Referenced by CVC3::Literal::count().
unsigned & CVC3::Variable::countPrev | ( | bool | neg | ) | [inline] |
Definition at line 343 of file variable.h.
References d_val, and CVC3::VariableValue::countPrev().
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 d_val, and CVC3::VariableValue::added().
Referenced by CVC3::Literal::added().
unsigned CVC3::Variable::count | ( | bool | neg | ) | const [inline] |
Definition at line 348 of file variable.h.
References d_val, and CVC3::VariableValue::count().
unsigned CVC3::Variable::countPrev | ( | bool | neg | ) | const [inline] |
Definition at line 349 of file variable.h.
References d_val, and CVC3::VariableValue::countPrev().
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 d_val, and CVC3::VariableValue::added().
std::vector< std::pair< Clause, int > > & CVC3::Variable::wp | ( | bool | neg | ) | const [inline] |
Definition at line 354 of file variable.h.
References d_val, CVC3::VariableValue::d_negwp, 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().
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.
VariableValue* CVC3::Variable::d_val [private] |
Definition at line 41 of file variable.h.
Referenced by Variable(), ~Variable(), operator=(), getExpr(), getNegExpr(), getValue(), getScope(), getTheorem(), getAntecedent(), getAntecedentIdx(), getAssumpThm(), setValue(), setAssumpThm(), deriveThmRec(), CVC3::operator<<(), isNull(), count(), countPrev(), score(), added(), and wp().