#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)
Detailed Description
Definition at line 120 of file variable.h.
Constructor & Destructor Documentation
| 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.
Member Function Documentation
| Variable& CVC3::Literal::getVar | ( | ) | [inline] |
Definition at line 134 of file variable.h.
References d_var.
Referenced by getScope(), CVC3::operator!(), CVC3::operator<<(), and CVC3::printLit().
| 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::operator!(), CVC3::operator<<(), CVC3::printLit(), and CVC3::SearchEngineFast::recordFact().
| 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::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().
| 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::SearchEngineFast::addNonLiteralFact(), CVC3::SearchEngineFast::bcp(), CVC3::SearchEngineFast::findSplitter(), CVC3::SearchEngineFast::newIntAssumption(), CVC3::printLit(), CVC3::SearchEngineFast::propagate(), CVC3::Circuit::propagate(), CVC3::SearchEngineFast::recordFact(), CVC3::SearchEngineFast::split(), and CVC3::SearchEngineFast::traceConflict().
| int CVC3::Literal::getScope | ( | ) | const [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().
| void CVC3::Literal::setValue | ( | const Theorem & | thm | ) | [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().
| 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::addNonLiteralFact(), CVC3::SearchEngineFast::recordFact(), and CVC3::SearchEngineFast::split().
| unsigned& CVC3::Literal::count | ( | ) | [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=(), CVC3::SearchImplBase::Splitter::Splitter(), and CVC3::SearchEngineFast::updateLitScores().
| unsigned& CVC3::Literal::countPrev | ( | ) | [inline] |
Definition at line 167 of file variable.h.
References CVC3::Variable::countPrev(), d_negative, and d_var.
Referenced by CVC3::SearchEngineFast::updateLitScores().
| int& CVC3::Literal::score | ( | ) | [inline] |
Definition at line 168 of file variable.h.
References d_negative, d_var, and CVC3::Variable::score().
Referenced by compareLits(), CVC3::SearchEngineFast::findSplitter(), CVC3::operator<<(), and CVC3::SearchEngineFast::updateLitScores().
| bool& CVC3::Literal::added | ( | ) | [inline] |
Definition at line 169 of file variable.h.
References CVC3::Variable::added(), d_negative, and d_var.
Referenced by CVC3::SearchEngineFast::updateLitCounts(), and CVC3::SearchEngineFast::updateLitScores().
| unsigned CVC3::Literal::count | ( | ) | const [inline] |
Definition at line 171 of file variable.h.
References CVC3::Variable::count(), d_negative, and d_var.
| unsigned CVC3::Literal::countPrev | ( | ) | const [inline] |
Definition at line 172 of file variable.h.
References CVC3::Variable::countPrev(), d_negative, and d_var.
| int CVC3::Literal::score | ( | ) | const [inline] |
Definition at line 173 of file variable.h.
References d_negative, d_var, and CVC3::Variable::score().
| bool CVC3::Literal::added | ( | ) | const [inline] |
Definition at line 174 of file variable.h.
References CVC3::Variable::added(), d_negative, and d_var.
| std::vector<std::pair<Clause, int> >& CVC3::Literal::wp | ( | ) | const [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(), CVC3::SearchEngineFast::split(), and CVC3::SearchEngineFast::updateLitScores().
Friends And Related Function Documentation
| std::ostream& operator<< | ( | std::ostream & | os, |
| const Literal & | l | ||
| ) | [friend] |
Definition at line 182 of file variable.h.
Member Data Documentation
Variable CVC3::Literal::d_var [private] |
Definition at line 122 of file variable.h.
Referenced by added(), count(), countPrev(), deriveTheorem(), getExpr(), getTheorem(), getValue(), getVar(), isNull(), score(), setValue(), and wp().
bool CVC3::Literal::d_negative [private] |
Definition at line 123 of file variable.h.
Referenced by added(), count(), countPrev(), getExpr(), getValue(), isNegative(), isPositive(), score(), and wp().
The documentation for this class was generated from the following files:
