CVCL::Type Class Reference

#include <type.h>

Collaboration diagram for CVCL::Type:

[legend]List of all members.

Public Member Functions

• Type ()
• Type (Expr expr)
• Type (Expr expr, bool dummy)

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

• const Expr & getExpr () const
• int arity () const
• Type operator[] (int i) const
• bool isNull () const
• bool isBool () const
• bool isSubtype () const
• bool isFunction () const
• Type funType (const Type &typeRan) const
• std::string toString () const

Static Public Member Functions

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

Private Attributes

• Expr d_expr

---

Detailed Description

Definition at line 48 of file type.h.

---

Constructor & Destructor Documentation

CVCL::Type::Type (   )  [inline]

Definition at line 52 of file type.h. Referenced by funType(), operator[](), and typeBool().

CVCL::Type::Type (  Expr  expr  )

Definition at line 476 of file expr.cpp. References CVCL::ExprManager::checkType(), CVCL::Expr::getEM(), and CVCL::Expr::isNull().

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

Special constructor that doesn't check if expr is a type. Definition at line 56 of file type.h.

---

Member Function Documentation

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

Definition at line 57 of file type.h. References d_expr. Referenced by CVCL::TheoryDatatype::addSharedTerm(), CVCL::arrayType(), CVCL::TheoryRecords::assertFact(), CVCL::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVCL::BitvectorTheoremProducer::bitBlastEqnRule(), CVCL::BitvectorTheoremProducer::bitExtractBitwise(), CVCL::BitvectorTheoremProducer::bitExtractBVMult(), CVCL::BitvectorTheoremProducer::bitExtractConcatenation(), CVCL::BitvectorTheoremProducer::bitExtractConstBVMult(), CVCL::BitvectorTheoremProducer::bitExtractExtraction(), CVCL::BitvectorTheoremProducer::bitExtractFixedLeftShift(), CVCL::BitvectorTheoremProducer::bitExtractFixedRightShift(), CVCL::BitvectorTheoremProducer::bitExtractNot(), CVCL::BitvectorTheoremProducer::bvmultConst(), CVCL::BitvectorTheoremProducer::bvPlusAssociativityRule(), CVCL::TheoryBitvector::BVSize(), CVCL::TheoryDatatype::checkSat(), CVCL::TheoryUF::computeBaseType(), CVCL::TheoryRecords::computeBaseType(), TheoryCore::computeBaseType(), CVCL::TheoryArray::computeBaseType(), CVCL::TheoryArith::computeBaseType(), CVCL::TheoryRecords::computeModel(), CVCL::TheoryBitvector::computeModel(), CVCL::TheoryRecords::computeModelTerm(), CVCL::TheoryBitvector::computeModelTerm(), CVCL::TheoryArray::computeModelTerm(), CVCL::TheoryUF::computeType(), CVCL::TheoryRecords::computeType(), CVCL::TheoryDatatype::computeType(), CVCL::TypeComputerCore::computeType(), CVCL::TheoryBitvector::computeType(), CVCL::ExprManager::computeType(), CVCL::TheoryRecords::computeTypePred(), TheoryCore::computeTypePred(), CVCL::TheoryBitvector::computeTypePred(), CVCL::TheoryArith::computeTypePred(), CVCL::BitvectorTheoremProducer::createNewPlusCollection(), CVCL::BitvectorTheoremProducer::eqToBits(), CVCL::RecordsTheoremProducer::expandEq(), CVCL::RecordsTheoremProducer::expandNeq(), CVCL::RecordsTheoremProducer::expandRecord(), CVCL::RecordsTheoremProducer::expandTuple(), funType(), CVCL::Theory::getBaseType(), CVCL::TheoryBitvector::getBitvectorTypeParam(), CVCL::TheoryDatatype::getConsPos(), CVCL::TheoryDatatype::getConstant(), CVCL::TheoryDatatype::getReachablePredicate(), CVCL::Theory::getTypePred(), CVCL::VCL::importType(), CVCL::TheoryDatatypeLazy::initializeLabels(), CVCL::TheoryDatatype::initializeLabels(), CVCL::TheoryDatatypeLazy::instantiate(), CVCL::TheoryDatatype::instantiate(), CVCL::isArray(), CVCL::isDatatype(), CVCL::isInt(), CVCL::isReal(), CVCL::TheoryRecords::isRecordType(), CVCL::TheoryRecords::isTupleType(), CVCL::TheoryBitvector::newBitvectorTypePred(), CVCL::TheoryBitvector::newBoolExtractExpr(), CVCL::ExprManager::newBoundVarExpr(), CVCL::TheoryBitvector::newBVAndExpr(), CVCL::TheoryBitvector::newBVExtractExpr(), CVCL::TheoryBitvector::newBVLEExpr(), CVCL::TheoryBitvector::newBVLTExpr(), CVCL::TheoryBitvector::newBVMultExpr(), CVCL::TheoryBitvector::newBVNandExpr(), CVCL::TheoryBitvector::newBVNegExpr(), CVCL::TheoryBitvector::newBVNorExpr(), CVCL::TheoryBitvector::newBVOrExpr(), CVCL::TheoryBitvector::newBVUminusExpr(), CVCL::TheoryBitvector::newBVXnorExpr(), CVCL::TheoryBitvector::newBVXorExpr(), CVCL::TheoryBitvector::newConcatExpr(), CVCL::TheoryBitvector::newFixedLeftShiftExpr(), CVCL::TheoryBitvector::newFixedRightShiftExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoryBitvector::newSBVLEExpr(), CVCL::TheoryBitvector::newSBVLTExpr(), CVCL::TheoryBitvector::newSXExpr(), CVCL::operator!=(), CVCL::TheoryQuant::TypeComp::operator()(), CVCL::operator<<(), CVCL::operator==(), CVCL::TheoryBitvector::pad(), CVCL::BitvectorTheoremProducer::pad(), CVCL::TheoryRecords::parseExprOp(), TheoryCore::print(), CVCL::TheoryBitvector::pushNegation(), CVCL::ExprManager::rebuildRec(), CVCL::CommonTheoremProducer::reflexivityRule(), CVCL::CoreTheoremProducer::rewriteIteFalse(), CVCL::CoreTheoremProducer::rewriteIteSame(), CVCL::CoreTheoremProducer::rewriteIteTrue(), CVCL::DatatypeTheoremProducer::rewriteSelCons(), CVCL::CommonTheoremProducer::rewriteUsingSymmetry(), CVCL::TheoryDatatypeLazy::setup(), CVCL::TheoryDatatype::setup(), CVCL::TheoryBitvector::setupExpr(), TheoryCore::setupTerm(), CVCL::BitvectorTheoremProducer::signExtendRule(), CVCL::CommonTheoremProducer::symmetryRule(), CVCL::Theory::theoryOf(), toString(), CVCL::CommonTheoremProducer::transitivityRule(), CVCL::CoreTheoremProducer::typePred(), CVCL::BitvectorTheoremProducer::typePredBit(), and CVCL::BitvectorTheoremProducer::zeroPaddingRule().

