CVCL::AssumptionsValue Class Reference

#include <assumptions_value.h>

List of all members.

Public Member Functions

Private Member Functions

Static Private Member Functions

Private Attributes


Detailed Description

Definition at line 49 of file assumptions_value.h.

Constructor & Destructor Documentation

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


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

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

bool operator== const AssumptionsValue a1,
const AssumptionsValue a2

Definition at line 97 of file assumptions_value.h.

bool operator!= const AssumptionsValue a1,
const AssumptionsValue a2

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:
Generated on Thu Apr 13 16:57:42 2006 for CVC Lite by  doxygen 1.4.4