CVC3  2.4.1
Public Member Functions | Static Public Member Functions | Private Attributes | List of all members
CVC3::Type Class Reference

MS C++ specific settings. More...

#include <type.h>

Public Member Functions

 Type ()
 
 Type (Expr expr)
 
 Type (const Type &type)
 Special constructor that doesn't check if expr is a type. More...
 
 Type (Expr expr, bool dummy)
 
const ExprgetExpr () const
 
int arity () const
 
Type operator[] (int i) const
 
bool isNull () const
 
bool isBool () const
 
bool isSubtype () const
 
bool isFunction () const
 
Cardinality card () const
 Return cardinality of type. More...
 
Expr enumerateFinite (Unsigned n) const
 Return nth (starting with 0) element in a finite type. More...
 
Unsigned sizeFinite () const
 Return size of a finite type; returns 0 if size cannot be determined. More...
 
Type funType (const Type &typeRan) const
 
std::string toString () const
 

Static Public Member Functions

static Type typeBool (ExprManager *em)
 
static Type anyType (ExprManager *em)
 
static Type funType (const std::vector< Type > &typeDom, const Type &typeRan)
 

Private Attributes

Expr d_expr
 

Detailed Description

MS C++ specific settings.

Definition at line 42 of file type.h.

Constructor & Destructor Documentation

CVC3::Type::Type ( )
inline

Definition at line 46 of file type.h.

Referenced by funType().

CVC3::Type::Type ( Expr  expr)
CVC3::Type::Type ( const Type type)
inline

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

Definition at line 50 of file type.h.

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

Definition at line 51 of file type.h.

Member Function Documentation

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

Definition at line 52 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::TheoryDatatypeLazy::checkSat(), CVC3::TheoryDatatype::checkSat(), CVC3::TheoryRecords::computeBaseType(), CVC3::TheoryUF::computeBaseType(), CVC3::TheoryArray::computeBaseType(), CVC3::TheoryArithNew::computeBaseType(), CVC3::TheoryArith3::computeBaseType(), CVC3::TheoryArithOld::computeBaseType(), CVC3::TheoryCore::computeBaseType(), CVC3::TheoryRecords::computeModel(), CVC3::TheoryRecords::computeModelTerm(), CVC3::TheoryArray::computeModelTerm(), CVC3::TheoryRecords::computeTCC(), CVC3::TypeComputerCore::computeType(), CVC3::TheoryRecords::computeType(), CVC3::TheoryDatatype::computeType(), CVC3::ExprManager::computeType(), CVC3::TheoryBitvector::computeType(), CVC3::TheoryCore::computeType(), CVC3::TheoryRecords::computeTypePred(), CVC3::TheoryArithNew::computeTypePred(), CVC3::TheoryBitvector::computeTypePred(), CVC3::TheoryArith3::computeTypePred(), CVC3::TheoryArithOld::computeTypePred(), CVC3::TheoryCore::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::TheoryBitvector::parseExprOp(), CVC3::TheoryCore::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
Type CVC3::Type::operator[] ( int  i) const
inline

Definition at line 56 of file type.h.

bool CVC3::Type::isNull ( ) const
inline
bool CVC3::Type::isBool ( ) const
inline

Definition at line 60 of file type.h.

References BOOLEAN.

Referenced by CVC3::VCL::assertFormula(), CVC3::TheoryCore::assignValue(), CVC3::SearchSat::check(), CVC3::TheoryRecords::checkType(), CVC3::TheoryUF::checkType(), CVC3::TheoryArray::checkType(), CVC3::SearchSimple::checkValidInternal(), CVC3::SearchEngineFast::checkValidInternal(), CVC3::CompleteInstPreProcessor::collectHeads(), CVC3::TheoryCore::computeType(), CVC3::TheoryQuant::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 61 of file type.h.

References SUBTYPE.

bool CVC3::Type::isFunction ( ) const
inline
Cardinality CVC3::Type::card ( ) const
inline

Return cardinality of type.

Definition at line 64 of file type.h.

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 68 of file type.h.

References CVC3::Expr::typeEnumerateFinite().

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 70 of file type.h.

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

static Type CVC3::Type::typeBool ( ExprManager em)
inlinestatic

Definition at line 73 of file type.h.

References CVC3::ExprManager::boolExpr().

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

static Type CVC3::Type::anyType ( ExprManager em)
inlinestatic
Type CVC3::Type::funType ( const std::vector< Type > &  typeDom,
const Type typeRan 
)
static
Type CVC3::Type::funType ( const Type typeRan) const
inline

Definition at line 76 of file type.h.

References ARROW, and d_expr.

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

Member Data Documentation

Expr CVC3::Type::d_expr
private

Definition at line 43 of file type.h.

Referenced by funType().


The documentation for this class was generated from the following files: