CVC3
2.4.1
|
A class representing a CNF clause (a smart pointer) More...
#include <clause.h>
A class representing a CNF clause (a smart pointer)
CVC3::Clause::Clause | ( | TheoryCore * | core, |
VariableManager * | vm, | ||
const Theorem & | clause, | ||
int | scope, | ||
const std::string & | file = "" , |
||
int | line = 0 |
||
) | [inline] |
Definition at line 96 of file clause.h.
References d_clause, CVC3::ClauseValue::d_refcount, and IF_DEBUG.
CVC3::Clause::Clause | ( | const Clause & | c | ) | [inline] |
Definition at line 103 of file clause.h.
References d_clause, and CVC3::ClauseValue::d_refcount.
CVC3::Clause::~Clause | ( | ) |
Definition at line 85 of file clause.cpp.
References FatalAssert, and CVC3::int2string().
int& CVC3::Clause::countOwner | ( | ) | [inline, private] |
Export owner refcounting to ClauseOwner.
Definition at line 89 of file clause.h.
References DebugAssert, d_clause, and CVC3::ClauseValue::d_refcountOwner.
Definition at line 115 of file clause.cpp.
References DebugAssert, CVC3::int2string(), d_clause, and CVC3::ClauseValue::d_refcount.
bool CVC3::Clause::isNull | ( | ) | const [inline] |
Definition at line 111 of file clause.h.
References d_clause.
Referenced by CVC3::operator<<(), getTheorem(), getScope(), getLiteral(), getLiterals(), wp(), dir(), sat(), markSat(), deleted(), CVC3::SearchEngineFast::fixConflict(), and CVC3::SearchEngineFast::analyzeUIPs().
size_t CVC3::Clause::size | ( | ) | const [inline] |
Definition at line 113 of file clause.h.
References d_clause, and CVC3::ClauseValue::d_literals.
Referenced by CVC3::operator<<(), getLiteral(), wp(), CVC3::SearchEngineFast::updateLitCounts(), CVC3::SearchEngineFast::findSplitter(), CVC3::SearchEngineFast::propagate(), CVC3::SearchEngineFast::unitPropagation(), CVC3::SearchEngineFast::fixConflict(), CVC3::SearchEngineFast::addNewClause(), CVC3::SearchEngineFast::analyzeUIPs(), CVC3::SearchEngineFast::traceConflict(), and CVC3::VariableValue::setValue().
const Theorem& CVC3::Clause::getTheorem | ( | ) | const [inline] |
Definition at line 117 of file clause.h.
References DebugAssert, isNull(), d_clause, and CVC3::ClauseValue::d_thm.
Referenced by CVC3::operator<<(), CVC3::SearchEngineFast::propagate(), CVC3::SearchEngineFast::unitPropagation(), CVC3::SearchEngineFast::fixConflict(), and CVC3::Variable::deriveThmRec().
int CVC3::Clause::getScope | ( | ) | const [inline] |
Definition at line 122 of file clause.h.
References isNull(), d_clause, and CVC3::ClauseValue::d_scope.
Referenced by CVC3::SearchEngineFast::analyzeUIPs(), and CVC3::VariableValue::setValue().
const Literal& CVC3::Clause::getLiteral | ( | size_t | i | ) | const [inline] |
Definition at line 127 of file clause.h.
References DebugAssert, isNull(), size(), CVC3::int2string(), d_clause, and CVC3::ClauseValue::d_literals.
Referenced by operator[](), and watched().
const Literal& CVC3::Clause::operator[] | ( | size_t | i | ) | const [inline] |
Definition at line 135 of file clause.h.
References getLiteral().
const std::vector<Literal>& CVC3::Clause::getLiterals | ( | ) | const [inline] |
Definition at line 138 of file clause.h.
References DebugAssert, isNull(), d_clause, and CVC3::ClauseValue::d_literals.
Referenced by CVC3::operator<<(), and CVC3::Variable::deriveThmRec().
size_t CVC3::Clause::wp | ( | int | i | ) | const [inline] |
Definition at line 143 of file clause.h.
References DebugAssert, isNull(), CVC3::int2string(), d_clause, and CVC3::ClauseValue::d_wp.
Referenced by CVC3::operator<<(), watched(), CVC3::SearchEngineFast::propagate(), CVC3::SearchEngineFast::addNewClause(), and CVC3::SearchEngineFast::analyzeUIPs().
const Literal& CVC3::Clause::watched | ( | int | i | ) | const [inline] |
Definition at line 151 of file clause.h.
References getLiteral(), and wp().
Referenced by CVC3::SearchEngineFast::bcp(), CVC3::SearchEngineFast::propagate(), CVC3::SearchEngineFast::addNewClause(), and CVC3::SearchEngineFast::analyzeUIPs().
size_t CVC3::Clause::wp | ( | int | i, |
size_t | l | ||
) | const [inline] |
Definition at line 153 of file clause.h.
References DebugAssert, isNull(), CVC3::int2string(), size(), TRACE, d_clause, and CVC3::ClauseValue::d_wp.
int CVC3::Clause::dir | ( | int | i | ) | const [inline] |
Definition at line 168 of file clause.h.
References DebugAssert, isNull(), CVC3::int2string(), d_clause, and CVC3::ClauseValue::d_dir.
Referenced by CVC3::operator<<(), and CVC3::SearchEngineFast::propagate().
int CVC3::Clause::dir | ( | int | i, |
int | d | ||
) | const [inline] |
Definition at line 176 of file clause.h.
References DebugAssert, isNull(), CVC3::int2string(), d_clause, and CVC3::ClauseValue::d_dir.
bool CVC3::Clause::sat | ( | ) | const [inline] |
Check if the clause marked as SAT.
Definition at line 187 of file clause.h.
References DebugAssert, isNull(), d_clause, and CVC3::ClauseValue::d_sat.
Referenced by CVC3::operator<<(), and CVC3::SearchEngineFast::bcp().
bool CVC3::Clause::sat | ( | bool | ignored | ) | const [inline] |
Precise version of sat(): check all the literals and cache the result.
Definition at line 192 of file clause.h.
References DebugAssert, isNull(), d_clause, CVC3::ClauseValue::d_sat, CVC3::ClauseValue::d_literals, and markSat().
void CVC3::Clause::markSat | ( | ) | const [inline] |
Definition at line 207 of file clause.h.
References DebugAssert, isNull(), d_clause, and CVC3::ClauseValue::d_sat.
Referenced by sat(), and CVC3::SearchEngineFast::propagate().
bool CVC3::Clause::deleted | ( | ) | const [inline] |
Definition at line 212 of file clause.h.
References DebugAssert, isNull(), d_clause, and CVC3::ClauseValue::d_deleted.
Referenced by CVC3::operator<<(), and CVC3::SearchEngineFast::bcp().
void CVC3::Clause::markDeleted | ( | ) | const |
Definition at line 96 of file clause.cpp.
References TRACE, DebugAssert, IF_DEBUG, and TRACE_MSG.
size_t CVC3::Clause::id | ( | ) | const [inline] |
bool CVC3::Clause::operator== | ( | const Clause & | c | ) | const [inline] |
int CVC3::Clause::owners | ( | ) | const [inline] |
Tell how many owners this clause has (for debugging)
Definition at line 225 of file clause.h.
References d_clause, and CVC3::ClauseValue::d_refcountOwner.
Referenced by CVC3::operator<<().
string CVC3::Clause::toString | ( | ) | const |
Definition at line 129 of file clause.cpp.
Referenced by CVC3::SearchEngineFast::propagate(), CVC3::SearchEngineFast::unitPropagation(), and CVC3::VariableValue::setValue().
friend class ClauseOwner [friend] |
std::ostream& operator<< | ( | std::ostream & | os, |
const Clause & | c | ||
) | [friend] |
Definition at line 135 of file clause.cpp.
ClauseValue* CVC3::Clause::d_clause [private] |
The only value member.
Definition at line 87 of file clause.h.
Referenced by operator=(), countOwner(), Clause(), isNull(), size(), getTheorem(), getScope(), getLiteral(), getLiterals(), wp(), dir(), sat(), markSat(), deleted(), id(), operator==(), owners(), CVC3::ClauseOwner::ClauseOwner(), CVC3::ClauseOwner::operator=(), CVC3::ClauseOwner::~ClauseOwner(), CVC3::ClauseOwner::operator Clause &(), and CVC3::ClauseOwner::operator const Clause &().