CVC3
2.4.1
|
#include <variable.h>
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) |
Definition at line 39 of file variable.h.
|
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().
|
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().
Definition at line 57 of file variable.cpp.
References CVC3::VariableValue::d_refcount, d_val, CVC3::VariableValue::d_vm, CVC3::VariableManager::gc(), and isNull().
|
inline |
Definition at line 57 of file variable.h.
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().
|
inline |
Definition at line 342 of file variable.h.
References CVC3::VariableValue::count(), and d_val.
Referenced by CVC3::Literal::count().
|
inline |
Definition at line 343 of file variable.h.
References CVC3::VariableValue::countPrev(), and d_val.
Referenced by CVC3::Literal::countPrev().
|
inline |
Definition at line 345 of file variable.h.
References d_val, and CVC3::VariableValue::score().
Referenced by CVC3::Literal::score().
|
inline |
Definition at line 346 of file variable.h.
References CVC3::VariableValue::added(), and d_val.
Referenced by CVC3::Literal::added().
|
inline |
Definition at line 348 of file variable.h.
References CVC3::VariableValue::count(), and d_val.
|
inline |
Definition at line 349 of file variable.h.
References CVC3::VariableValue::countPrev(), and d_val.
|
inline |
Definition at line 351 of file variable.h.
References d_val, and CVC3::VariableValue::score().
|
inline |
Definition at line 352 of file variable.h.
References CVC3::VariableValue::added(), and d_val.
|
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().
Definition at line 112 of file variable.h.
|
friend |
Definition at line 202 of file variable.cpp.
|
private |
Definition at line 41 of file variable.h.
Referenced by added(), count(), countPrev(), deriveThmRec(), getAntecedent(), getAntecedentIdx(), getAssumpThm(), getExpr(), getNegExpr(), getScope(), getTheorem(), getValue(), CVC3::operator<<(), operator=(), score(), setAssumpThm(), setValue(), Variable(), wp(), and ~Variable().