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