CVC3
|
#include <variable.h>
Public Member Functions | |
Literal (const Variable &v, bool positive=true) | |
Literal () | |
Literal (VariableManager *vm, const Expr &e) | |
Variable & | getVar () |
const Variable & | getVar () const |
bool | isPositive () const |
bool | isNegative () const |
bool | isNull () const |
const Expr & | getExpr () const |
int | getValue () const |
int | getScope () const |
void | setValue (const Theorem &thm) |
void | setValue (const Theorem &thm, int scope) |
const Theorem & | getTheorem () const |
Theorem | deriveTheorem () const |
unsigned & | count () |
unsigned & | countPrev () |
int & | score () |
bool & | added () |
unsigned | count () const |
unsigned | countPrev () const |
int | score () const |
bool | added () const |
std::vector< std::pair< Clause, int > > & | wp () const |
std::string | toString () const |
Private Attributes | |
Variable | d_var |
bool | d_negative |
Friends | |
std::ostream & | operator<< (std::ostream &os, const Literal &l) |
bool | operator== (const Literal &l1, const Literal &l2) |
Definition at line 120 of file variable.h.
|
inline |
Definition at line 126 of file variable.h.
|
inline |
Definition at line 129 of file variable.h.
|
inline |
Definition at line 132 of file variable.h.
|
inline |
Definition at line 134 of file variable.h.
References d_var.
Referenced by getScope(), CVC3::operator!(), CVC3::operator<<(), and CVC3::printLit().
|
inline |
Definition at line 135 of file variable.h.
References d_var.
|
inline |
Definition at line 136 of file variable.h.
References d_negative.
|
inline |
Definition at line 137 of file variable.h.
References d_negative.
Referenced by CVC3::operator!(), CVC3::operator<<(), CVC3::printLit(), and CVC3::SearchEngineFast::recordFact().
|
inline |
Definition at line 138 of file variable.h.
References d_var, and CVC3::Variable::isNull().
|
inline |
Definition at line 140 of file variable.h.
References d_negative, d_var, CVC3::Variable::getExpr(), and CVC3::Variable::getNegExpr().
Referenced by CVC3::SearchEngineFast::bcp(), CVC3::SearchEngineFast::findSplitter(), CVC3::SearchEngineFast::fixConflict(), CVC3::SearchEngineFast::newIntAssumption(), CVC3::SearchEngineFast::propagate(), CVC3::SearchEngineFast::recordFact(), and CVC3::SearchEngineFast::updateLitCounts().
|
inline |
Definition at line 144 of file variable.h.
References d_negative, d_var, and CVC3::Variable::getValue().
Referenced by CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::SearchEngineFast::bcp(), CVC3::SearchEngineFast::findSplitter(), CVC3::SearchEngineFast::newIntAssumption(), CVC3::printLit(), CVC3::Circuit::propagate(), CVC3::SearchEngineFast::propagate(), CVC3::SearchEngineFast::recordFact(), CVC3::SearchEngineFast::split(), and CVC3::SearchEngineFast::traceConflict().
|
inline |
Definition at line 148 of file variable.h.
References CVC3::Variable::getScope(), and getVar().
Referenced by CVC3::printLit(), CVC3::SearchEngineFast::recordFact(), and CVC3::SearchEngineFast::traceConflict().
|
inline |
Definition at line 153 of file variable.h.
References d_var, CVC3::Theorem::getScope(), and CVC3::Variable::setValue().
Referenced by CVC3::SearchEngineFast::newIntAssumption(), and CVC3::SearchEngineFast::recordFact().
|
inline |
Definition at line 156 of file variable.h.
References d_var, and CVC3::Variable::setValue().
|
inline |
Definition at line 159 of file variable.h.
References d_var, and CVC3::Variable::getTheorem().
Referenced by CVC3::Circuit::propagate().
|
inline |
Definition at line 164 of file variable.h.
References d_var, and CVC3::Variable::deriveTheorem().
Referenced by CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::SearchEngineFast::recordFact(), and CVC3::SearchEngineFast::split().
|
inline |
Definition at line 166 of file variable.h.
References CVC3::Variable::count(), d_negative, and d_var.
Referenced by CVC3::ClauseValue::ClauseValue(), CVC3::operator<<(), CVC3::SearchImplBase::Splitter::operator=(), and CVC3::SearchImplBase::Splitter::Splitter().
|
inline |
Definition at line 167 of file variable.h.
References CVC3::Variable::countPrev(), d_negative, and d_var.
|
inline |
Definition at line 168 of file variable.h.
References d_negative, d_var, and CVC3::Variable::score().
Referenced by compareLits(), CVC3::SearchEngineFast::findSplitter(), and CVC3::operator<<().
|
inline |
Definition at line 169 of file variable.h.
References CVC3::Variable::added(), d_negative, and d_var.
Referenced by CVC3::SearchEngineFast::updateLitCounts().
|
inline |
Definition at line 171 of file variable.h.
References CVC3::Variable::count(), d_negative, and d_var.
|
inline |
Definition at line 172 of file variable.h.
References CVC3::Variable::countPrev(), d_negative, and d_var.
|
inline |
Definition at line 173 of file variable.h.
References d_negative, d_var, and CVC3::Variable::score().
|
inline |
Definition at line 174 of file variable.h.
References CVC3::Variable::added(), d_negative, and d_var.
|
inline |
Definition at line 176 of file variable.h.
References d_negative, d_var, and CVC3::Variable::wp().
Referenced by CVC3::SearchEngineFast::wp().
string CVC3::Literal::toString | ( | ) | const |
Definition at line 211 of file variable.cpp.
Referenced by CVC3::SearchEngineFast::bcp(), CVC3::SearchEngineFast::fixConflict(), CVC3::SearchEngineFast::newIntAssumption(), and CVC3::SearchEngineFast::split().
|
friend |
Definition at line 182 of file variable.h.
|
private |
Definition at line 122 of file variable.h.
Referenced by added(), count(), countPrev(), deriveTheorem(), getExpr(), getTheorem(), getValue(), getVar(), isNull(), score(), setValue(), and wp().
|
private |
Definition at line 123 of file variable.h.
Referenced by added(), count(), countPrev(), getExpr(), getValue(), isNegative(), isPositive(), score(), and wp().