CVC3
2.4.1
|
#include <variable.h>
Public Member Functions | |
~VariableValue () | |
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, int scope) |
void | setAssumpThm (const Theorem &a, int scope) |
unsigned & | count (bool neg) |
unsigned & | countPrev (bool neg) |
int & | score (bool neg) |
bool & | added (bool neg) |
void * | operator new (size_t size, MemoryManager *mm) |
void | operator delete (void *pMem, MemoryManager *mm) |
void | operator delete (void *) |
Private Member Functions | |
VariableValue (VariableManager *vm, const Expr &e) | |
Private Attributes | |
VariableManager * | d_vm |
int | d_refcount |
Expr | d_expr |
Expr | d_neg |
unsigned | d_count |
unsigned | d_countPrev |
int | d_score |
unsigned | d_negCount |
unsigned | d_negCountPrev |
int | d_negScore |
bool | d_added |
bool | d_negAdded |
std::vector< std::pair< Clause, int > > | d_wp |
std::vector< std::pair< Clause, int > > | d_negwp |
CDO< int > * | d_val |
CDO< int > * | d_scope |
CDO< Theorem > * | d_thm |
CDO< Clause > * | d_ante |
CDO< int > * | d_anteIdx |
CDO< Theorem > * | d_assump |
Friends | |
class | Variable |
class | VariableManager |
std::ostream & | operator<< (std::ostream &os, const VariableValue &v) |
bool | operator== (const VariableValue &v1, const VariableValue &v2) |
Definition at line 206 of file variable.h.
|
inlineprivate |
Definition at line 245 of file variable.h.
Referenced by CVC3::VariableManager::newVariableValue().
CVC3::VariableValue::~VariableValue | ( | ) |
|
inline |
Definition at line 255 of file variable.h.
References d_expr.
Referenced by CVC3::Variable::getExpr(), CVC3::VariableManager::HashLV::operator()(), CVC3::VariableManager::EqLV::operator()(), CVC3::operator<<(), and setValue().
|
inline |
Definition at line 257 of file variable.h.
References d_expr, d_neg, CVC3::Expr::isNull(), and CVC3::Expr::negate().
Referenced by CVC3::Variable::getNegExpr().
|
inline |
Definition at line 265 of file variable.h.
References d_val, and CVC3::CDO< T >::get().
Referenced by CVC3::Variable::getValue(), CVC3::operator<<(), and setValue().
|
inline |
Definition at line 270 of file variable.h.
References d_scope, and CVC3::CDO< T >::get().
Referenced by CVC3::Variable::getScope(), CVC3::operator<<(), and setValue().
|
inline |
Definition at line 275 of file variable.h.
References d_thm.
Referenced by CVC3::Variable::getTheorem(), CVC3::operator<<(), and setValue().
|
inline |
Definition at line 281 of file variable.h.
References d_ante.
Referenced by CVC3::Variable::getAntecedent(), CVC3::operator<<(), and setValue().
|
inline |
Definition at line 287 of file variable.h.
References d_anteIdx, and CVC3::CDO< T >::get().
Referenced by CVC3::Variable::getAntecedentIdx(), and CVC3::operator<<().
|
inline |
Definition at line 292 of file variable.h.
References d_assump.
Referenced by CVC3::Variable::getAssumpThm().
void CVC3::VariableValue::setValue | ( | int | val, |
const Clause & | c, | ||
int | idx | ||
) |
Definition at line 242 of file variable.cpp.
References d_ante, d_anteIdx, d_scope, d_thm, d_val, d_vm, DebugAssert, CVC3::VariableManager::getCM(), CVC3::ContextManager::getCurrentContext(), getExpr(), CVC3::Clause::getScope(), getScope(), getTheorem(), getValue(), IF_DEBUG, CVC3::int2string(), CVC3::CDO< T >::set(), CVC3::Clause::size(), CVC3::Clause::toString(), and CVC3::Expr::toString().
Referenced by CVC3::Variable::deriveThmRec(), and CVC3::Variable::setValue().
void CVC3::VariableValue::setValue | ( | const Theorem & | thm, |
int | scope | ||
) |
Definition at line 295 of file variable.cpp.
References d_ante, d_expr, d_scope, d_thm, d_val, d_vm, DebugAssert, getAntecedent(), CVC3::VariableManager::getCM(), CVC3::ContextManager::getCurrentContext(), CVC3::Theorem::getExpr(), IF_DEBUG, CVC3::CDO< T >::set(), CVC3::Theorem::toString(), and CVC3::Expr::toString().
void CVC3::VariableValue::setAssumpThm | ( | const Theorem & | a, |
int | scope | ||
) |
Definition at line 328 of file variable.cpp.
References d_assump, d_val, d_vm, CVC3::VariableManager::getCM(), CVC3::ContextManager::getCurrentContext(), and IF_DEBUG.
Referenced by CVC3::Variable::setAssumpThm().
|
inline |
Definition at line 308 of file variable.h.
References d_count, and d_negCount.
Referenced by CVC3::Variable::count().
|
inline |
Definition at line 312 of file variable.h.
References d_countPrev, and d_negCountPrev.
Referenced by CVC3::Variable::countPrev().
|
inline |
Definition at line 316 of file variable.h.
References d_negScore, and d_score.
Referenced by CVC3::Variable::score().
|
inline |
Definition at line 320 of file variable.h.
References d_added, and d_negAdded.
Referenced by CVC3::Variable::added().
|
inline |
Definition at line 326 of file variable.h.
|
inline |
Definition at line 329 of file variable.h.
|
inline |
Definition at line 332 of file variable.h.
|
friend |
Definition at line 207 of file variable.h.
|
friend |
Definition at line 208 of file variable.h.
|
friend |
Definition at line 337 of file variable.cpp.
|
friend |
Definition at line 336 of file variable.h.
|
private |
Definition at line 210 of file variable.h.
Referenced by CVC3::Variable::deriveThmRec(), CVC3::Variable::operator=(), setAssumpThm(), setValue(), and CVC3::Variable::~Variable().
|
private |
Definition at line 211 of file variable.h.
Referenced by CVC3::Variable::operator=(), CVC3::Variable::Variable(), and CVC3::Variable::~Variable().
|
private |
Definition at line 213 of file variable.h.
Referenced by getExpr(), getNegExpr(), and setValue().
|
private |
Definition at line 215 of file variable.h.
Referenced by getNegExpr().
|
private |
Definition at line 220 of file variable.h.
Referenced by count().
|
private |
Definition at line 221 of file variable.h.
Referenced by countPrev().
|
private |
Definition at line 222 of file variable.h.
Referenced by score().
|
private |
Definition at line 224 of file variable.h.
Referenced by count().
|
private |
Definition at line 225 of file variable.h.
Referenced by countPrev().
|
private |
Definition at line 226 of file variable.h.
Referenced by score().
|
private |
Definition at line 228 of file variable.h.
Referenced by added().
|
private |
Definition at line 229 of file variable.h.
Referenced by added().
|
private |
Definition at line 231 of file variable.h.
Referenced by CVC3::Variable::wp().
|
private |
Definition at line 232 of file variable.h.
Referenced by CVC3::Variable::wp().
|
private |
Definition at line 237 of file variable.h.
Referenced by getValue(), setAssumpThm(), setValue(), and ~VariableValue().
|
private |
Definition at line 238 of file variable.h.
Referenced by getScope(), setValue(), and ~VariableValue().
Definition at line 240 of file variable.h.
Referenced by getTheorem(), setValue(), and ~VariableValue().
Definition at line 241 of file variable.h.
Referenced by getAntecedent(), setValue(), and ~VariableValue().
|
private |
Definition at line 242 of file variable.h.
Referenced by getAntecedentIdx(), setValue(), and ~VariableValue().
Definition at line 243 of file variable.h.
Referenced by getAssumpThm(), setAssumpThm(), and ~VariableValue().