#include <type.h>
Collaboration diagram for CVC3::Type:
Definition at line 127 of file type.h.
| CVC3::Type::Type | ( | Expr | expr | ) |
Definition at line 593 of file expr.cpp.
References CVC3::ExprManager::checkType(), CVC3::Expr::getEM(), and CVC3::Expr::isNull().
| CVC3::Type::Type | ( | const Type & | type | ) | [inline] |
| const Expr& CVC3::Type::getExpr | ( | ) | const [inline] |
Definition at line 137 of file type.h.
Referenced by CVC3::arrayType(), CVC3::TheoryRecords::assertFact(), CVC3::TheoryDatatype::assertFact(), CVC3::BitvectorTheoremProducer::bitblastBVMult(), CVC3::BitvectorTheoremProducer::bitblastBVPlus(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::BitvectorTheoremProducer::bitBlastEqnRule(), CVC3::BitvectorTheoremProducer::bitExtractBitwise(), CVC3::BitvectorTheoremProducer::bitExtractBVASHR(), CVC3::BitvectorTheoremProducer::bitExtractBVLSHR(), CVC3::BitvectorTheoremProducer::bitExtractBVMult(), CVC3::BitvectorTheoremProducer::bitExtractBVSHL(), CVC3::BitvectorTheoremProducer::bitExtractConstBVMult(), CVC3::BitvectorTheoremProducer::bitExtractExtraction(), CVC3::BitvectorTheoremProducer::bitExtractFixedLeftShift(), CVC3::BitvectorTheoremProducer::bitExtractFixedRightShift(), CVC3::BitvectorTheoremProducer::bitExtractNot(), CVC3::BitvectorTheoremProducer::bvmultConst(), CVC3::BitvectorTheoremProducer::bvSDivRewrite(), CVC3::BitvectorTheoremProducer::bvshlSplit(), CVC3::TheoryBitvector::BVSize(), CVC3::BitvectorTheoremProducer::bvSModRewrite(), CVC3::BitvectorTheoremProducer::bvSRemRewrite(), CVC3::BitvectorTheoremProducer::bvUDivTheorem(), CVC3::TheoryDatatype::checkSat(), CVC3::TheoryUF::computeBaseType(), CVC3::TheoryRecords::computeBaseType(), CVC3::TheoryCore::computeBaseType(), CVC3::TheoryArray::computeBaseType(), CVC3::TheoryArithOld::computeBaseType(), CVC3::TheoryArithNew::computeBaseType(), CVC3::TheoryArith3::computeBaseType(), CVC3::TheoryRecords::computeModel(), CVC3::TheoryRecords::computeModelTerm(), CVC3::TheoryRecords::computeType(), CVC3::TheoryDatatype::computeType(), CVC3::TheoryCore::computeType(), CVC3::TypeComputerCore::computeType(), CVC3::TheoryBitvector::computeType(), CVC3::ExprManager::computeType(), CVC3::TheoryRecords::computeTypePred(), CVC3::TheoryCore::computeTypePred(), CVC3::TheoryBitvector::computeTypePred(), CVC3::TheoryArithOld::computeTypePred(), CVC3::TheoryArithNew::computeTypePred(), CVC3::TheoryArith3::computeTypePred(), CVC3::VCL::createOp(), CVC3::VCL::createType(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::Translator::finish(), CVC3::TheoryDatatype::finiteTypeInfo(), funType(), CVC3::Theory::getBaseType(), CVC3::TheoryBitvector::getBitvectorTypeParam(), CVC3::TheoryDatatype::getConstant(), CVC3::TheoryDatatype::getReachablePredicate(), CVC3::Theory::getTypePred(), CVC3::VCL::importType(), CVC3::TheoryDatatypeLazy::initializeLabels(), CVC3::TheoryDatatype::initializeLabels(), CVC3::TheoryDatatypeLazy::instantiate(), CVC3::TheoryDatatype::instantiate(), CVC3::isArray(), CVC3::isDatatype(), CVC3::isInt(), CVC3::isReal(), CVC3::TheoryRecords::isRecordType(), CVC3::TheoryRecords::isTupleType(), CVC3::TheoryBitvector::newBitvectorTypePred(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::ExprManager::newBoundVarExpr(), CVC3::TheoryBitvector::newBVAndExpr(), CVC3::TheoryBitvector::newBVCompExpr(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVIndexExpr(), CVC3::TheoryBitvector::newBVLEExpr(), CVC3::TheoryBitvector::newBVLTExpr(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoryBitvector::newBVNandExpr(), CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoryBitvector::newBVNorExpr(), CVC3::TheoryBitvector::newBVOrExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoryBitvector::newBVSDivExpr(), CVC3::TheoryBitvector::newBVSLEExpr(), CVC3::TheoryBitvector::newBVSLTExpr(), CVC3::TheoryBitvector::newBVSModExpr(), CVC3::TheoryBitvector::newBVSRemExpr(), CVC3::TheoryBitvector::newBVSubExpr(), CVC3::TheoryBitvector::newBVUDivExpr(), CVC3::TheoryBitvector::newBVUminusExpr(), CVC3::TheoryBitvector::newBVURemExpr(), CVC3::TheoryBitvector::newBVXnorExpr(), CVC3::TheoryBitvector::newBVXorExpr(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoryBitvector::newFixedConstWidthLeftShiftExpr(), CVC3::TheoryBitvector::newFixedLeftShiftExpr(), CVC3::TheoryBitvector::newFixedRightShiftExpr(), CVC3::Theory::newFunction(), CVC3::TheoryBitvector::newSXExpr(), CVC3::Theory::newTypeExpr(), CVC3::Theory::newVar(), CVC3::TheoryQuant::TypeComp::operator()(), CVC3::operator<<(), CVC3::TheoryBitvector::pad(), CVC3::BitvectorTheoremProducer::pad(), CVC3::TheoryRecords::parseExprOp(), CVC3::TheoryCore::parseExprOp(), CVC3::TheoryBitvector::parseExprOp(), CVC3::Translator::preprocess2Rec(), CVC3::TheoryCore::print(), CVC3::VCCmd::printSymbols(), CVC3::Translator::processType(), CVC3::ExprManager::rebuildRec(), CVC3::BitvectorTheoremProducer::repeatRule(), CVC3::CommonTheoremProducer::rewriteIteFalse(), CVC3::CommonTheoremProducer::rewriteIteSame(), CVC3::CommonTheoremProducer::rewriteIteTrue(), CVC3::DatatypeTheoremProducer::rewriteSelCons(), CVC3::CommonTheoremProducer::rewriteUsingSymmetry(), CVC3::BitvectorTheoremProducer::rotlRule(), CVC3::BitvectorTheoremProducer::rotrRule(), CVC3::TheoryDatatypeLazy::setup(), CVC3::BitvectorTheoremProducer::signExtendRule(), CVC3::CommonTheoremProducer::symmetryRule(), CVC3::Theory::theoryOf(), CVC3::CommonTheoremProducer::transitivityRule(), CVC3::BitvectorTheoremProducer::typePredBit(), CVC3::VCL::varExpr(), CVC3::BitvectorTheoremProducer::zeroExtendRule(), CVC3::BitvectorTheoremProducer::zeroPaddingRule(), and CVC3::Translator::zeroVar().
| int CVC3::Type::arity | ( | ) | const [inline] |
Definition at line 140 of file type.h.
Referenced by CVC3::TheorySimulate::computeTCC(), CVC3::TheoryUF::computeType(), CVC3::TheorySimulate::computeType(), CVC3::TheoryCore::computeType(), CVC3::VCL::createOp(), CVC3::TheoryDatatypeLazy::instantiate(), CVC3::TheoryDatatype::instantiate(), CVC3::isConstructor(), CVC3::Theory::newFunction(), CVC3::Theory::newVar(), and CVC3::DatatypeTheoremProducer::noCycle().
| bool CVC3::Type::isNull | ( | ) | const [inline] |
Definition at line 144 of file type.h.
Referenced by CVC3::Theory::addBoundVar(), CVC3::CoreTheoremProducer::AndToIte(), CVC3::TheoryDatatype::computeType(), CVC3::Expr::getType(), CVC3::ExprManager::newBoundVarExpr(), CVC3::Theory::newFunction(), CVC3::Theory::newVar(), CVC3::CoreTheoremProducer::OrToIte(), CVC3::Translator::preprocess2Rec(), CVC3::TheoryCore::print(), CVC3::ExprManager::rebuildRec(), CVC3::CoreTheoremProducer::rewriteIteElse(), CVC3::CommonTheoremProducer::rewriteIteFalse(), CVC3::CommonTheoremProducer::rewriteIteSame(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::CommonTheoremProducer::rewriteIteTrue(), CVC3::CommonTheoremProducer::rewriteUsingSymmetry(), and CVC3::CommonTheoremProducer::transitivityRule().
| bool CVC3::Type::isBool | ( | ) | const [inline] |
Definition at line 145 of file type.h.
Referenced by CVC3::VCL::assertFormula(), CVC3::TheoryCore::assignValue(), CVC3::SearchSat::check(), CVC3::TheoryUF::checkType(), CVC3::TheoryArray::checkType(), CVC3::SearchSimple::checkValidInternal(), CVC3::SearchEngineFast::checkValidInternal(), CVC3::CompleteInstPreProcessor::collectHeads(), CVC3::TheoryQuant::computeType(), CVC3::TheoryCore::computeType(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::CommonTheoremProducer::findITE(), findPolarity(), findPolarityAtomic(), CVC3::BitvectorTheoremProducer::generalIneqn(), CVC3::TheoryDatatype::getConstant(), CVC3::RWTheoremValue::getExpr(), CVC3::CommonTheoremProducer::iffContrapositive(), CVC3::SearchEngineTheoremProducer::iffToClauses(), CVC3::CoreTheoremProducer::IffToIte(), CVC3::CNF_TheoremProducer::ifLiftRule(), CVC3::CoreTheoremProducer::ifLiftUnaryRule(), CVC3::CoreTheoremProducer::ImpToIte(), CVC3::ArrayTheoremProducer::interchangeIndices(), CVC3::Expr::isTerm(), CVC3::SearchEngineTheoremProducer::iteToClauses(), CVC3::TheoryQuant::matchListOld(), CVC3::Theory::newFunction(), CVC3::ExprTransform::newPP(), CVC3::ExprTransform::newPPrec(), CVC3::TheoryQuant::newTopMatchNoSig(), CVC3::TheoryQuant::newTopMatchSig(), CVC3::Theory::newVar(), CVC3::CoreTheoremProducer::NotToIte(), CVC3::TheoryCore::print(), CVC3::TheoryCore::processUpdates(), CVC3::VCL::query(), CVC3::CompleteInstPreProcessor::recInstMacros(), CVC3::CompleteInstPreProcessor::recRewriteNot(), CVC3::CompleteInstPreProcessor::recSkolemize(), CVC3::TheoryQuant::recursiveMap(), CVC3::SearchSimple::restartInternal(), CVC3::SearchEngineFast::restartInternal(), CVC3::TheoryUF::rewrite(), CVC3::CoreTheoremProducer::rewriteIteBool(), CVC3::CoreTheoremProducer::rewriteIteElse(), CVC3::CommonTheoremProducer::rewriteIteFalse(), CVC3::CommonTheoremProducer::rewriteIteSame(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::CommonTheoremProducer::rewriteIteTrue(), CVC3::ArrayTheoremProducer::rewriteReadWrite(), CVC3::ArrayTheoremProducer::rewriteReadWrite2(), CVC3::ArrayTheoremProducer::rewriteSameStore(), CVC3::ArrayTheoremProducer::rewriteWriteWrite(), CVC3::CompleteInstPreProcessor::simplifyEq(), CVC3::ExprTransform::simplifyWithCare(), CVC3::CommonTheoremProducer::symmetryRule(), CVC3::CommonTheoremProducer::transitivityRule(), CVC3::TheoryUF::update(), CVC3::Theory::updateCC(), and CVC3::CommonTheoremProducer::varIntroRule().
| bool CVC3::Type::isFunction | ( | ) | const [inline] |
Definition at line 147 of file type.h.
Referenced by CVC3::TheoryCore::checkType(), CVC3::TheoryArray::checkType(), CVC3::TheoryCore::computeBaseType(), CVC3::TheoryUF::computeType(), CVC3::TheoryCore::computeType(), CVC3::VCL::createOp(), CVC3::TheoryDatatype::getConstant(), and CVC3::Theory::newFunction().
| Cardinality CVC3::Type::card | ( | ) | const [inline] |
Return cardinality of type.
Definition at line 149 of file type.h.
Referenced by CVC3::TheoryArray::finiteTypeInfo().
Return nth (starting with 0) element in a finite type.
Returns NULL Expr if unable to compute nth element
Definition at line 153 of file type.h.
Referenced by CVC3::TheoryArray::finiteTypeInfo().
| Unsigned CVC3::Type::sizeFinite | ( | ) | const [inline] |
Return size of a finite type; returns 0 if size cannot be determined.
Definition at line 155 of file type.h.
Referenced by CVC3::TheoryArray::finiteTypeInfo().
| static Type CVC3::Type::typeBool | ( | ExprManager * | em | ) | [inline, static] |
Definition at line 158 of file type.h.
Referenced by CVC3::Theory::boolType(), and CVC3::ExprManager::ExprManager().
| static Type CVC3::Type::anyType | ( | ExprManager * | em | ) | [inline, static] |
Definition at line 159 of file type.h.
Referenced by CVC3::TheoryCore::computeType(), CVC3::TheoryBitvector::computeType(), CVC3::TheoryArray::computeType(), and CVC3::TheoryQuant::TheoryQuant().
Definition at line 600 of file expr.cpp.
References CVC3::ARROW, getExpr(), and Type().
Referenced by CVC3::TheoryUF::computeType(), CVC3::TheorySimulate::computeType(), and CVC3::VCL::funType().
| std::string CVC3::Type::toString | ( | ) | const [inline] |
Definition at line 165 of file type.h.
Referenced by CVC3::Theory::addBoundVar(), CVC3::VCL::assertFormula(), CVC3::BitvectorTheoremProducer::bitExtractBitwise(), CVC3::SearchSat::check(), CVC3::TheoryDatatype::checkSat(), CVC3::SearchSimple::checkValidInternal(), CVC3::SearchEngineFast::checkValidInternal(), CVC3::TheoryUF::computeBaseType(), CVC3::TheoryRecords::computeBaseType(), CVC3::TheoryCore::computeBaseType(), CVC3::TheoryArray::computeBaseType(), CVC3::TheoryArithOld::computeBaseType(), CVC3::TheoryArithNew::computeBaseType(), CVC3::TheoryArith3::computeBaseType(), CVC3::TheoryUF::computeType(), CVC3::TheorySimulate::computeType(), CVC3::TheoryQuant::computeType(), CVC3::TheoryCore::computeType(), CVC3::TheoryArray::computeType(), CVC3::TheoryArithOld::computeType(), CVC3::TheoryArithNew::computeType(), CVC3::TheoryArith3::computeType(), CVC3::TheoryBitvector::computeTypePred(), CVC3::VCL::createOp(), CVC3::Theory::getBaseType(), CVC3::TheoryDatatype::getConstant(), CVC3::TheoryDatatypeLazy::instantiate(), CVC3::TheoryDatatype::instantiate(), CVC3::Theory::newFunction(), CVC3::Theory::newVar(), CVC3::VCL::query(), CVC3::TheoryQuant::recursiveMap(), CVC3::SearchSimple::restartInternal(), CVC3::SearchEngineFast::restartInternal(), and CVC3::VCL::varExpr().
Expr CVC3::Type::d_expr [private] |
1.5.2