CVC3::Assumptions Class Reference

#include <assumptions.h>

Collaboration diagram for CVC3::Assumptions:

Collaboration graph
[legend]
List of all members.

Public Member Functions

Static Public Member Functions

Private Member Functions

Static Private Member Functions

Private Attributes

Static Private Attributes

Friends

Classes


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.

Referenced by CVC3::operator-().

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::clashingBounds(), CVC3::ArithTheoremProducer3::clashingBounds(), CVC3::ArithTheoremProducer::clashingBounds(), CVC3::SearchEngineTheoremProducer::confIterIfThen(), CVC3::SearchEngineTheoremProducer::cutRule(), CVC3::ArithTheoremProducerOld::cycleConflict(), CVC3::CommonTheoremProducer::implIntro3(), CVC3::ArithTheoremProducerOld::implyDiffLogicBothBounds(), CVC3::ArithTheoremProducerOld::implyEqualities(), CVC3::ArithTheoremProducerOld::implyWeakerInequalityDiffLogic(), 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(), and print().

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::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::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:
Generated on Wed Nov 18 16:14:22 2009 for CVC3 by  doxygen 1.5.2