CVC3::Assumptions Class Reference

#include <assumptions.h>

Collaboration diagram for CVC3::Assumptions:

[legend]

List of all members.

Classes

• class iterator

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

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)
• void add1 (const Theorem &t)
• void add (const Theorem &t)
• void add (const Assumptions &a)
• void clear ()
• unsigned size () const
• bool empty () const
• Theorem & getFirst ()
• 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

Static Public Member Functions

• static const Assumptions & emptyAssump ()

Private Member Functions

• const Theorem & findTheorem (const Expr &e) const
• void add (const std::vector< Theorem > &thms)

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

• std::vector< Theorem > d_vector

Static Private Attributes

• static Assumptions s_empty

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)

---

Detailed Description

Definition at line 46 of file assumptions.h.

---

Constructor & Destructor Documentation

CVC3::Assumptions::Assumptions

(

)

[inline]

Default constructor: no value is created.

Definition at line 67 of file assumptions.h.

Assumptions::Assumptions

(

const std::vector< Theorem > &

v

)

Constructor from a vector of theorems.

Definition at line 127 of file assumptions.cpp.

References d_vector, and CVC3::Theorem::TheoremEq().

CVC3::Assumptions::Assumptions

(

const Theorem &

t

)

[inline]

Constructor for one theorem (common case).

Definition at line 71 of file assumptions.h.

References d_vector.

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

Constructor for two theorems (common case).

Definition at line 149 of file assumptions.cpp.

References CVC3::compare(), d_vector, empty(), and CVC3::Theorem::getAssumptionsRef().

CVC3::Assumptions::~Assumptions

(

)

[inline]

Definition at line 76 of file assumptions.h.

CVC3::Assumptions::Assumptions

(

const Assumptions &

assump

)

[inline]

Definition at line 78 of file assumptions.h.

---

Member Function Documentation

const Theorem & Assumptions::findTheorem

(

const Expr &

e

)

const [private]

Definition at line 34 of file assumptions.cpp.

References CVC3::compare(), d_vector, find(), findTheorem(), CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::isNull(), and CVC3::Theorem::setFlag().

Referenced by findTheorem(), and operator[]().

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

Definition at line 58 of file assumptions.cpp.

References begin(), and end().

Referenced by CVC3::operator-().

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

Definition at line 92 of file assumptions.cpp.

References begin(), end(), and find().

Referenced by CVC3::operator-().

void Assumptions::add

(

const std::vector< Theorem > &

thms

)

[private]

Definition at line 200 of file assumptions.cpp.

References CVC3::compare(), d_vector, DebugAssert, and IF_DEBUG.

Referenced by CVC3::ArithTheoremProducerOld::addInequalities(), CVC3::ArithTheoremProducerOld::clashingBounds(), CVC3::ArithTheoremProducer3::clashingBounds(), CVC3::ArithTheoremProducer::clashingBounds(), CVC3::SearchEngineTheoremProducer::confAndrAF(), CVC3::SearchEngineTheoremProducer::confAndrAT(), CVC3::SearchEngineTheoremProducer::confIffr(), CVC3::SearchEngineTheoremProducer::confIterIfThen(), CVC3::SearchEngineTheoremProducer::confIterThenElse(), CVC3::SearchEngineTheoremProducer::conflictRule(), CVC3::SearchEngineTheoremProducer::cutRule(), CVC3::ArithTheoremProducerOld::cycleConflict(), CVC3::CommonTheoremProducer::implIntro3(), CVC3::ArithTheoremProducerOld::implyDiffLogicBothBounds(), CVC3::ArithTheoremProducerOld::implyEqualities(), CVC3::ArithTheoremProducerOld::implyNegatedInequalityDiffLogic(), CVC3::ArithTheoremProducerOld::implyWeakerInequalityDiffLogic(), CVC3::ArithTheoremProducerOld::nonLinearIneqSignSplit(), CVC3::SearchEngineTheoremProducer::propAndrAT(), CVC3::SearchEngineTheoremProducer::propAndrLF(), CVC3::SearchEngineTheoremProducer::propAndrRF(), CVC3::SearchEngineTheoremProducer::propIffr(), CVC3::SearchEngineTheoremProducer::propIterIfThen(), CVC3::SearchEngineTheoremProducer::propIterIte(), CVC3::SearchEngineTheoremProducer::propIterThen(), CVC3::CommonTheoremProducer::queryTCC(), and CVC3::SearchEngineTheoremProducer::unitProp().

