CVC3::Type Class Reference

#include <type.h>

Collaboration diagram for CVC3::Type:

[legend]List of all members.

Public Member Functions

• Type ()
• Type (Expr expr)
• Type (const Type &type)

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

• Type (Expr expr, bool dummy)
• 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 anyType (ExprManager *em)
• static Type funType (const std::vector< Type > &typeDom, const Type &typeRan)

Private Attributes

• Expr d_expr

---

Detailed Description

Definition at line 117 of file type.h.

---

Constructor & Destructor Documentation

CVC3::Type::Type

(

)

[inline]

Definition at line 121 of file type.h.

Referenced by funType().

CVC3::Type::Type

(

Expr

expr

)

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

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

Definition at line 126 of file type.h.

---

Member Function Documentation

const Expr& CVC3::Type::getExpr

(

)

const [inline]

Definition at line 127 of file type.h.

Referenced by CVC3::arrayType(), CVC3::TheoryRecords::assertFact(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::BitvectorTheoremProducer::bitBlastEqnRule(), CVC3::BitvectorTheoremProducer::bitExtractBitwise(), CVC3::BitvectorTheoremProducer::bitExtractBVMult(), CVC3::BitvectorTheoremProducer::bitExtractConstBVMult(), CVC3::BitvectorTheoremProducer::bitExtractExtraction(), CVC3::BitvectorTheoremProducer::bitExtractFixedLeftShift(), CVC3::BitvectorTheoremProducer::bitExtractFixedRightShift(), CVC3::BitvectorTheoremProducer::bitExtractNot(), CVC3::BitvectorTheoremProducer::bvmultConst(), CVC3::TheoryBitvector::BVSize(), CVC3::TheoryDatatype::checkSat(), CVC3::TheoryUF::computeBaseType(), CVC3::TheoryRecords::computeBaseType(), CVC3::TheoryCore::computeBaseType(), CVC3::TheoryArray::computeBaseType(), CVC3::TheoryArithOld::computeBaseType(), CVC3::TheoryArithNew::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::VCL::createOp(), CVC3::VCL::createType(), CVC3::TheoryDatatype::dataType(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::Translator::finish(), 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::newBVSLEExpr(), CVC3::TheoryBitvector::newBVSLTExpr(), CVC3::TheoryBitvector::newBVSubExpr(), CVC3::TheoryBitvector::newBVUminusExpr(), 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::Translator::processType(), CVC3::TheoryBitvector::pushNegation(), CVC3::ExprManager::rebuildRec(), CVC3::CoreTheoremProducer::rewriteIteFalse(), CVC3::CoreTheoremProducer::rewriteIteSame(), CVC3::CoreTheoremProducer::rewriteIteTrue(), CVC3::DatatypeTheoremProducer::rewriteSelCons(), CVC3::CommonTheoremProducer::rewriteUsingSymmetry(), CVC3::TheoryDatatypeLazy::setup(), CVC3::BitvectorTheoremProducer::signExtendRule(), CVC3::CommonTheoremProducer::symmetryRule(), CVC3::Theory::theoryOf(), CVC3::CommonTheoremProducer::transitivityRule(), CVC3::BitvectorTheoremProducer::typePredBit(), CVC3::VCL::varExpr(), CVC3::BitvectorTheoremProducer::zeroPaddingRule(), and CVC3::Translator::zeroVar().

int CVC3::Type::arity

(

)

const [inline]

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

bool CVC3::Type::isNull

(

)

const [inline]

Definition at line 134 of file type.h.

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::CoreTheoremProducer::rewriteIteFalse(), CVC3::CoreTheoremProducer::rewriteIteSame(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::CoreTheoremProducer::rewriteIteTrue(), CVC3::CommonTheoremProducer::rewriteUsingSymmetry(), and CVC3::CommonTheoremProducer::transitivityRule().

bool CVC3::Type::isBool

(

)

const [inline]

Definition at line 135 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::TheoryQuant::computeType(), CVC3::TheoryCore::computeType(), CVC3::TheoryDatatype::dataType(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::RecordsTheoremProducer::expandNeq(), findPolarity(), 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::TheoryQuant::newTopMatch(), CVC3::Theory::newVar(), CVC3::CoreTheoremProducer::NotToIte(), CVC3::TheoryCore::print(), CVC3::TheoryCore::processUpdates(), CVC3::VCL::query(), CVC3::TheoryQuant::recursiveMap(), CVC3::SearchSimple::restartInternal(), CVC3::SearchEngineFast::restartInternal(), CVC3::TheoryUF::rewrite(), CVC3::CoreTheoremProducer::rewriteIteBool(), CVC3::CoreTheoremProducer::rewriteIteElse(), CVC3::CoreTheoremProducer::rewriteIteFalse(), CVC3::CoreTheoremProducer::rewriteIteSame(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::CoreTheoremProducer::rewriteIteTrue(), CVC3::ArrayTheoremProducer::rewriteReadWrite(), CVC3::ArrayTheoremProducer::rewriteSameStore(), CVC3::ArrayTheoremProducer::rewriteWriteWrite(), CVC3::TheoryQuant::setupTriggers(), 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 136 of file type.h.

bool CVC3::Type::isFunction

(

)

const [inline]

Definition at line 137 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::dataType(), CVC3::TheoryDatatype::getConstant(), and CVC3::Theory::newFunction().

static Type CVC3::Type::typeBool

(

ExprManager *

em

)

[inline, static]

Definition at line 140 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 141 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 457 of file expr.cpp.

References CVC3::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 143 of file type.h.

std::string CVC3::Type::toString

(

)

const [inline]

Definition at line 147 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::TheoryUF::computeType(), CVC3::TheorySimulate::computeType(), CVC3::TheoryQuant::computeType(), CVC3::TheoryCore::computeType(), CVC3::TheoryArray::computeType(), CVC3::TheoryArithOld::computeType(), CVC3::TheoryArithNew::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().

---

Member Data Documentation

Expr CVC3::Type::d_expr [private]

Definition at line 118 of file type.h.

---

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

• type.h
• expr.cpp

---