CVC3  2.4.1
Public Member Functions | Private Member Functions | Private Attributes
CVC3::ClauseOwner Class Reference

Same as class Clause, but when destroyed, marks the clause as deleted. More...

#include <clause.h>

List of all members.

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)
ClauseOwneroperator= (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

Detailed Description

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.

Definition at line 242 of file clause.h.


Constructor & Destructor Documentation

CVC3::ClauseOwner::ClauseOwner ( )
inlineprivate

Disable default constructor.

Definition at line 245 of file clause.h.

CVC3::ClauseOwner::ClauseOwner ( const Clause c)
inline

Constructor from class Clause.

Definition at line 248 of file clause.h.

References CVC3::Clause::d_clause.

CVC3::ClauseOwner::ClauseOwner ( TheoryCore core,
VariableManager vm,
const Theorem clause,
int  scope 
)
inline

Construct a new Clause.

Definition at line 250 of file clause.h.

References CVC3::Clause::d_clause.

CVC3::ClauseOwner::ClauseOwner ( const ClauseOwner c)
inline

Copy constructor (keep track of refcounts)

Definition at line 255 of file clause.h.

References CVC3::Clause::d_clause.

CVC3::ClauseOwner::~ClauseOwner ( )
inline

Destructor: mark the clause as deleted.

Definition at line 269 of file clause.h.

References CVC3::Clause::d_clause, and FatalAssert.


Member Function Documentation

ClauseOwner& CVC3::ClauseOwner::operator= ( const ClauseOwner c)
inline

Assignment (keep track of refcounts)

Definition at line 259 of file clause.h.

References CVC3::Clause::d_clause, d_clause, and DebugAssert.

CVC3::ClauseOwner::operator Clause & ( )
inline

Automatic type conversion to Clause ref.

Definition at line 276 of file clause.h.

References CVC3::Clause::d_clause.

CVC3::ClauseOwner::operator const Clause & ( ) const
inline

Automatic type conversion to Clause const ref.

Definition at line 278 of file clause.h.

References CVC3::Clause::d_clause.


Member Data Documentation

Clause CVC3::ClauseOwner::d_clause
private

Definition at line 243 of file clause.h.

Referenced by operator=().


The documentation for this class was generated from the following file: