CVC3::Variable Class Reference
#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
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 | |||
| ) |
| 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().
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] |
| unsigned CVC3::Variable::countPrev | ( | bool | neg | ) | const [inline] |
| int CVC3::Variable::score | ( | bool | neg | ) | const [inline] |
| bool CVC3::Variable::added | ( | bool | neg | ) | const [inline] |
| 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 |
Friends And Related Function Documentation
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:
