CVCL::Assumptions Class Reference

#include <assumptions.h>

Collaboration diagram for CVCL::Assumptions:

[legend]List of all members.

Public Member Functions

• Assumptions ()

  Default constructor: no value is created.
  

• Assumptions (const std::vector< Theorem > &v)

  Constructor from a vector of theorems.
  

• Assumptions (const Theorem &t)

  Constructor for one theorem (common case).
  

• Assumptions (const Theorem &t1, const Theorem &t2)

  Constructor for two theorems (common case).
  

• ~Assumptions ()
• Assumptions (const Assumptions &assump)
• Assumptions & operator= (const Assumptions &assump)
• bool isNull () const
• void init ()
• Assumptions copy () const
• void add (const Theorem &t)
• void add (const Assumptions &a)
• void clear ()
• int size () const
• bool empty () const
• bool isConst () const
• void setConst ()
• std::string toString () const
• void print () const
• const Theorem & operator[] (const Expr &e) const
• const Theorem & find (const Expr &e) const
• iterator begin () const
• iterator end () const
• void add (const iterator &it)

Private Member Functions

• Assumptions (AssumptionsValue *v)
• const Theorem & findTheorem (const Expr &e) const

Static Private Member Functions

• static bool findExpr (const Assumptions &a, const Expr &e, std::vector< Theorem > &gamma)
• static bool findExprs (const Assumptions &a, const std::vector< Expr > &es, std::vector< Theorem > &gamma)

Private Attributes

• AssumptionsValue * d_val

Friends

• Assumptions operator- (const Assumptions &a, const Expr &e)

  Returns all (recursive) assumptions except e.
  

• Assumptions operator- (const Assumptions &a, const std::vector< Expr > &es)

  Returns all (recursive) assumptions except those in es.
  

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

Classes

• class iterator

  Iterator for the Assumptions: points to class Theorem. More...
  

---

Detailed Description

Definition at line 56 of file assumptions.h.

---

Constructor & Destructor Documentation

Assumptions::Assumptions (  AssumptionsValue *  v  )  [private]

Definition at line 39 of file assumptions.cpp. References CVCL::AssumptionsValue::d_refcount, and d_val.

CVCL::Assumptions::Assumptions (   )  [inline]

Default constructor: no value is created. Definition at line 74 of file assumptions.h. Referenced by copy().

CVCL::Assumptions::Assumptions (  const std::vector< Theorem > &  v  )

Constructor from a vector of theorems.

Assumptions::Assumptions (  const Theorem &  t  )

Constructor for one theorem (common case). Definition at line 143 of file assumptions.cpp. References CVCL::AssumptionsValue::d_refcount, and d_val.

Assumptions::Assumptions (  const Theorem &  t1, const Theorem &  t2 )

Constructor for two theorems (common case). Definition at line 151 of file assumptions.cpp. References CVCL::AssumptionsValue::d_refcount, and d_val.

Assumptions::~Assumptions (   )

Definition at line 157 of file assumptions.cpp. References CVCL::AssumptionsValue::d_refcount, d_val, and CVCL::int2string().

Assumptions::Assumptions (  const Assumptions &  assump  )

Definition at line 166 of file assumptions.cpp. References CVCL::AssumptionsValue::d_refcount, d_val, and CVCL::int2string().

---

Member Function Documentation

const Theorem & Assumptions::findTheorem (  const Expr &  e  )  const [private]

Definition at line 43 of file assumptions.cpp. References CVCL::compare(), d_val, CVCL::AssumptionsValue::d_vector, find(), findTheorem(), CVCL::Theorem::getAssumptions(), CVCL::Theorem::isNull(), and CVCL::Theorem::setFlag(). Referenced by findTheorem(), and operator[]().

static bool CVCL::Assumptions::findExpr (  const Assumptions &  a, const Expr &  e, std::vector< Theorem > &  gamma )  [static, private]

Referenced by CVCL::operator-().

static bool CVCL::Assumptions::findExprs (  const Assumptions &  a, const std::vector< Expr > &  es, std::vector< Theorem > &  gamma )  [static, private]

Referenced by CVCL::operator-().

Assumptions & Assumptions::operator= (  const Assumptions &  assump  )

Definition at line 175 of file assumptions.cpp. References CVCL::AssumptionsValue::d_refcount, d_val, and CVCL::int2string().

bool CVCL::Assumptions::isNull (   )  const [inline]

Definition at line 91 of file assumptions.h. References d_val. Referenced by checkAssumpDebug(), copy(), CVCL::Theorem::getAssumptions(), init(), CVCL::operator-(), CVCL::operator<<(), operator[](), setConst(), size(), CVCL::TheoremValue::TheoremValue(), and toString().

void Assumptions::init (   )

Definition at line 195 of file assumptions.cpp. References CVCL::AssumptionsValue::d_refcount, d_val, and isNull(). Referenced by add(), and CVCL::Theorem::getAssumptions().

Assumptions Assumptions::copy (   )  const

Definition at line 203 of file assumptions.cpp. References Assumptions(), d_val, and isNull(). Referenced by CVCL::CommonTheoremProducer::andElim(), CVCL::Theorem::getAssumptionsCopy(), CVCL::CommonTheoremProducer::iffContrapositive(), CVCL::CommonTheoremProducer::iffFalseElim(), CVCL::CommonTheoremProducer::iffNotFalse(), CVCL::CommonTheoremProducer::iffTrue(), CVCL::CommonTheoremProducer::iffTrueElim(), CVCL::merge(), CVCL::CommonTheoremProducer::notToIff(), CVCL::operator-(), CVCL::UFTheoremProducer::relToClosure(), and CVCL::ArrayTheoremProducer::rewriteRedundantWrite1().

void Assumptions::add (  const Theorem &  t  )

