CVC3
2.4.1
|
#include <clause.h>
Public Member Functions | |
~ClauseValue () | |
Private Member Functions | |
ClauseValue (const ClauseValue &c) | |
ClauseValue & | operator= (const ClauseValue &c) |
ClauseValue (TheoryCore *core, VariableManager *vm, const Theorem &clause, int scope) | |
Private Attributes | |
int | d_refcount |
Ref. counter. More... | |
int | d_refcountOwner |
Ref. counter of ClauseOwner classes holding it. More... | |
Theorem | d_thm |
int | d_scope |
std::vector< Literal > | d_literals |
size_t | d_wp [2] |
int | d_dir [2] |
CDO< bool > | d_sat |
bool | d_deleted |
Friends | |
class | Clause |
|
private |
|
private |
Definition at line 35 of file clause.cpp.
References CVC3::Expr::arity(), CVC3::Literal::count(), d_dir, d_literals, d_sat, d_wp, DebugAssert, CVC3::Theorem::getExpr(), IF_DEBUG, CVC3::Expr::isOr(), and CVC3::Theorem::toString().
CVC3::ClauseValue::~ClauseValue | ( | ) |
Definition at line 65 of file clause.cpp.
References d_deleted, d_literals, d_refcount, FatalAssert, IF_DEBUG, CVC3::int2string(), TRACE, and TRACE_MSG.
|
inlineprivate |
|
private |
Ref. counter.
Definition at line 46 of file clause.h.
Referenced by CVC3::Clause::Clause(), CVC3::Clause::operator=(), and ~ClauseValue().
|
private |
Ref. counter of ClauseOwner classes holding it.
Definition at line 48 of file clause.h.
Referenced by CVC3::Clause::countOwner(), and CVC3::Clause::owners().
|
private |
Definition at line 50 of file clause.h.
Referenced by CVC3::Clause::getTheorem().
|
private |
Definition at line 52 of file clause.h.
Referenced by CVC3::Clause::getScope().
|
private |
Definition at line 55 of file clause.h.
Referenced by ClauseValue(), CVC3::Clause::getLiteral(), CVC3::Clause::getLiterals(), CVC3::Clause::sat(), CVC3::Clause::size(), and ~ClauseValue().
|
private |
Definition at line 61 of file clause.h.
Referenced by ClauseValue(), and CVC3::Clause::wp().
|
private |
Definition at line 65 of file clause.h.
Referenced by ClauseValue(), and CVC3::Clause::dir().
|
private |
Definition at line 67 of file clause.h.
Referenced by ClauseValue(), CVC3::Clause::markSat(), and CVC3::Clause::sat().
|
private |
Definition at line 69 of file clause.h.
Referenced by CVC3::Clause::deleted(), and ~ClauseValue().