CVC3
Public Member Functions | Static Public Member Functions | Private Attributes

CVC3::Type Class Reference

MS C++ specific settings. More...

#include <type.h>

Collaboration diagram for CVC3::Type:
Collaboration graph
[legend]

List of all members.

Public Member Functions

Static Public Member Functions

Private Attributes

Detailed Description

MS C++ specific settings.

Definition at line 42 of file type.h.

Constructor & Destructor Documentation

CVC3::Type::Type ( ) [inline]

Definition at line 47 of file type.h.

Referenced by funType().

CVC3::Type::Type ( Expr  expr)

Definition at line 634 of file expr.cpp.

References CVC3::ExprManager::checkType(), CVC3::Expr::getEM(), and CVC3::Expr::isNull().

CVC3::Type::Type ( const Type &  type) [inline]

Special constructor that doesn't check if expr is a type.

Definition at line 51 of file type.h.

CVC3::Type::Type ( Expr  expr,
bool  dummy 
) [inline]

Definition at line 52 of file type.h.

Member Function Documentation

const Expr& CVC3::Type::getExpr ( ) const [inline]

Definition at line 53 of file type.h.

References CVC3::Expr::arity().

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::TheoryDatatypeLazy::checkSat(), 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::TheoryArray::computeModelTerm(), CVC3::TheoryRecords::computeTCC(), 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::BitvectorTheoremProducer::createNewPlusCollection(), CVC3::VCL::createOp(), CVC3::VCL::createType(), CVC3::TheoryDatatype::dataType(), 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::TheoremProducer::newPf(), CVC3::TheoryBitvector::newSXExpr(), CVC3::Theory::newTypeExpr(), CVC3::Theory::newVar(), CVC3::QuantTheoremProducer::normalizeQuant(), CVC3::operator!=(), CVC3::TheoryQuant::TypeComp::operator()(), CVC3::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::Translator::processType(), CVC3::ExprManager::rebuildRec(), CVC3::BitvectorTheoremProducer::repeatRule(), CVC3::CommonTheoremProducer::rewriteIteFalse(), CVC3::CommonTheoremProducer::rewriteIteSame(), CVC3::CommonTheoremProducer::rewriteIteTrue(), CVC3::TheoryCore::rewriteLiteral(), CVC3::DatatypeTheoremProducer::rewriteSelCons(), CVC3::CommonTheoremProducer::rewriteUsingSymmetry(), CVC3::BitvectorTheoremProducer::rotlRule(), CVC3::BitvectorTheoremProducer::rotrRule(), CVC3::TheoryDatatypeLazy::setup(), CVC3::TheoryCore::setupTerm(), 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 56 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().

Type CVC3::Type::operator[] ( int  i) const [inline]

Definition at line 57 of file type.h.

bool CVC3::Type::isNull ( ) const [inline]

Definition at line 60 of file type.h.

References BOOLEAN.

Referenced by CVC3::Theory::addBoundVar(), CVC3::CoreTheoremProducer::AndToIte(), CVC3::TheoryDatatype::computeType(), CVC3::TheoryDatatype::dataType(), 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 61 of file type.h.

References SUBTYPE.

Referenced by CVC3::VCL::assertFormula(), CVC3::TheoryCore::assignValue(), CVC3::SearchSat::check(), CVC3::TheoryUF::checkType(), CVC3::TheoryRecords::checkType(), CVC3::TheoryArray::checkType(), CVC3::SearchSimple::checkValidInternal(), CVC3::SearchEngineFast::checkValidInternal(), CVC3::CompleteInstPreProcessor::collectHeads(), CVC3::TheoryQuant::computeType(), CVC3::TheoryCore::computeType(), CVC3::TheoryDatatype::dataType(), 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::matchListNew(), 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(), SAT::CNF_Manager::replaceITErec(), 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::TheoryQuant::setupTriggers(), CVC3::CompleteInstPreProcessor::simplifyEq(), CVC3::ExprTransform::simplifyWithCare(), CVC3::ExprTransform::specialSimplify(), CVC3::CommonTheoremProducer::symmetryRule(), CVC3::CommonTheoremProducer::transitivityRule(), CVC3::TheoryUF::update(), CVC3::Theory::updateCC(), and CVC3::CommonTheoremProducer::varIntroRule().

