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