Assumptions& CVC3::Assumptions::operator=

(

const Assumptions &

assump

)

[inline]

Definition at line 80 of file assumptions.h.

References d_vector.

static const Assumptions& CVC3::Assumptions::emptyAssump

(

)

[inline, static]

Definition at line 83 of file assumptions.h.

References s_empty.

Referenced by CVC3::CommonTheoremProducer::ackermann(), CVC3::QuantTheoremProducer::addNewConst(), CVC3::CoreTheoremProducer::andDistributivityRule(), CVC3::CoreTheoremProducer::AndToIte(), CVC3::UFTheoremProducer::applyLambda(), CVC3::BitvectorTheoremProducer::bitblastBVMult(), CVC3::BitvectorTheoremProducer::bitblastBVPlus(), CVC3::BitvectorTheoremProducer::bitBlastEqnRule(), CVC3::BitvectorTheoremProducer::bitExtractBitwise(), CVC3::BitvectorTheoremProducer::bitExtractBVASHR(), CVC3::BitvectorTheoremProducer::bitExtractBVLSHR(), CVC3::BitvectorTheoremProducer::bitExtractBVMult(), CVC3::BitvectorTheoremProducer::bitExtractBVPlus(), CVC3::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVC3::BitvectorTheoremProducer::bitExtractBVSHL(), CVC3::BitvectorTheoremProducer::bitExtractConcatenation(), CVC3::BitvectorTheoremProducer::bitExtractConstant(), CVC3::BitvectorTheoremProducer::bitExtractConstBVMult(), CVC3::BitvectorTheoremProducer::bitExtractExtraction(), CVC3::BitvectorTheoremProducer::bitExtractFixedLeftShift(), CVC3::BitvectorTheoremProducer::bitExtractFixedRightShift(), CVC3::BitvectorTheoremProducer::bitExtractNot(), CVC3::BitvectorTheoremProducer::bitExtractRewrite(), CVC3::BitvectorTheoremProducer::bitExtractSXRule(), CVC3::BitvectorTheoremProducer::bitwiseConcat(), CVC3::BitvectorTheoremProducer::bitwiseConst(), CVC3::BitvectorTheoremProducer::bitwiseConstElim(), CVC3::BitvectorTheoremProducer::bitwiseFlatten(), CVC3::BitvectorTheoremProducer::bvashrToConcat(), CVC3::BitvectorTheoremProducer::bvConstIneqn(), CVC3::BitvectorTheoremProducer::bvConstMultAssocRule(), CVC3::BitvectorTheoremProducer::bvlshrToConcat(), CVC3::BitvectorTheoremProducer::BVMult_order_subterms(), CVC3::BitvectorTheoremProducer::bvMultAssocRule(), CVC3::BitvectorTheoremProducer::bvmultBVUminus(), CVC3::BitvectorTheoremProducer::bvmultConst(), CVC3::BitvectorTheoremProducer::bvMultDistRule(), CVC3::BitvectorTheoremProducer::bvPlusAssociativityRule(), CVC3::BitvectorTheoremProducer::bvplusConst(), CVC3::BitvectorTheoremProducer::bvplusZeroConcatRule(), CVC3::BitvectorTheoremProducer::bvSDivRewrite(), CVC3::BitvectorTheoremProducer::bvShiftZero(), CVC3::BitvectorTheoremProducer::bvshlSplit(), CVC3::BitvectorTheoremProducer::bvshlToConcat(), CVC3::BitvectorTheoremProducer::bvSModRewrite(), CVC3::BitvectorTheoremProducer::bvSRemRewrite(), CVC3::BitvectorTheoremProducer::bvUDivConst(), CVC3::BitvectorTheoremProducer::bvUDivTheorem(), CVC3::BitvectorTheoremProducer::bvuminusBVConst(), CVC3::BitvectorTheoremProducer::bvuminusBVMult(), CVC3::BitvectorTheoremProducer::bvuminusBVPlus(), CVC3::BitvectorTheoremProducer::bvuminusBVUminus(), CVC3::BitvectorTheoremProducer::bvuminusToBVPlus(), CVC3::BitvectorTheoremProducer::bvuminusVar(), CVC3::BitvectorTheoremProducer::bvURemConst(), CVC3::BitvectorTheoremProducer::bvURemRewrite(), CVC3::BitvectorTheoremProducer::canonBVEQ(), CVC3::BitvectorTheoremProducer::canonBVMult(), CVC3::BitvectorTheoremProducer::canonBVPlus(), CVC3::BitvectorTheoremProducer::canonBVUMinus(), CVC3::ArithTheoremProducerOld::canonComboLikeTerms(), CVC3::ArithTheoremProducer3::canonComboLikeTerms(), CVC3::ArithTheoremProducer::canonComboLikeTerms(), CVC3::ArithTheoremProducerOld::canonDivide(), CVC3::ArithTheoremProducer3::canonDivide(), CVC3::ArithTheoremProducer::canonDivide(), CVC3::ArithTheoremProducerOld::canonDivideConst(), CVC3::ArithTheoremProducer3::canonDivideConst(), CVC3::ArithTheoremProducer::canonDivideConst(), CVC3::ArithTheoremProducerOld::canonDivideMult(), CVC3::ArithTheoremProducer3::canonDivideMult(), CVC3::ArithTheoremProducer::canonDivideMult(), CVC3::ArithTheoremProducerOld::canonDividePlus(), CVC3::ArithTheoremProducer3::canonDividePlus(), CVC3::ArithTheoremProducer::canonDividePlus(), CVC3::ArithTheoremProducerOld::canonDivideVar(), CVC3::ArithTheoremProducer3::canonDivideVar(), CVC3::ArithTheoremProducer::canonDivideVar(), CVC3::ArithTheoremProducerOld::canonFlattenSum(), CVC3::ArithTheoremProducer3::canonFlattenSum(), CVC3::ArithTheoremProducer::canonFlattenSum(), CVC3::ArithTheoremProducerOld::canonInvertConst(), CVC3::ArithTheoremProducer3::canonInvertConst(), CVC3::ArithTheoremProducer::canonInvertConst(), CVC3::ArithTheoremProducerOld::canonInvertLeaf(), CVC3::ArithTheoremProducer3::canonInvertLeaf(), CVC3::ArithTheoremProducer::canonInvertLeaf(), CVC3::ArithTheoremProducerOld::canonInvertMult(), CVC3::ArithTheoremProducer3::canonInvertMult(), CVC3::ArithTheoremProducer::canonInvertMult(), CVC3::ArithTheoremProducerOld::canonInvertPow(), CVC3::ArithTheoremProducer3::canonInvertPow(), CVC3::ArithTheoremProducer::canonInvertPow(), CVC3::ArithTheoremProducerOld::canonMult(), CVC3::ArithTheoremProducer3::canonMult(), CVC3::ArithTheoremProducer::canonMult(), CVC3::ArithTheoremProducerOld::canonMultConstConst(), CVC3::ArithTheoremProducer3::canonMultConstConst(), CVC3::ArithTheoremProducer::canonMultConstConst(), CVC3::ArithTheoremProducerOld::canonMultConstSum(), CVC3::ArithTheoremProducer3::canonMultConstSum(), CVC3::ArithTheoremProducer::canonMultConstSum(), CVC3::ArithTheoremProducerOld::canonMultConstTerm(), CVC3::ArithTheoremProducer3::canonMultConstTerm(), CVC3::ArithTheoremProducer::canonMultConstTerm(), CVC3::ArithTheoremProducerOld::canonMultMtermMterm(), CVC3::ArithTheoremProducer3::canonMultMtermMterm(), CVC3::ArithTheoremProducer::canonMultMtermMterm(), CVC3::ArithTheoremProducerOld::canonMultOne(), CVC3::ArithTheoremProducer3::canonMultOne(), CVC3::ArithTheoremProducer::canonMultOne(), CVC3::ArithTheoremProducerOld::canonMultTermConst(), CVC3::ArithTheoremProducer3::canonMultTermConst(), CVC3::ArithTheoremProducer::canonMultTermConst(), CVC3::ArithTheoremProducerOld::canonMultZero(), CVC3::ArithTheoremProducer3::canonMultZero(), CVC3::ArithTheoremProducer::canonMultZero(), CVC3::ArithTheoremProducerOld::canonPlus(), CVC3::ArithTheoremProducer3::canonPlus(), CVC3::ArithTheoremProducer::canonPlus(), CVC3::ArithTheoremProducerOld::canonPowConst(), CVC3::ArithTheoremProducer3::canonPowConst(), CVC3::ArithTheoremProducer::canonPowConst(), CVC3::ArithTheoremProducerOld::canonUMinusToDivide(), CVC3::ArithTheoremProducer3::canonUMinusToDivide(), CVC3::ArithTheoremProducer::canonUMinusToDivide(), CVC3::CNF_TheoremProducer::CNFtranslate(), CVC3::BitvectorTheoremProducer::combineLikeTermsRule(), CVC3::ArithTheoremProducerOld::compactNonLinearTerm(), CVC3::BitvectorTheoremProducer::concatConst(), CVC3::BitvectorTheoremProducer::concatFlatten(), CVC3::BitvectorTheoremProducer::concatMergeExtract(), CVC3::BitvectorTheoremProducer::constEq(), CVC3::BitvectorTheoremProducer::constMultToPlus(), CVC3::ArithTheoremProducerOld::constPredicate(), CVC3::ArithTheoremProducer3::constPredicate(), CVC3::ArithTheoremProducer::constPredicate(), CVC3::BitvectorTheoremProducer::constWidthLeftShiftToConcat(), CVC3::BitvectorTheoremProducer::distributive_rule(), CVC3::ArithTheoremProducerOld::divideEqnNonConst(), CVC3::ArithTheoremProducer3::divideEqnNonConst(), CVC3::ArithTheoremProducer::divideEqnNonConst(), CVC3::CoreTheoremProducer::dummyTheorem(), CVC3::ArithTheoremProducerOld::dummyTheorem(), CVC3::ArithTheoremProducer3::dummyTheorem(), CVC3::ArithTheoremProducer::dummyTheorem(), CVC3::ArithTheoremProducerOld::elimPower(), CVC3::ArithTheoremProducer3::elimPower(), CVC3::ArithTheoremProducer::elimPower(), CVC3::ArithTheoremProducerOld::elimPowerConst(), CVC3::ArithTheoremProducer3::elimPowerConst(), CVC3::ArithTheoremProducer::elimPowerConst(), CVC3::BitvectorTheoremProducer::eqConst(), CVC3::ArithTheoremProducerOld::eqToIneq(), CVC3::ArithTheoremProducer3::eqToIneq(), CVC3::ArithTheoremProducer::eqToIneq(), CVC3::ArithTheoremProducerOld::evenPowerEqNegConst(), CVC3::ArithTheoremProducer3::evenPowerEqNegConst(), CVC3::ArithTheoremProducer::evenPowerEqNegConst(), CVC3::CommonTheoremProducer::excludedMiddle(), CVC3::ArithTheoremProducerOld::expandGrayShadowRewrite(), CVC3::RecordsTheoremProducer::expandRecord(), CVC3::SimulateTheoremProducer::expandSimulate(), CVC3::RecordsTheoremProducer::expandTuple(), CVC3::BitvectorTheoremProducer::extractBitwise(), CVC3::BitvectorTheoremProducer::extractBVMult(), CVC3::BitvectorTheoremProducer::extractBVPlus(), CVC3::BitvectorTheoremProducer::extractConcat(), CVC3::BitvectorTheoremProducer::extractConst(), CVC3::BitvectorTheoremProducer::extractExtract(), CVC3::BitvectorTheoremProducer::extractWhole(), CVC3::BitvectorTheoremProducer::flattenBVPlus(), CVC3::BitvectorTheoremProducer::flipBVMult(), CVC3::ArithTheoremProducerOld::flipInequality(), CVC3::ArithTheoremProducer3::flipInequality(), CVC3::ArithTheoremProducer::flipInequality(), CVC3::BitvectorTheoremProducer::generalIneqn(), CVC3::RWTheoremValue::getAssumptionsRef(), CVC3::Theorem::getAssumptionsRef(), CVC3::SearchImplBase::getAssumptionsUsed(), CVC3::CNF_TheoremProducer::getSmartClauses(), CVC3::CoreTheoremProducer::iffAndDistrib(), CVC3::CoreTheoremProducer::iffOrDistrib(), CVC3::CoreTheoremProducer::IffToIte(), CVC3::CNF_TheoremProducer::ifLiftRule(), CVC3::CoreTheoremProducer::ifLiftUnaryRule(), CVC3::ArithTheoremProducerOld::implyNegatedInequality(), CVC3::ArithTheoremProducer3::implyNegatedInequality(), CVC3::ArithTheoremProducer::implyNegatedInequality(), CVC3::ArithTheoremProducerOld::implyWeakerInequality(), CVC3::ArithTheoremProducer3::implyWeakerInequality(), CVC3::ArithTheoremProducer::implyWeakerInequality(), CVC3::CoreTheoremProducer::ImpToIte(), CVC3::ArithTheoremProducerOld::integerSplit(), CVC3::ArithTheoremProducer3::integerSplit(), CVC3::ArithTheoremProducer::integerSplit(), CVC3::ArrayTheoremProducer::interchangeIndices(), CVC3::ArithTheoremProducerOld::isIntConst(), CVC3::ArithTheoremProducer3::isIntConst(), CVC3::ArithTheoremProducer::isIntConst(), CVC3::BitvectorTheoremProducer::isolate_var(), CVC3::BitvectorTheoremProducer::iteBVnegRule(), CVC3::BitvectorTheoremProducer::iteExtractRule(), CVC3::CNF_TheoremProducer::learnedClauses(), CVC3::ArithTheoremProducerOld::leftMinusRight(), CVC3::ArithTheoremProducer3::leftMinusRight(), CVC3::ArithTheoremProducer::leftMinusRight(), CVC3::BitvectorTheoremProducer::leftShiftToConcat(), CVC3::BitvectorTheoremProducer::lhsEqRhsIneqn(), CVC3::BitvectorTheoremProducer::lhsMinusRhsRule(), CVC3::BitvectorTheoremProducer::liftConcatBVMult(), CVC3::BitvectorTheoremProducer::liftConcatBVPlus(), CVC3::CommonTheoremProducer::liftOneITE(), CVC3::ArrayTheoremProducer::liftReadIte(), CVC3::BitvectorTheoremProducer::MarkNonSolvableEq(), CVC3::ArithTheoremProducerOld::minusToPlus(), CVC3::ArithTheoremProducer3::minusToPlus(), CVC3::ArithTheoremProducer::minusToPlus(), CVC3::ArithTheoremProducerOld::moveSumConstantRight(), CVC3::ArithTheoremProducer3::moveSumConstantRight(), CVC3::ArithTheoremProducer::moveSumConstantRight(), CVC3::ArithTheoremProducerOld::multEqn(), CVC3::ArithTheoremProducer3::multEqn(), CVC3::ArithTheoremProducer::multEqn(), CVC3::ArithTheoremProducerOld::multEqZero(), CVC3::ArithTheoremProducer3::multEqZero(), CVC3::ArithTheoremProducer::multEqZero(), CVC3::ArithTheoremProducerOld::multIneqn(), CVC3::ArithTheoremProducer3::multIneqn(), CVC3::ArithTheoremProducer::multIneqn(), CVC3::ArithTheoremProducerOld::negatedInequality(), CVC3::ArithTheoremProducer3::negatedInequality(), CVC3::ArithTheoremProducer::negatedInequality(), CVC3::BitvectorTheoremProducer::negBVand(), CVC3::BitvectorTheoremProducer::negBVor(), CVC3::BitvectorTheoremProducer::negBVxnor(), CVC3::BitvectorTheoremProducer::negBVxor(), CVC3::BitvectorTheoremProducer::negConcat(), CVC3::BitvectorTheoremProducer::negConst(), CVC3::BitvectorTheoremProducer::negElim(), CVC3::BitvectorTheoremProducer::negNeg(), CVC3::TheoremProducer::newAssumption(), CVC3::QuantTheoremProducer::newRWThm(), CVC3::DatatypeTheoremProducer::noCycle(), CVC3::QuantTheoremProducer::normalizeQuant(), CVC3::BitvectorTheoremProducer::notBVEQ1Rule(), CVC3::BitvectorTheoremProducer::notBVLTRule(), CVC3::CoreTheoremProducer::NotToIte(), CVC3::BitvectorTheoremProducer::oneBVAND(), CVC3::BitvectorTheoremProducer::oneCoeffBVMult(), CVC3::ArithTheoremProducerOld::oneElimination(), CVC3::ArithTheoremProducer3::oneElimination(), CVC3::ArithTheoremProducer::oneElimination(), CVC3::CoreTheoremProducer::orDistributivityRule(), CVC3::CoreTheoremProducer::OrToIte(), CVC3::BitvectorTheoremProducer::padBVLTRule(), CVC3::BitvectorTheoremProducer::padBVMult(), CVC3::BitvectorTheoremProducer::padBVPlus(), CVC3::BitvectorTheoremProducer::padBVSLTRule(), CVC3::ArithTheoremProducerOld::plusPredicate(), CVC3::ArithTheoremProducer3::plusPredicate(), CVC3::ArithTheoremProducer::plusPredicate(), CVC3::ArithTheoremProducerOld::powEqZero(), CVC3::ArithTheoremProducer3::powEqZero(), CVC3::ArithTheoremProducer::powEqZero(), CVC3::ArithTheoremProducerOld::powerOfOne(), CVC3::ArrayTheoremProducer::readArrayLiteral(), CVC3::BitvectorTheoremProducer::repeatRule(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::CoreTheoremProducer::rewriteAndSubterms(), CVC3::BitvectorTheoremProducer::rewriteBVCOMP(), CVC3::BitvectorTheoremProducer::rewriteBVSub(), CVC3::CoreTheoremProducer::rewriteDistinct(), CVC3::CommonTheoremProducer::rewriteIff(), CVC3::CoreTheoremProducer::rewriteImplies(), CVC3::CoreTheoremProducer::rewriteIteBool(), CVC3::CoreTheoremProducer::rewriteIteCond(), CVC3::CommonTheoremProducer::rewriteIteFalse(), CVC3::CommonTheoremProducer::rewriteIteSame(), CVC3::CoreTheoremProducer::rewriteIteToAnd(), CVC3::CoreTheoremProducer::rewriteIteToIff(), CVC3::CoreTheoremProducer::rewriteIteToImp(), CVC3::CoreTheoremProducer::rewriteIteToNot(), CVC3::CoreTheoremProducer::rewriteIteToOr(), CVC3::CommonTheoremProducer::rewriteIteTrue(), CVC3::ArithTheoremProducerOld::rewriteLeavesConst(), CVC3::CoreTheoremProducer::rewriteLetDecl(), CVC3::RecordsTheoremProducer::rewriteLitSelect(), CVC3::RecordsTheoremProducer::rewriteLitUpdate(), CVC3::BitvectorTheoremProducer::rewriteNAND(), CVC3::BitvectorTheoremProducer::rewriteNOR(), CVC3::CoreTheoremProducer::rewriteNotAnd(), CVC3::QuantTheoremProducer::rewriteNotExists(), CVC3::CommonTheoremProducer::rewriteNotExists(), CVC3::CommonTheoremProducer::rewriteNotFalse(), CVC3::QuantTheoremProducer::rewriteNotForall(), CVC3::CommonTheoremProducer::rewriteNotForall(), CVC3::CoreTheoremProducer::rewriteNotIff(), CVC3::CoreTheoremProducer::rewriteNotIte(), CVC3::CommonTheoremProducer::rewriteNotNot(), CVC3::CoreTheoremProducer::rewriteNotOr(), CVC3::CommonTheoremProducer::rewriteNotTrue(), CVC3::UFTheoremProducer::rewriteOpDef(), CVC3::CommonTheoremProducer::rewriteOr(), CVC3::CoreTheoremProducer::rewriteOrSubterms(), CVC3::ArrayTheoremProducer::rewriteReadWrite(), CVC3::ArrayTheoremProducer::rewriteReadWrite2(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite2(), CVC3::CommonTheoremProducer::rewriteReflexivity(), CVC3::ArrayTheoremProducer::rewriteSameStore(), CVC3::DatatypeTheoremProducer::rewriteSelCons(), CVC3::DatatypeTheoremProducer::rewriteTestCons(), CVC3::RecordsTheoremProducer::rewriteUpdateSelect(), CVC3::CommonTheoremProducer::rewriteUsingSymmetry(), CVC3::ArrayTheoremProducer::rewriteWriteWrite(), CVC3::BitvectorTheoremProducer::rewriteXNOR(), CVC3::ArithTheoremProducerOld::rightMinusLeft(), CVC3::ArithTheoremProducer3::rightMinusLeft(), CVC3::ArithTheoremProducer::rightMinusLeft(), CVC3::BitvectorTheoremProducer::rightShiftToConcat(), CVC3::BitvectorTheoremProducer::rotlRule(), CVC3::BitvectorTheoremProducer::rotrRule(), CVC3::SearchEngineTheoremProducer::satProof(), CVC3::BitvectorTheoremProducer::signBVLTRule(), CVC3::BitvectorTheoremProducer::signExtendRule(), CVC3::ArithTheoremProducerOld::simpleIneqInt(), CVC3::CommonTheoremProducer::skolemizeRewrite(), CVC3::CommonTheoremProducer::skolemizeRewriteVar(), CVC3::BitvectorTheoremProducer::solveExtractOverlap(), CVC3::ArithTheoremProducerOld::trustedRewrite(), CVC3::ArithTheoremProducer3::trustedRewrite(), CVC3::ArithTheoremProducer::trustedRewrite(), CVC3::CoreTheoremProducer::typePred(), CVC3::BitvectorTheoremProducer::typePredBit(), CVC3::ArithTheoremProducerOld::uMinusToMult(), CVC3::ArithTheoremProducer3::uMinusToMult(), CVC3::ArithTheoremProducer::uMinusToMult(), CVC3::CommonTheoremProducer::varIntroRule(), CVC3::ArithTheoremProducerOld::varToMult(), CVC3::ArithTheoremProducer3::varToMult(), CVC3::ArithTheoremProducer::varToMult(), CVC3::CommonTheoremProducer::xorToIff(), CVC3::BitvectorTheoremProducer::zeroBVOR(), CVC3::BitvectorTheoremProducer::zeroCoeffBVMult(), CVC3::BitvectorTheoremProducer::zeroExtendRule(), CVC3::BitvectorTheoremProducer::zeroLeq(), and CVC3::BitvectorTheoremProducer::zeroPaddingRule().

void CVC3::Assumptions::add1

(

const Theorem &

t

)

[inline]

Definition at line 85 of file assumptions.h.

References d_vector, and DebugAssert.

void Assumptions::add

(

const Theorem &

t

)

Definition at line 190 of file assumptions.cpp.

References CVC3::compare(), d_vector, empty(), and CVC3::Theorem::getAssumptionsRef().

void CVC3::Assumptions::add

(

const Assumptions &

a

)

[inline]

Definition at line 90 of file assumptions.h.

void CVC3::Assumptions::clear

(

)

[inline]

Definition at line 92 of file assumptions.h.

References d_vector.

unsigned CVC3::Assumptions::size

(

)

const [inline]

Definition at line 94 of file assumptions.h.

References d_vector.

Referenced by CVC3::Theorem::getAssumptionsAndCongRec(), and getFirst().

bool CVC3::Assumptions::empty

(

)

const [inline]

Definition at line 95 of file assumptions.h.

References d_vector.

Referenced by add(), Assumptions(), CVC3::VCL::getAssumptions(), CVC3::RWTheoremValue::init(), and CVC3::RegTheoremValue::RegTheoremValue().

Theorem& CVC3::Assumptions::getFirst

(

)

[inline]

Definition at line 98 of file assumptions.h.

References d_vector, DebugAssert, and size().

string Assumptions::toString

(

)

const

Definition at line 250 of file assumptions.cpp.

Referenced by CVC3::TheoryQuant::notifyInconsistent(), print(), and CVC3::TheoremValue::toString().

void Assumptions::print

(

)

const

Definition at line 257 of file assumptions.cpp.

References std::endl(), and toString().

const Theorem & Assumptions::operator[]

(

const Expr &

e

)

const

Definition at line 263 of file assumptions.cpp.

References d_vector, and findTheorem().

const Theorem & Assumptions::find

(

const Expr &

e

)

const

Definition at line 271 of file assumptions.cpp.

References CVC3::compare(), and d_vector.

Referenced by findExprs(), and findTheorem().

iterator CVC3::Assumptions::begin

(

)

const [inline]

Definition at line 151 of file assumptions.h.

References d_vector.

Referenced by CVC3::SearchEngineFast::analyzeUIPs(), findExpr(), findExprs(), CVC3::TheoryQuant::findInstAssumptions(), CVC3::VCL::getAssumptions(), CVC3::Theorem::getAssumptionsAndCongRec(), CVC3::Theorem::getAssumptionsRec(), CVC3::Theorem::GetSatAssumptions(), CVC3::Theorem::GetSatAssumptionsRec(), CVC3::RWTheoremValue::init(), CVC3::operator-(), CVC3::Theorem::recursivePrint(), and CVC3::SearchEngineFast::traceConflict().

iterator CVC3::Assumptions::end

(

)

const [inline]

Definition at line 152 of file assumptions.h.

References d_vector.

Referenced by CVC3::SearchEngineFast::analyzeUIPs(), findExpr(), findExprs(), CVC3::TheoryQuant::findInstAssumptions(), CVC3::VCL::getAssumptions(), CVC3::Theorem::getAssumptionsAndCongRec(), CVC3::Theorem::getAssumptionsRec(), CVC3::Theorem::GetSatAssumptions(), CVC3::Theorem::GetSatAssumptionsRec(), CVC3::RWTheoremValue::init(), CVC3::operator-(), CVC3::Theorem::recursivePrint(), and CVC3::SearchEngineFast::traceConflict().

---

Friends And Related Function Documentation

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

Returns all (recursive) assumptions except e.

Definition at line 301 of file assumptions.cpp.

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

Returns all (recursive) assumptions except those in es.

Definition at line 311 of file assumptions.cpp.

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

Definition at line 321 of file assumptions.cpp.

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

Definition at line 166 of file assumptions.h.

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

Definition at line 168 of file assumptions.h.

---

Member Data Documentation

std::vector<Theorem> CVC3::Assumptions::d_vector [private]

Definition at line 48 of file assumptions.h.

Referenced by add(), add1(), Assumptions(), begin(), clear(), empty(), end(), find(), findTheorem(), getFirst(), CVC3::operator<<(), operator=(), operator[](), and size().

Assumptions Assumptions::s_empty [static, private]

Definition at line 49 of file assumptions.h.

Referenced by emptyAssump().

---

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

• assumptions.h
• assumptions.cpp