int CVCL::Type::arity (   )  const [inline]

Definition at line 60 of file type.h. References CVCL::Expr::arity(), and d_expr. Referenced by CVCL::TheoryUF::computeModel(), CVCL::TheoryArray::computeModel(), CVCL::TheoryUF::computeTCC(), CVCL::TheorySimulate::computeTCC(), CVCL::TheoryUF::computeType(), CVCL::TheorySimulate::computeType(), CVCL::RecordsTheoremProducer::expandTuple(), CVCL::TheoryDatatype::getConsPos(), CVCL::TheoryDatatypeLazy::instantiate(), CVCL::TheoryDatatype::instantiate(), CVCL::isConstructor(), and CVCL::DatatypeTheoremProducer::noCycle().

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

Definition at line 61 of file type.h. References d_expr, and Type().

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

Definition at line 64 of file type.h. References d_expr, and CVCL::Expr::isNull(). Referenced by CVCL::CoreTheoremProducer::AndToIte(), CVCL::TheoryDatatype::computeType(), CVCL::Theory::getBaseType(), CVCL::Expr::getType(), CVCL::ExprManager::newBoundVarExpr(), CVCL::CoreTheoremProducer::OrToIte(), TheoryCore::print(), CVCL::ExprManager::rebuildRec(), CVCL::CommonTheoremProducer::reflexivityRule(), CVCL::CoreTheoremProducer::rewriteIteElse(), CVCL::CoreTheoremProducer::rewriteIteFalse(), CVCL::CoreTheoremProducer::rewriteIteSame(), CVCL::CoreTheoremProducer::rewriteIteThen(), CVCL::CoreTheoremProducer::rewriteIteTrue(), CVCL::CommonTheoremProducer::rewriteUsingSymmetry(), and CVCL::CommonTheoremProducer::transitivityRule().

bool CVCL::Type::isBool (   )  const [inline]

