CVC3
|
Inherits CVC3::ExprManager::TypeComputer.
Definition at line 70 of file theory_core.cpp.
CVC3::TypeComputerCore::TypeComputerCore | ( | TheoryCore * | core | ) | [inline] |
Definition at line 73 of file theory_core.cpp.
void CVC3::TypeComputerCore::computeType | ( | const Expr & | e | ) | [inline, virtual] |
Compute the type of e.
Implements CVC3::ExprManager::TypeComputer.
Definition at line 74 of file theory_core.cpp.
References CVC3::Theory::computeType(), DebugAssert, CVC3::Type::getExpr(), CVC3::Expr::getKind(), CVC3::Expr::isApply(), CVC3::Expr::isNull(), CVC3::Expr::isVar(), CVC3::Expr::lookupType(), CVC3::Theory::theoryOf(), and CVC3::Expr::toString().
void CVC3::TypeComputerCore::checkType | ( | const Expr & | e | ) | [inline, virtual] |
Check that e is a valid Type expr.
Implements CVC3::ExprManager::TypeComputer.
Definition at line 82 of file theory_core.cpp.
References CVC3::Expr::isType(), CVC3::Expr::setValidType(), and CVC3::Expr::toString().
Cardinality CVC3::TypeComputerCore::finiteTypeInfo | ( | Expr & | e, |
Unsigned & | n, | ||
bool | enumerate, | ||
bool | computeSize | ||
) | [inline, virtual] |
Get information related to finiteness of a type.
Implements CVC3::ExprManager::TypeComputer.
Definition at line 89 of file theory_core.cpp.
References DebugAssert, and CVC3::Expr::isType().
TheoryCore* CVC3::TypeComputerCore::d_core [private] |
Definition at line 71 of file theory_core.cpp.