Definition at line 68 of file theory_core.cpp.
CVC3::TypeComputerCore::TypeComputerCore | ( | TheoryCore * | core | ) | [inline] |
Definition at line 71 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 72 of file theory_core.cpp.
References CVC3::Theory::computeType(), d_core, 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 80 of file theory_core.cpp.
References CVC3::Theory::checkType(), d_core, CVC3::Expr::isType(), CVC3::Theory::theoryOf(), and CVC3::Expr::toString().
TheoryCore* CVC3::TypeComputerCore::d_core [private] |