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:

[legend]

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).
  

• 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

---

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

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:

• clause.h