CVC3  2.4.1
Classes | Public Member Functions | Static Public Member Functions | Private Member Functions | Static Private Member Functions | Private Attributes | Static Private Attributes | Friends
CVC3::Assumptions Class Reference

#include <assumptions.h>

List of all members.

Classes

Public Member Functions

Static Public Member Functions

Private Member Functions

Static Private Member Functions

Private Attributes

Static Private Attributes

Friends


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 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::Theorem::getAssumptionsRef(), empty(), and CVC3::compare().

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]
bool Assumptions::findExpr ( const Assumptions a,
const Expr e,
std::vector< Theorem > &  gamma 
) [static, private]

Definition at line 58 of file assumptions.cpp.

References end(), and begin().

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 end(), and begin().

void Assumptions::add ( const std::vector< Theorem > &  thms) [private]
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::ArrayTheoremProducer::rewriteSameStore(), CVC3::ArrayTheoremProducer::rewriteWriteWrite(), CVC3::ArrayTheoremProducer::rewriteReadWrite(), CVC3::ArrayTheoremProducer::rewriteReadWrite2(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite2(), CVC3::ArrayTheoremProducer::interchangeIndices(), CVC3::ArrayTheoremProducer::readArrayLiteral(), CVC3::ArrayTheoremProducer::liftReadIte(), CVC3::ArrayTheoremProducer::splitOnConstants(), CVC3::BitvectorTheoremProducer::bitBlastEqnRule(), CVC3::BitvectorTheoremProducer::padBVLTRule(), CVC3::BitvectorTheoremProducer::signExtendRule(), CVC3::BitvectorTheoremProducer::bitExtractSXRule(), CVC3::BitvectorTheoremProducer::padBVSLTRule(), CVC3::BitvectorTheoremProducer::signBVLTRule(), CVC3::BitvectorTheoremProducer::notBVEQ1Rule(), CVC3::BitvectorTheoremProducer::notBVLTRule(), CVC3::BitvectorTheoremProducer::lhsEqRhsIneqn(), CVC3::BitvectorTheoremProducer::zeroLeq(), CVC3::BitvectorTheoremProducer::bvConstIneqn(), CVC3::BitvectorTheoremProducer::generalIneqn(), CVC3::BitvectorTheoremProducer::bitExtractRewrite(), CVC3::BitvectorTheoremProducer::bitExtractConstant(), CVC3::BitvectorTheoremProducer::bitExtractConcatenation(), CVC3::BitvectorTheoremProducer::bitExtractConstBVMult(), CVC3::BitvectorTheoremProducer::bitExtractBVMult(), CVC3::BitvectorTheoremProducer::bitExtractExtraction(), CVC3::BitvectorTheoremProducer::bitExtractBVPlus(), CVC3::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVC3::BitvectorTheoremProducer::zeroPaddingRule(), CVC3::BitvectorTheoremProducer::bvPlusAssociativityRule(), CVC3::BitvectorTheoremProducer::bitExtractNot(), CVC3::BitvectorTheoremProducer::bitExtractBitwise(), CVC3::BitvectorTheoremProducer::bitExtractFixedLeftShift(), CVC3::BitvectorTheoremProducer::bitExtractFixedRightShift(), CVC3::BitvectorTheoremProducer::bitExtractBVSHL(), CVC3::BitvectorTheoremProducer::bitExtractBVLSHR(), CVC3::BitvectorTheoremProducer::bitExtractBVASHR(), CVC3::BitvectorTheoremProducer::eqConst(), CVC3::BitvectorTheoremProducer::leftShiftToConcat(), CVC3::BitvectorTheoremProducer::constWidthLeftShiftToConcat(), CVC3::BitvectorTheoremProducer::rightShiftToConcat(), CVC3::BitvectorTheoremProducer::bvshlToConcat(), CVC3::BitvectorTheoremProducer::bvshlSplit(), CVC3::BitvectorTheoremProducer::bvlshrToConcat(), CVC3::BitvectorTheoremProducer::bvShiftZero(), CVC3::BitvectorTheoremProducer::bvashrToConcat(), CVC3::BitvectorTheoremProducer::rewriteXNOR(), CVC3::BitvectorTheoremProducer::rewriteNAND(), CVC3::BitvectorTheoremProducer::rewriteNOR(), CVC3::BitvectorTheoremProducer::rewriteBVCOMP(), CVC3::BitvectorTheoremProducer::rewriteBVSub(), CVC3::BitvectorTheoremProducer::constMultToPlus(), CVC3::BitvectorTheoremProducer::bvplusZeroConcatRule(), CVC3::BitvectorTheoremProducer::extractConst(), CVC3::BitvectorTheoremProducer::extractWhole(), CVC3::BitvectorTheoremProducer::extractExtract(), CVC3::BitvectorTheoremProducer::extractConcat(), CVC3::BitvectorTheoremProducer::extractBitwise(), CVC3::BitvectorTheoremProducer::iteExtractRule(), CVC3::BitvectorTheoremProducer::iteBVnegRule(), CVC3::BitvectorTheoremProducer::negConst(), CVC3::BitvectorTheoremProducer::negConcat(), CVC3::BitvectorTheoremProducer::negNeg(), CVC3::BitvectorTheoremProducer::negElim(), CVC3::BitvectorTheoremProducer::negBVand(), CVC3::BitvectorTheoremProducer::negBVor(), CVC3::BitvectorTheoremProducer::negBVxor(), CVC3::BitvectorTheoremProducer::negBVxnor(), CVC3::BitvectorTheoremProducer::bitwiseConst(), CVC3::BitvectorTheoremProducer::bitwiseConcat(), CVC3::BitvectorTheoremProducer::bitwiseFlatten(), CVC3::BitvectorTheoremProducer::bitwiseConstElim(), CVC3::BitvectorTheoremProducer::concatConst(), CVC3::BitvectorTheoremProducer::concatFlatten(), CVC3::BitvectorTheoremProducer::concatMergeExtract(), CVC3::BitvectorTheoremProducer::bvplusConst(), CVC3::BitvectorTheoremProducer::bvmultConst(), CVC3::BitvectorTheoremProducer::zeroCoeffBVMult(), CVC3::BitvectorTheoremProducer::oneCoeffBVMult(), CVC3::BitvectorTheoremProducer::flipBVMult(), CVC3::BitvectorTheoremProducer::padBVPlus(), CVC3::BitvectorTheoremProducer::padBVMult(), CVC3::BitvectorTheoremProducer::bvConstMultAssocRule(), CVC3::BitvectorTheoremProducer::bvMultAssocRule(), CVC3::BitvectorTheoremProducer::bvMultDistRule(), CVC3::BitvectorTheoremProducer::flattenBVPlus(), CVC3::BitvectorTheoremProducer::combineLikeTermsRule(), CVC3::BitvectorTheoremProducer::lhsMinusRhsRule(), CVC3::BitvectorTheoremProducer::bvuminusToBVPlus(), CVC3::BitvectorTheoremProducer::bvuminusBVConst(), CVC3::BitvectorTheoremProducer::bvuminusBVMult(), CVC3::BitvectorTheoremProducer::bvuminusBVUminus(), CVC3::BitvectorTheoremProducer::bvuminusVar(), CVC3::BitvectorTheoremProducer::bvmultBVUminus(), CVC3::BitvectorTheoremProducer::bvuminusBVPlus(), CVC3::BitvectorTheoremProducer::extractBVMult(), CVC3::BitvectorTheoremProducer::extractBVPlus(), CVC3::BitvectorTheoremProducer::typePredBit(), CVC3::BitvectorTheoremProducer::MarkNonSolvableEq(), CVC3::BitvectorTheoremProducer::isolate_var(), CVC3::BitvectorTheoremProducer::BVMult_order_subterms(), CVC3::BitvectorTheoremProducer::liftConcatBVMult(), CVC3::BitvectorTheoremProducer::canonBVMult(), CVC3::BitvectorTheoremProducer::distributive_rule(), CVC3::BitvectorTheoremProducer::liftConcatBVPlus(), CVC3::BitvectorTheoremProducer::canonBVPlus(), CVC3::BitvectorTheoremProducer::canonBVUMinus(), CVC3::BitvectorTheoremProducer::canonBVEQ(), CVC3::BitvectorTheoremProducer::zeroExtendRule(), CVC3::BitvectorTheoremProducer::repeatRule(), CVC3::BitvectorTheoremProducer::rotlRule(), CVC3::BitvectorTheoremProducer::rotrRule(), CVC3::BitvectorTheoremProducer::bvURemConst(), CVC3::BitvectorTheoremProducer::bvURemRewrite(), CVC3::BitvectorTheoremProducer::bvUDivConst(), CVC3::BitvectorTheoremProducer::bvUDivTheorem(), CVC3::BitvectorTheoremProducer::bitblastBVMult(), CVC3::BitvectorTheoremProducer::bitblastBVPlus(), CVC3::BitvectorTheoremProducer::bvSDivRewrite(), CVC3::BitvectorTheoremProducer::bvSRemRewrite(), CVC3::BitvectorTheoremProducer::bvSModRewrite(), CVC3::BitvectorTheoremProducer::zeroBVOR(), CVC3::BitvectorTheoremProducer::oneBVAND(), CVC3::BitvectorTheoremProducer::constEq(), CVC3::BitvectorTheoremProducer::solveExtractOverlap(), CVC3::CommonTheoremProducer::rewriteReflexivity(), CVC3::CommonTheoremProducer::rewriteUsingSymmetry(), CVC3::CommonTheoremProducer::excludedMiddle(), CVC3::CommonTheoremProducer::rewriteIteTrue(), CVC3::CommonTheoremProducer::rewriteIteFalse(), CVC3::CommonTheoremProducer::rewriteIteSame(), CVC3::CommonTheoremProducer::xorToIff(), CVC3::CommonTheoremProducer::rewriteIff(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::CommonTheoremProducer::rewriteOr(), CVC3::CommonTheoremProducer::rewriteNotTrue(), CVC3::CommonTheoremProducer::rewriteNotFalse(), CVC3::CommonTheoremProducer::rewriteNotNot(), CVC3::CommonTheoremProducer::rewriteNotForall(), CVC3::CommonTheoremProducer::rewriteNotExists(), CVC3::CommonTheoremProducer::skolemizeRewrite(), CVC3::CommonTheoremProducer::skolemizeRewriteVar(), CVC3::CommonTheoremProducer::varIntroRule(), CVC3::CommonTheoremProducer::ackermann(), CVC3::CommonTheoremProducer::liftOneITE(), CVC3::CoreTheoremProducer::typePred(), CVC3::CoreTheoremProducer::rewriteLetDecl(), CVC3::CoreTheoremProducer::rewriteNotAnd(), CVC3::CoreTheoremProducer::rewriteNotOr(), CVC3::CoreTheoremProducer::rewriteNotIff(), CVC3::CoreTheoremProducer::rewriteNotIte(), CVC3::CoreTheoremProducer::rewriteIteBool(), CVC3::CoreTheoremProducer::orDistributivityRule(), CVC3::CoreTheoremProducer::andDistributivityRule(), CVC3::CoreTheoremProducer::rewriteImplies(), CVC3::CoreTheoremProducer::rewriteDistinct(), CVC3::CoreTheoremProducer::NotToIte(), CVC3::CoreTheoremProducer::OrToIte(), CVC3::CoreTheoremProducer::AndToIte(), CVC3::CoreTheoremProducer::IffToIte(), CVC3::CoreTheoremProducer::ImpToIte(), CVC3::CoreTheoremProducer::rewriteIteToNot(), CVC3::CoreTheoremProducer::rewriteIteToOr(), CVC3::CoreTheoremProducer::rewriteIteToAnd(), CVC3::CoreTheoremProducer::rewriteIteToIff(), CVC3::CoreTheoremProducer::rewriteIteToImp(), CVC3::CoreTheoremProducer::rewriteIteCond(), CVC3::CoreTheoremProducer::iffOrDistrib(), CVC3::CoreTheoremProducer::iffAndDistrib(), CVC3::CoreTheoremProducer::ifLiftUnaryRule(), CVC3::CoreTheoremProducer::rewriteAndSubterms(), CVC3::CoreTheoremProducer::rewriteOrSubterms(), CVC3::CoreTheoremProducer::dummyTheorem(), CVC3::SearchImplBase::getAssumptionsUsed(), CVC3::SearchEngineTheoremProducer::satProof(), CVC3::Theorem::getAssumptionsRef(), CVC3::TheoremProducer::newAssumption(), and CVC3::RWTheoremValue::getAssumptionsRef().

void CVC3::Assumptions::add1 ( const Theorem t) [inline]

Definition at line 85 of file assumptions.h.

References DebugAssert, and d_vector.

void Assumptions::add ( const Theorem t)

Definition at line 190 of file assumptions.cpp.

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

void CVC3::Assumptions::add ( const Assumptions a) [inline]

Definition at line 90 of file assumptions.h.

References add().

Referenced by add().

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 getFirst(), and CVC3::Theorem::getAssumptionsAndCongRec().

bool CVC3::Assumptions::empty ( ) const [inline]
Theorem& CVC3::Assumptions::getFirst ( ) [inline]

Definition at line 98 of file assumptions.h.

References DebugAssert, size(), and d_vector.

string Assumptions::toString ( ) const
void Assumptions::print ( ) const

Definition at line 257 of file assumptions.cpp.

References std::endl().

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

Definition at line 263 of file assumptions.cpp.

References CVC3::Theorem::clearAllFlags().

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

Definition at line 271 of file assumptions.cpp.

References CVC3::compare().

iterator CVC3::Assumptions::begin ( ) const [inline]
iterator CVC3::Assumptions::end ( ) const [inline]

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

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: