CVC3
|
Same as class Clause, but when destroyed, marks the clause as deleted. More...
#include <clause.h>
Public Member Functions | |
ClauseOwner (const Clause &c) | |
Constructor from class Clause. | |
ClauseOwner (TheoryCore *core, VariableManager *vm, const Theorem &clause, int scope) | |
Construct a new Clause. | |
ClauseOwner (const ClauseOwner &c) | |
Copy constructor (keep track of refcounts) | |
ClauseOwner & | operator= (const ClauseOwner &c) |
Assignment (keep track of refcounts) | |
~ClauseOwner () | |
Destructor: mark the clause as deleted. | |
operator Clause & () | |
Automatic type conversion to Clause ref. | |
operator const Clause & () const | |
Automatic type conversion to Clause const ref. | |
Private Member Functions | |
ClauseOwner () | |
Disable default constructor. | |
Private Attributes | |
Clause | d_clause |
Same as class Clause, but when destroyed, marks the clause as deleted.
Needed for backtraking data structures. When the SAT solver backtracks, some clauses will be thrown away automatically, and we need to mark those as deleted.
|
inlineprivate |
|
inline |
Constructor from class Clause.
Definition at line 248 of file clause.h.
References CVC3::Clause::d_clause.
|
inline |
|
inline |
Copy constructor (keep track of refcounts)
Definition at line 255 of file clause.h.
References CVC3::Clause::d_clause.
|
inline |
Destructor: mark the clause as deleted.
Definition at line 269 of file clause.h.
References CVC3::Clause::d_clause, and FatalAssert.
|
inline |
Assignment (keep track of refcounts)
Definition at line 259 of file clause.h.
References CVC3::Clause::d_clause, d_clause, and DebugAssert.
|
inline |
Automatic type conversion to Clause ref.
Definition at line 276 of file clause.h.
References CVC3::Clause::d_clause.
|
inline |
Automatic type conversion to Clause const ref.
Definition at line 278 of file clause.h.
References CVC3::Clause::d_clause.
|
private |
Definition at line 243 of file clause.h.
Referenced by operator=().