Definition at line 65 of file type.h. References CVCL::BOOLEAN, d_expr, and CVCL::Expr::getKind(). Referenced by CVCL::VCL::assertFormula(), TheoryCore::assignValue(), CVCL::SearchSat::check(), CVCL::TheoryUF::checkType(), CVCL::TheoryArray::checkType(), CVCL::SearchSimple::checkValidInternal(), CVCL::SearchEngineFast::checkValidInternal(), CVCL::ExprStream::collectShared(), CVCL::TheoryUF::computeTCC(), CVCL::TheoryQuant::computeType(), TheoryCore::computeType(), CVCL::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVCL::RecordsTheoremProducer::expandEq(), CVCL::RecordsTheoremProducer::expandNeq(), CVCL::BitvectorTheoremProducer::generalIneqn(), CVCL::TheoryDatatype::getConstant(), CVCL::ReflexivityTheoremValue::getExpr(), CVCL::RWTheoremValue::getExpr(), CVCL::CommonTheoremProducer::iffContrapositive(), CVCL::SearchEngineTheoremProducer::iffToClauses(), CVCL::CoreTheoremProducer::IffToIte(), CVCL::CNF_TheoremProducer::ifLiftRule(), CVCL::CoreTheoremProducer::ifLiftUnaryRule(), CVCL::CoreTheoremProducer::ImpToIte(), CVCL::ArrayTheoremProducer::interchangeIndices(), CVCL::Expr::isTerm(), CVCL::SearchEngineTheoremProducer::iteToClauses(), CVCL::CoreTheoremProducer::NotToIte(), TheoryCore::print(), TheoryCore::processUpdates(), CVCL::VCL::query(), CVCL::TheoryQuant::recursiveMap(), CVCL::CommonTheoremProducer::reflexivityRule(), SAT::CNF_Manager::replaceITErec(), CVCL::SearchSimple::restartInternal(), CVCL::SearchEngineFast::restartInternal(), CVCL::TheoryUF::rewrite(), CVCL::CoreTheoremProducer::rewriteIteBool(), CVCL::CoreTheoremProducer::rewriteIteElse(), CVCL::CoreTheoremProducer::rewriteIteFalse(), CVCL::CoreTheoremProducer::rewriteIteSame(), CVCL::CoreTheoremProducer::rewriteIteThen(), CVCL::CoreTheoremProducer::rewriteIteTrue(), CVCL::ArrayTheoremProducer::rewriteReadWrite(), CVCL::ArrayTheoremProducer::rewriteSameStore(), CVCL::ArrayTheoremProducer::rewriteWriteWrite(), CVCL::VCL::subtypeType(), CVCL::CommonTheoremProducer::symmetryRule(), CVCL::CommonTheoremProducer::transitivityRule(), and CVCL::CommonTheoremProducer::varIntroRule().

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

Definition at line 66 of file type.h. References d_expr, CVCL::Expr::getKind(), and CVCL::SUBTYPE.

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

Definition at line 67 of file type.h. References CVCL::ARROW, d_expr, and CVCL::Expr::getKind(). Referenced by CVCL::TheoryUF::checkType(), CVCL::TheoryRecords::checkType(), TheoryCore::checkType(), CVCL::TheoryArray::checkType(), TheoryCore::computeBaseType(), CVCL::TheoryUF::computeModel(), CVCL::TheoryUF::computeTCC(), CVCL::TheorySimulate::computeTCC(), CVCL::TheoryUF::computeType(), CVCL::TheorySimulate::computeType(), CVCL::VCCmd::evaluateCommand(), CVCL::TheoryDatatype::getConsPos(), CVCL::TheoryDatatype::getConstant(), and CVCL::VCL::subtypeType().

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

Definition at line 70 of file type.h. References CVCL::ExprManager::boolExpr(), and Type(). Referenced by CVCL::Theory::boolType(), and CVCL::ExprManager::ExprManager().

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

Definition at line 483 of file expr.cpp. References CVCL::ARROW, getExpr(), and Type(). Referenced by CVCL::TheoryUF::computeType(), CVCL::TheorySimulate::computeType(), and CVCL::VCL::funType().

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

Definition at line 72 of file type.h. References CVCL::ARROW, d_expr, and Type().

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

Definition at line 76 of file type.h. References getExpr(), and CVCL::Expr::toString(). Referenced by CVCL::VCL::assertFormula(), CVCL::BitvectorTheoremProducer::bitExtractBitwise(), CVCL::SearchSat::check(), checkRewriteType(), CVCL::TheoryDatatype::checkSat(), CVCL::SearchSimple::checkValidInternal(), CVCL::SearchEngineFast::checkValidInternal(), CVCL::TheoryUF::computeBaseType(), CVCL::TheoryRecords::computeBaseType(), TheoryCore::computeBaseType(), CVCL::TheoryArray::computeBaseType(), CVCL::TheoryArith::computeBaseType(), CVCL::TheoryUF::computeModel(), CVCL::TheoryUF::computeTCC(), CVCL::TheoryUF::computeType(), CVCL::TheorySimulate::computeType(), CVCL::TheoryQuant::computeType(), TheoryCore::computeType(), CVCL::TheoryBitvector::computeType(), CVCL::TheoryArray::computeType(), CVCL::TheoryArith::computeType(), CVCL::TheoryBitvector::computeTypePred(), CVCL::Theory::getBaseType(), CVCL::TheoryDatatype::getConsPos(), CVCL::TheoryDatatype::getConstant(), CVCL::Theory::getTypePred(), CVCL::TheoryDatatypeLazy::instantiate(), CVCL::TheoryDatatype::instantiate(), CVCL::VCL::printV(), CVCL::VCL::query(), CVCL::TheoryQuant::recursiveMap(), CVCL::TheoryArith::refineCounterExample(), CVCL::SearchSimple::restartInternal(), CVCL::SearchEngineFast::restartInternal(), TheoryCore::rewrite(), and CVCL::VCL::subtypeType().

---

Member Data Documentation

Expr CVCL::Type::d_expr [private]

Definition at line 49 of file type.h. Referenced by arity(), funType(), getExpr(), isBool(), isFunction(), isNull(), isSubtype(), and operator[]().

---

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

• type.h
• expr.cpp

---