CVCL::AssumptionsValue Class Reference

#include <assumptions_value.h>

List of all members.

Public Member Functions

• std::string toString () const

Private Member Functions

• AssumptionsValue (int refcount=0)

  Constructor.
  

• AssumptionsValue (const AssumptionsValue &a)

  Copy constructor: reset d_const flag and refcount.
  

• AssumptionsValue (const std::vector< Theorem > &v)
• AssumptionsValue (const Theorem &t1, const Theorem &t2)

  Constructor from two theorems (optimized for common case).
  

• void add (const Theorem &t)
• void add (const AssumptionsValue &a)
• const Theorem & find (const Expr &e) const

Static Private Member Functions

• static void mergeVectors (const std::vector< Theorem > &v1, const std::vector< Theorem > &v2, std::vector< Theorem > &v)

Private Attributes

• int d_refcount
• bool d_const
• std::vector< Theorem > d_vector

Friends

• class Assumptions
• std::ostream & operator<< (std::ostream &os, const AssumptionsValue &assump)
• bool operator== (const AssumptionsValue &a1, const AssumptionsValue &a2)
• bool operator!= (const AssumptionsValue &a1, const AssumptionsValue &a2)

---

Detailed Description

Definition at line 49 of file assumptions_value.h.

---

Constructor & Destructor Documentation

CVCL::AssumptionsValue::AssumptionsValue (  int  refcount = 0  )  [inline, private]

Constructor. Definition at line 59 of file assumptions_value.h.

CVCL::AssumptionsValue::AssumptionsValue (  const AssumptionsValue &  a  )  [inline, private]

Copy constructor: reset d_const flag and refcount. Definition at line 61 of file assumptions_value.h.

AssumptionsValue::AssumptionsValue (  const std::vector< Theorem > &  v  )  [private]

Creates the set of assumptions from a vector of theorems. Theorems that do not have premises are not included, since they are valid without any context and thus do not add any information in the assumption tracking. Definition at line 45 of file assumptions_value.cpp. References d_vector, CVCL::debugger, std::endl(), IF_DEBUG(), and TheoremEq().

AssumptionsValue::AssumptionsValue (  const Theorem &  t1, const Theorem &  t2 )  [private]

Constructor from two theorems (optimized for common case). Definition at line 83 of file assumptions_value.cpp. References CVCL::compare(), d_vector, CVCL::Assumptions::empty(), CVCL::Theorem::getAssumptions(), and CVCL::Theorem::isAssump().

---

Member Function Documentation

static void CVCL::AssumptionsValue::mergeVectors (  const std::vector< Theorem > &  v1, const std::vector< Theorem > &  v2, std::vector< Theorem > &  v )  [static, private]

Referenced by add().

void AssumptionsValue::add (  const Theorem &  t  )  [private]

Definition at line 151 of file assumptions_value.cpp. References CVCL::compare(), d_const, d_vector, CVCL::Assumptions::empty(), CVCL::Theorem::getAssumptions(), CVCL::Theorem::isAssump(), CVCL::Theorem::isNull(), and CVCL::Theorem::toString(). Referenced by CVCL::Assumptions::add().

void AssumptionsValue::add (  const AssumptionsValue &  a  )  [private]

Definition at line 177 of file assumptions_value.cpp. References d_const, d_vector, and mergeVectors().

const Theorem & AssumptionsValue::find (  const Expr &  e  )  const [private]

Definition at line 194 of file assumptions_value.cpp. References CVCL::compare(), and d_vector. Referenced by CVCL::Assumptions::find().

string AssumptionsValue::toString (   )  const

Definition at line 218 of file assumptions_value.cpp. Referenced by CVCL::Assumptions::toString().

---

Friends And Related Function Documentation

friend class Assumptions [friend]

Definition at line 50 of file assumptions_value.h.

std::ostream& operator<< (  std::ostream &  os, const AssumptionsValue &  assump )  [friend]

bool operator== (  const AssumptionsValue &  a1, const AssumptionsValue &  a2 )  [friend]

Definition at line 97 of file assumptions_value.h.

bool operator!= (  const AssumptionsValue &  a1, const AssumptionsValue &  a2 )  [friend]

Definition at line 101 of file assumptions_value.h.

---

Member Data Documentation

int CVCL::AssumptionsValue::d_refcount [private]

Definition at line 52 of file assumptions_value.h. Referenced by CVCL::Assumptions::Assumptions(), CVCL::Assumptions::init(), CVCL::Assumptions::operator=(), CVCL::Assumptions::setConst(), and CVCL::Assumptions::~Assumptions().

bool CVCL::AssumptionsValue::d_const [private]

Definition at line 54 of file assumptions_value.h. Referenced by add(), CVCL::Assumptions::clear(), CVCL::Assumptions::isConst(), and CVCL::Assumptions::setConst().

std::vector<Theorem> CVCL::AssumptionsValue::d_vector [private]

Definition at line 55 of file assumptions_value.h. Referenced by add(), AssumptionsValue(), CVCL::Assumptions::begin(), CVCL::Assumptions::clear(), CVCL::Assumptions::empty(), CVCL::Assumptions::end(), find(), CVCL::Assumptions::findTheorem(), CVCL::operator!=(), CVCL::operator<<(), CVCL::operator==(), CVCL::Assumptions::operator[](), and CVCL::Assumptions::size().

---

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

• assumptions_value.h
• assumptions_value.cpp

---