CVCL::ClauseValue Class Reference

#include <clause.h>

Collaboration diagram for CVCL::ClauseValue:

[legend]List of all members.

Public Member Functions

• ~ClauseValue ()

Private Member Functions

• ClauseValue (const ClauseValue &c)
• ClauseValue & operator= (const ClauseValue &c)
• IF_DEBUG (std::string d_file;int d_line)
• ClauseValue (TheoryCore *core, VariableManager *vm, const Theorem &clause, int scope)

Private Attributes

• int d_refcount

  Ref. counter.
  

• int d_refcountOwner

  Ref. counter of ClauseOwner classes holding it.
  

• Theorem d_thm
• int d_scope
• std::vector< Literal > d_literals
• size_t d_wp [2]
• int d_dir [2]
• CDO< bool > d_sat
• bool d_deleted

Friends

• class Clause

---

Detailed Description

Definition at line 50 of file clause.h.

---

Constructor & Destructor Documentation

CVCL::ClauseValue::ClauseValue (  const ClauseValue &  c  )  [private]

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

Definition at line 43 of file clause.cpp. References CVCL::Expr::arity(), CVCL::Expr::begin(), d_dir, d_literals, d_sat, d_wp, CVCL::Expr::end(), CVCL::Theorem::getExpr(), IF_DEBUG(), CVCL::Expr::isOr(), and CVCL::Theorem::toString().

CVCL::ClauseValue::~ClauseValue (   )

Definition at line 73 of file clause.cpp. References d_deleted, d_literals, d_refcount, IF_DEBUG(), CVCL::int2string(), and CVCL::TRACE.

---

Member Function Documentation

ClauseValue& CVCL::ClauseValue::operator= (  const ClauseValue &  c  )  [inline, private]

Definition at line 66 of file clause.h.

CVCL::ClauseValue::IF_DEBUG (  std::string d_file;int  d_line  )  [private]

Referenced by ClauseValue(), and ~ClauseValue().

---

Friends And Related Function Documentation

friend class Clause [friend]

Definition at line 51 of file clause.h.

---

Member Data Documentation

int CVCL::ClauseValue::d_refcount [private]

Ref. counter. Definition at line 54 of file clause.h. Referenced by CVCL::Clause::Clause(), CVCL::Clause::operator=(), CVCL::Clause::~Clause(), and ~ClauseValue().

int CVCL::ClauseValue::d_refcountOwner [private]

Ref. counter of ClauseOwner classes holding it. Definition at line 56 of file clause.h. Referenced by CVCL::Clause::countOwner(), and CVCL::Clause::owners().

Theorem CVCL::ClauseValue::d_thm [private]

Definition at line 58 of file clause.h. Referenced by CVCL::Clause::getTheorem().

int CVCL::ClauseValue::d_scope [private]

Definition at line 60 of file clause.h. Referenced by CVCL::Clause::getScope().

std::vector<Literal> CVCL::ClauseValue::d_literals [private]

Definition at line 63 of file clause.h. Referenced by ClauseValue(), CVCL::Clause::getLiteral(), CVCL::Clause::getLiterals(), CVCL::Clause::markDeleted(), CVCL::Clause::sat(), CVCL::Clause::size(), and ~ClauseValue().

size_t CVCL::ClauseValue::d_wp[2] [private]

Definition at line 69 of file clause.h. Referenced by ClauseValue(), and CVCL::Clause::wp().

int CVCL::ClauseValue::d_dir[2] [private]

Definition at line 73 of file clause.h. Referenced by ClauseValue(), and CVCL::Clause::dir().

CDO<bool> CVCL::ClauseValue::d_sat [private]

Definition at line 75 of file clause.h. Referenced by ClauseValue(), CVCL::Clause::markSat(), and CVCL::Clause::sat().

bool CVCL::ClauseValue::d_deleted [private]

Definition at line 77 of file clause.h. Referenced by CVCL::Clause::deleted(), CVCL::Clause::markDeleted(), and ~ClauseValue().

---

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

• clause.h
• clause.cpp

---