CVC3::ClauseOwner Class Reference

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

#include <clause.h>

Collaboration diagram for CVC3::ClauseOwner:

Collaboration graph
[legend]

List of all members.

Public Member Functions

Private Member Functions

Private Attributes


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 (  )  [inline, private]

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 d_clause, CVC3::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

Definition at line 243 of file clause.h.

Referenced by operator=().


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

Generated on Thu Oct 15 22:18:06 2009 for CVC3 by  doxygen 1.5.8