bool CVC3::Type::isSubtype ( ) const [inline]

Definition at line 62 of file type.h.

References ARROW.

bool CVC3::Type::isFunction ( ) const [inline]

Definition at line 63 of file type.h.

Referenced by CVC3::TheoryUF::checkType(), CVC3::TheoryRecords::checkType(), CVC3::TheoryCore::checkType(), CVC3::TheoryArray::checkType(), CVC3::TheoryCore::computeBaseType(), CVC3::TheorySimulate::computeTCC(), CVC3::TheoryUF::computeType(), CVC3::TheorySimulate::computeType(), CVC3::TheoryCore::computeType(), CVC3::VCL::createOp(), CVC3::TheoryDatatype::dataType(), CVC3::TheoryDatatype::getConstant(), CVC3::Theory::newFunction(), and CVC3::Theory::newVar().

Cardinality CVC3::Type::card ( ) const [inline]

Return cardinality of type.

Definition at line 65 of file type.h.

References CVC3::Expr::typeEnumerateFinite().

Referenced by CVC3::TheoryArray::finiteTypeInfo(), CVC3::TheoryUF::setup(), and CVC3::TheoryArray::setup().

Expr CVC3::Type::enumerateFinite ( Unsigned  n) const [inline]

Return nth (starting with 0) element in a finite type.

Returns NULL Expr if unable to compute nth element

Definition at line 69 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 71 of file type.h.

References CVC3::ExprManager::boolExpr().

Referenced by CVC3::TheoryArray::finiteTypeInfo().

static Type CVC3::Type::typeBool ( ExprManager *  em) [inline, static]

Definition at line 74 of file type.h.

References ANY_TYPE, and CVC3::ExprManager::newLeafExpr().

Referenced by CVC3::Theory::boolType(), and CVC3::ExprManager::ExprManager().

static Type CVC3::Type::anyType ( ExprManager *  em) [inline, static]

Definition at line 75 of file type.h.

Referenced by CVC3::TheoryCore::computeType(), CVC3::TheoryBitvector::computeType(), CVC3::TheoryArray::computeType(), CVC3::TheoryDatatype::dataType(), and CVC3::TheoryQuant::TheoryQuant().

Type CVC3::Type::funType ( const std::vector< Type > &  typeDom,
const Type &  typeRan 
) [static]

Definition at line 641 of file expr.cpp.

References ARROW, getExpr(), and Type().

Referenced by CVC3::TheoryUF::computeType(), CVC3::TheorySimulate::computeType(), CVC3::TheoryDatatype::dataType(), and CVC3::VCL::funType().

Type CVC3::Type::funType ( const Type &  typeRan) const [inline]

Definition at line 77 of file type.h.

References ARROW, and d_expr.

std::string CVC3::Type::toString ( ) const [inline]

Definition at line 81 of file type.h.

Referenced by CVC3::Theory::addBoundVar(), CVC3::VCL::assertFormula(), CVC3::BitvectorTheoremProducer::bitExtractBitwise(), CVC3::SearchSat::check(), CVC3::TheoryDatatypeLazy::checkSat(), 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::TheoryArithOld::refineCounterExample(), CVC3::TheoryArithNew::refineCounterExample(), CVC3::TheoryArith3::refineCounterExample(), CVC3::SearchSimple::restartInternal(), CVC3::SearchEngineFast::restartInternal(), CVC3::TheoryCore::rewrite(), and CVC3::VCL::varExpr().

Member Data Documentation

sdb home mdeters cvc3 docs cvc3 src include type h Expr CVC3::Type::d_expr [private]

Definition at line 44 of file type.h.

Referenced by funType().

The documentation for this class was generated from the following files:
Generated on Thu Sep 1 2011 19:35:15 for CVC3 by  doxygen 1.7.3