#include <assumptions.h>
Collaboration diagram for CVC3::Assumptions:
Definition at line 44 of file assumptions.h.
| CVC3::Assumptions::Assumptions | ( | ) | [inline] |
| 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 69 of file assumptions.h.
References d_vector.
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 74 of file assumptions.h.
| CVC3::Assumptions::Assumptions | ( | const Assumptions & | assump | ) | [inline] |
Definition at line 76 of file assumptions.h.
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 183 of file assumptions.cpp.
References CVC3::compare(), d_vector, DebugAssert, and IF_DEBUG.
Referenced by add(), CVC3::ArithTheoremProducerOld::clashingBounds(), CVC3::ArithTheoremProducer::clashingBounds(), CVC3::SearchEngineTheoremProducer::confIterIfThen(), CVC3::SearchEngineTheoremProducer::cutRule(), CVC3::CommonTheoremProducer::implIntro3(), 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] |
| static const Assumptions& CVC3::Assumptions::emptyAssump | ( | ) | [inline, static] |
Definition at line 81 of file assumptions.h.
References s_empty.
Referenced by CVC3::CommonTheoremProducer::ackermann(), CVC3::QuantTheoremProducer::addNewConst(), CVC3::CoreTheoremProducer::andDistributivityRule(), CVC3::BitvectorTheoremProducer::andOne(), CVC3::CoreTheoremProducer::AndToIte(), CVC3::BitvectorTheoremProducer::andZero(), CVC3::UFTheoremProducer::applyLambda(), CVC3::BitvectorTheoremProducer::bitBlastEqnRule(), CVC3::BitvectorTheoremProducer::bitExtractBitwise(), CVC3::BitvectorTheoremProducer::bitExtractBVMult(), CVC3::BitvectorTheoremProducer::bitExtractBVPlus(), CVC3::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), 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::bitwiseFlatten(), CVC3::BitvectorTheoremProducer::bvConstIneqn(), CVC3::BitvectorTheoremProducer::bvConstMultAssocRule(), CVC3::BitvectorTheoremProducer::bvMultAssocRule(), CVC3::BitvectorTheoremProducer::bvmultBVUminus(), CVC3::BitvectorTheoremProducer::bvmultConst(), CVC3::BitvectorTheoremProducer::bvMultDistRule(), CVC3::BitvectorTheoremProducer::bvPlusAssociativityRule(), CVC3::BitvectorTheoremProducer::bvplusConst(), CVC3::BitvectorTheoremProducer::bvplusZeroConcatRule(), CVC3::BitvectorTheoremProducer::bvuminusBVConst(), CVC3::BitvectorTheoremProducer::bvuminusBVMult(), CVC3::BitvectorTheoremProducer::bvuminusBVPlus(), CVC3::BitvectorTheoremProducer::bvuminusBVUminus(), CVC3::BitvectorTheoremProducer::bvuminusToBVPlus(), CVC3::BitvectorTheoremProducer::bvuminusVar(), CVC3::ArithTheoremProducerOld::canonComboLikeTerms(), CVC3::ArithTheoremProducer::canonComboLikeTerms(), CVC3::ArithTheoremProducerOld::canonDivide(), CVC3::ArithTheoremProducer::canonDivide(), CVC3::ArithTheoremProducerOld::canonDivideConst(), CVC3::ArithTheoremProducer::canonDivideConst(), CVC3::ArithTheoremProducerOld::canonDivideMult(), CVC3::ArithTheoremProducer::canonDivideMult(), CVC3::ArithTheoremProducerOld::canonDividePlus(), CVC3::ArithTheoremProducer::canonDividePlus(), CVC3::ArithTheoremProducerOld::canonDivideVar(), CVC3::ArithTheoremProducer::canonDivideVar(), CVC3::ArithTheoremProducerOld::canonFlattenSum(), CVC3::ArithTheoremProducer::canonFlattenSum(), CVC3::ArithTheoremProducerOld::canonInvertConst(), CVC3::ArithTheoremProducer::canonInvertConst(), CVC3::ArithTheoremProducerOld::canonInvertLeaf(), CVC3::ArithTheoremProducer::canonInvertLeaf(), CVC3::ArithTheoremProducerOld::canonInvertMult(), CVC3::ArithTheoremProducer::canonInvertMult(), CVC3::ArithTheoremProducerOld::canonInvertPow(), CVC3::ArithTheoremProducer::canonInvertPow(), CVC3::ArithTheoremProducerOld::canonMult(), CVC3::ArithTheoremProducer::canonMult(), CVC3::ArithTheoremProducerOld::canonMultConstConst(), CVC3::ArithTheoremProducer::canonMultConstConst(), CVC3::ArithTheoremProducerOld::canonMultConstSum(), CVC3::ArithTheoremProducer::canonMultConstSum(), CVC3::ArithTheoremProducerOld::canonMultConstTerm(), CVC3::ArithTheoremProducer::canonMultConstTerm(), CVC3::ArithTheoremProducerOld::canonMultMtermMterm(), CVC3::ArithTheoremProducer::canonMultMtermMterm(), CVC3::ArithTheoremProducerOld::canonMultOne(), CVC3::ArithTheoremProducer::canonMultOne(), CVC3::ArithTheoremProducerOld::canonMultTermConst(), CVC3::ArithTheoremProducer::canonMultTermConst(), CVC3::ArithTheoremProducerOld::canonMultZero(), CVC3::ArithTheoremProducer::canonMultZero(), CVC3::ArithTheoremProducerOld::canonPlus(), CVC3::ArithTheoremProducer::canonPlus(), CVC3::ArithTheoremProducerOld::canonPowConst(), CVC3::ArithTheoremProducer::canonPowConst(), CVC3::ArithTheoremProducerOld::canonUMinusToDivide(), CVC3::ArithTheoremProducer::canonUMinusToDivide(), CVC3::BitvectorTheoremProducer::combineLikeTermsRule(), CVC3::BitvectorTheoremProducer::concatConst(), CVC3::BitvectorTheoremProducer::concatFlatten(), CVC3::BitvectorTheoremProducer::concatMergeExtract(), CVC3::BitvectorTheoremProducer::constMultToPlus(), CVC3::ArithTheoremProducerOld::constPredicate(), CVC3::ArithTheoremProducer::constPredicate(), CVC3::BitvectorTheoremProducer::constWidthLeftShiftToConcat(), CVC3::ArithTheoremProducerOld::dummyTheorem(), CVC3::ArithTheoremProducer::dummyTheorem(), CVC3::BitvectorTheoremProducer::eqConst(), CVC3::ArithTheoremProducerOld::eqToIneq(), CVC3::ArithTheoremProducer::eqToIneq(), CVC3::CommonTheoremProducer::excludedMiddle(), 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::ArithTheoremProducer::flipInequality(), CVC3::BitvectorTheoremProducer::generalIneqn(), CVC3::RWTheoremValue::getAssumptionsRef(), CVC3::Theorem::getAssumptionsRef(), CVC3::SearchImplBase::getAssumptionsUsed(), CVC3::CoreTheoremProducer::iffAndDistrib(), CVC3::CoreTheoremProducer::iffOrDistrib(), CVC3::CoreTheoremProducer::IffToIte(), CVC3::CNF_TheoremProducer::ifLiftRule(), CVC3::CoreTheoremProducer::ifLiftUnaryRule(), CVC3::ArithTheoremProducerOld::implyNegatedInequality(), CVC3::ArithTheoremProducer::implyNegatedInequality(), CVC3::ArithTheoremProducerOld::implyWeakerInequality(), CVC3::ArithTheoremProducer::implyWeakerInequality(), CVC3::CoreTheoremProducer::ImpToIte(), CVC3::ArithTheoremProducerOld::integerSplit(), CVC3::ArithTheoremProducer::integerSplit(), CVC3::ArrayTheoremProducer::interchangeIndices(), CVC3::ArithTheoremProducerOld::isIntConst(), CVC3::ArithTheoremProducer::isIntConst(), CVC3::BitvectorTheoremProducer::iteBVnegRule(), CVC3::BitvectorTheoremProducer::iteExtractRule(), CVC3::CNF_TheoremProducer::learnedClause(), CVC3::ArithTheoremProducerOld::leftMinusRight(), CVC3::ArithTheoremProducer::leftMinusRight(), CVC3::BitvectorTheoremProducer::leftShiftToConcat(), CVC3::BitvectorTheoremProducer::lhsEqRhsIneqn(), CVC3::BitvectorTheoremProducer::lhsMinusRhsRule(), CVC3::ArrayTheoremProducer::liftReadIte(), CVC3::ArithTheoremProducerOld::minusToPlus(), CVC3::ArithTheoremProducer::minusToPlus(), CVC3::ArithTheoremProducerOld::moveSumConstantRight(), CVC3::ArithTheoremProducer::moveSumConstantRight(), CVC3::ArithTheoremProducerOld::multEqn(), CVC3::ArithTheoremProducer::multEqn(), CVC3::ArithTheoremProducerOld::multIneqn(), CVC3::ArithTheoremProducer::multIneqn(), CVC3::ArithTheoremProducerOld::negatedInequality(), CVC3::ArithTheoremProducer::negatedInequality(), CVC3::BitvectorTheoremProducer::negBVand(), CVC3::BitvectorTheoremProducer::negBVor(), CVC3::BitvectorTheoremProducer::negBVxnor(), CVC3::BitvectorTheoremProducer::negBVxor(), CVC3::BitvectorTheoremProducer::negConcat(), CVC3::BitvectorTheoremProducer::negConst(), CVC3::BitvectorTheoremProducer::negNeg(), CVC3::TheoremProducer::newAssumption(), CVC3::DatatypeTheoremProducer::noCycle(), CVC3::BitvectorTheoremProducer::notBVLTRule(), CVC3::CoreTheoremProducer::NotToIte(), CVC3::BitvectorTheoremProducer::oneCoeffBVMult(), CVC3::ArithTheoremProducerOld::oneElimination(), CVC3::ArithTheoremProducer::oneElimination(), CVC3::CoreTheoremProducer::orDistributivityRule(), CVC3::BitvectorTheoremProducer::orOne(), CVC3::CoreTheoremProducer::OrToIte(), CVC3::BitvectorTheoremProducer::orZero(), CVC3::BitvectorTheoremProducer::padBVLTRule(), CVC3::BitvectorTheoremProducer::padBVMult(), CVC3::BitvectorTheoremProducer::padBVPlus(), CVC3::BitvectorTheoremProducer::padBVSLTRule(), CVC3::ArithTheoremProducerOld::plusPredicate(), CVC3::ArithTheoremProducer::plusPredicate(), CVC3::ArrayTheoremProducer::readArrayLiteral(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::CoreTheoremProducer::rewriteAndSubterms(), CVC3::BitvectorTheoremProducer::rewriteBVSub(), CVC3::CoreTheoremProducer::rewriteDistinct(), CVC3::CommonTheoremProducer::rewriteIff(), CVC3::CoreTheoremProducer::rewriteImplies(), CVC3::CoreTheoremProducer::rewriteIteBool(), CVC3::CoreTheoremProducer::rewriteIteCond(), CVC3::CoreTheoremProducer::rewriteIteFalse(), CVC3::CoreTheoremProducer::rewriteIteSame(), CVC3::CoreTheoremProducer::rewriteIteToAnd(), CVC3::CoreTheoremProducer::rewriteIteToIff(), CVC3::CoreTheoremProducer::rewriteIteToImp(), CVC3::CoreTheoremProducer::rewriteIteToNot(), CVC3::CoreTheoremProducer::rewriteIteToOr(), CVC3::CoreTheoremProducer::rewriteIteTrue(), 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::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::BitvectorTheoremProducer::rewriteXOR(), CVC3::ArithTheoremProducerOld::rightMinusLeft(), CVC3::ArithTheoremProducer::rightMinusLeft(), CVC3::BitvectorTheoremProducer::rightShiftToConcat(), CVC3::BitvectorTheoremProducer::signBVLTRule(), CVC3::BitvectorTheoremProducer::signExtendRule(), CVC3::CommonTheoremProducer::skolemizeRewrite(), CVC3::CommonTheoremProducer::skolemizeRewriteVar(), CVC3::ArithTheoremProducerOld::trustedRewrite(), CVC3::ArithTheoremProducer::trustedRewrite(), CVC3::CoreTheoremProducer::typePred(), CVC3::BitvectorTheoremProducer::typePredBit(), CVC3::ArithTheoremProducerOld::uMinusToMult(), CVC3::ArithTheoremProducer::uMinusToMult(), CVC3::CommonTheoremProducer::varIntroRule(), CVC3::ArithTheoremProducerOld::varToMult(), CVC3::ArithTheoremProducer::varToMult(), CVC3::CommonTheoremProducer::xorToIff(), CVC3::BitvectorTheoremProducer::zeroCoeffBVMult(), CVC3::BitvectorTheoremProducer::zeroLeq(), and CVC3::BitvectorTheoremProducer::zeroPaddingRule().
| void CVC3::Assumptions::add1 | ( | const Theorem & | t | ) | [inline] |
Definition at line 83 of file assumptions.h.
References d_vector, and DebugAssert.
Referenced by CVC3::RegTheoremValue::RegTheoremValue().
| void Assumptions::add | ( | const Theorem & | t | ) |
Definition at line 173 of file assumptions.cpp.
References CVC3::compare(), d_vector, empty(), and CVC3::Theorem::getAssumptionsRef().
| void CVC3::Assumptions::add | ( | const Assumptions & | a | ) | [inline] |
| void CVC3::Assumptions::clear | ( | ) | [inline] |
| unsigned CVC3::Assumptions::size | ( | ) | const [inline] |
Definition at line 92 of file assumptions.h.
References d_vector.
Referenced by getFirst(), CVC3::RegTheoremValue::~RegTheoremValue(), and CVC3::RWTheoremValue::~RWTheoremValue().
| bool CVC3::Assumptions::empty | ( | ) | const [inline] |
Definition at line 93 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 96 of file assumptions.h.
References d_vector, DebugAssert, and size().
Referenced by CVC3::RegTheoremValue::~RegTheoremValue(), and CVC3::RWTheoremValue::~RWTheoremValue().
| string Assumptions::toString | ( | ) | const |
Definition at line 233 of file assumptions.cpp.
Referenced by CVC3::TheoryQuant::notifyInconsistent(), print(), and CVC3::TheoremValue::toString().
| void Assumptions::print | ( | ) | const |
Definition at line 254 of file assumptions.cpp.
References CVC3::compare(), and d_vector.
Referenced by findExprs(), and findTheorem().
| iterator CVC3::Assumptions::begin | ( | ) | const [inline] |
Definition at line 149 of file assumptions.h.
References d_vector.
Referenced by CVC3::SearchEngineFast::analyzeUIPs(), findExpr(), findExprs(), CVC3::TheoryQuant::findInstAssumptions(), CVC3::VCL::getAssumptions(), CVC3::Theorem::getAssumptionsRec(), CVC3::operator-(), CVC3::RegTheoremValue::RegTheoremValue(), and CVC3::SearchEngineFast::traceConflict().
| iterator CVC3::Assumptions::end | ( | ) | const [inline] |
Definition at line 150 of file assumptions.h.
References d_vector.
Referenced by CVC3::SearchEngineFast::analyzeUIPs(), findExpr(), findExprs(), CVC3::TheoryQuant::findInstAssumptions(), CVC3::VCL::getAssumptions(), CVC3::Theorem::getAssumptionsRec(), CVC3::RWTheoremValue::init(), CVC3::operator-(), CVC3::Theorem::recursivePrint(), CVC3::RegTheoremValue::RegTheoremValue(), and CVC3::SearchEngineFast::traceConflict().
| Assumptions operator- | ( | const Assumptions & | a, | |
| const Expr & | e | |||
| ) | [friend] |
| Assumptions operator- | ( | const Assumptions & | a, | |
| const std::vector< Expr > & | es | |||
| ) | [friend] |
Returns all (recursive) assumptions except those in es.
Definition at line 294 of file assumptions.cpp.
| std::ostream& operator<< | ( | std::ostream & | os, | |
| const Assumptions & | assump | |||
| ) | [friend] |
Definition at line 304 of file assumptions.cpp.
| bool operator== | ( | const Assumptions & | a1, | |
| const Assumptions & | a2 | |||
| ) | [friend] |
Definition at line 164 of file assumptions.h.
| bool operator!= | ( | const Assumptions & | a1, | |
| const Assumptions & | a2 | |||
| ) | [friend] |
Definition at line 166 of file assumptions.h.
std::vector<Theorem> CVC3::Assumptions::d_vector [private] |
Definition at line 46 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] |
1.5.1