CVCL::ClauseOwner Class Reference

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

#include <clause.h>

Collaboration diagram for CVCL::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 250 of file clause.h.

---

Constructor & Destructor Documentation

CVCL::ClauseOwner::ClauseOwner (   )  [inline, private]

Disable default constructor. Definition at line 253 of file clause.h.

CVCL::ClauseOwner::ClauseOwner (  const Clause &  c  )  [inline]

Constructor from class Clause. Definition at line 256 of file clause.h.

CVCL::ClauseOwner::ClauseOwner (  TheoryCore *  core, VariableManager *  vm, const Theorem &  clause, int  scope )  [inline]

Construct a new Clause. Definition at line 258 of file clause.h.

CVCL::ClauseOwner::ClauseOwner (  const ClauseOwner &  c  )  [inline]

Copy constructor (keep track of refcounts). Definition at line 263 of file clause.h.

CVCL::ClauseOwner::~ClauseOwner (   )  [inline]

Destructor: mark the clause as deleted. Definition at line 277 of file clause.h.

---

Member Function Documentation

ClauseOwner& CVCL::ClauseOwner::operator= (  const ClauseOwner &  c  )  [inline]

Assignment (keep track of refcounts). Definition at line 267 of file clause.h. References CVCL::Clause::countOwner(), and d_clause.

CVCL::ClauseOwner::operator Clause & (   )  [inline]

Automatic type conversion to Clause ref. Definition at line 284 of file clause.h.

CVCL::ClauseOwner::operator const Clause & (   )  const [inline]

Automatic type conversion to Clause const ref. Definition at line 286 of file clause.h.

---

Member Data Documentation

Clause CVCL::ClauseOwner::d_clause [private]

Definition at line 251 of file clause.h. Referenced by operator=().

---

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

• clause.h

---