Definition at line 211 of file assumptions.cpp. References CVCL::AssumptionsValue::add(), d_val, and init(). Referenced by add(), CVCL::SearchEngineTheoremProducer::caseSplit(), CVCL::SearchEngineTheoremProducer::confAndrAF(), CVCL::SearchEngineTheoremProducer::confAndrAT(), CVCL::SearchEngineTheoremProducer::confIffr(), CVCL::SearchEngineTheoremProducer::confIterIfThen(), CVCL::SearchEngineTheoremProducer::confIterThenElse(), CVCL::SearchEngineTheoremProducer::conflictRule(), CVCL::Theorem::getAssumptions(), CVCL::merge(), CVCL::SearchEngineTheoremProducer::propAndrAF(), CVCL::SearchEngineTheoremProducer::propAndrAT(), CVCL::SearchEngineTheoremProducer::propAndrLF(), CVCL::SearchEngineTheoremProducer::propAndrLRT(), CVCL::SearchEngineTheoremProducer::propAndrRF(), CVCL::SearchEngineTheoremProducer::propIffr(), CVCL::SearchEngineTheoremProducer::propIterIfThen(), CVCL::SearchEngineTheoremProducer::propIterIte(), CVCL::SearchEngineTheoremProducer::propIterThen(), and CVCL::SearchEngineTheoremProducer::unitProp().

void Assumptions::add (  const Assumptions &  a  )

Definition at line 217 of file assumptions.cpp. References CVCL::AssumptionsValue::add(), d_val, and init().

void Assumptions::clear (   )

Definition at line 223 of file assumptions.cpp. References CVCL::AssumptionsValue::d_const, d_val, and CVCL::AssumptionsValue::d_vector.

int Assumptions::size (   )  const

Definition at line 229 of file assumptions.cpp. References d_val, CVCL::AssumptionsValue::d_vector, and isNull().

bool Assumptions::empty (   )  const

Definition at line 237 of file assumptions.cpp. References d_val, and CVCL::AssumptionsValue::d_vector. Referenced by CVCL::AssumptionsValue::add(), CVCL::AssumptionsValue::AssumptionsValue(), CVCL::VCL::deriveClosure(), CVCL::Theorem::getAssumptions(), and CVCL::TheoremValue::TheoremValue().

bool Assumptions::isConst (   )  const

Definition at line 243 of file assumptions.cpp. References CVCL::AssumptionsValue::d_const, and d_val.

void Assumptions::setConst (   )

Definition at line 249 of file assumptions.cpp. References CVCL::AssumptionsValue::d_const, CVCL::AssumptionsValue::d_refcount, d_val, and isNull(). Referenced by CVCL::Theorem::getAssumptions(), and CVCL::TheoremValue::TheoremValue().

string Assumptions::toString (   )  const

Definition at line 259 of file assumptions.cpp. References d_val, isNull(), and CVCL::AssumptionsValue::toString(). Referenced by print(), and CVCL::TheoremValue::toString().

void Assumptions::print (   )  const

Definition at line 265 of file assumptions.cpp. References std::endl(), and toString().

const Theorem & Assumptions::operator[] (  const Expr &  e  )  const

Definition at line 271 of file assumptions.cpp. References d_val, CVCL::AssumptionsValue::d_vector, findTheorem(), and isNull().

const Theorem & Assumptions::find (  const Expr &  e  )  const

Definition at line 279 of file assumptions.cpp. References d_val, and CVCL::AssumptionsValue::find(). Referenced by findTheorem().

Assumptions::iterator Assumptions::begin (   )  const

Definition at line 299 of file assumptions.cpp. References d_val, and CVCL::AssumptionsValue::d_vector. Referenced by CVCL::SearchEngineFast::analyzeUIPs(), checkAssump(), CVCL::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVCL::VCL::deriveClosure(), CVCL::TheoryQuant::findInstAssumptions(), CVCL::operator-(), CVCL::TheoremValue::TheoremValue(), CVCL::SearchEngineFast::traceConflict(), and CVCL::SearchEngineTheoremProducer::verifyConflict().

Assumptions::iterator Assumptions::end (   )  const

Definition at line 306 of file assumptions.cpp. References d_val, and CVCL::AssumptionsValue::d_vector. Referenced by CVCL::SearchEngineFast::analyzeUIPs(), checkAssump(), CVCL::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVCL::VCL::deriveClosure(), CVCL::TheoryQuant::findInstAssumptions(), CVCL::operator-(), CVCL::Theorem::recursivePrint(), CVCL::TheoremValue::TheoremValue(), CVCL::SearchEngineFast::traceConflict(), and CVCL::SearchEngineTheoremProducer::verifyConflict().

void CVCL::Assumptions::add (  const iterator &  it  )  [inline]

Definition at line 163 of file assumptions.h. References add().

---

Friends And Related Function Documentation

Assumptions operator- (  const Assumptions &  a, const Expr &  e )  [friend]

Returns all (recursive) assumptions except e. Definition at line 321 of file assumptions.cpp.

Assumptions operator- (  const Assumptions &  a, const std::vector< Expr > &  es )  [friend]

Returns all (recursive) assumptions except those in es.

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

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

Definition at line 350 of file assumptions.cpp.

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

Definition at line 357 of file assumptions.cpp.

---

Member Data Documentation

AssumptionsValue* CVCL::Assumptions::d_val [private]

Definition at line 58 of file assumptions.h. Referenced by add(), Assumptions(), begin(), clear(), copy(), empty(), end(), find(), findTheorem(), init(), isConst(), isNull(), CVCL::operator!=(), CVCL::operator<<(), operator=(), CVCL::operator==(), operator[](), setConst(), size(), toString(), and ~Assumptions().

---

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

• assumptions.h
• assumptions.cpp

---