Definition at line 74 of file theory_core.cpp.
|
Definition at line 77 of file theory_core.cpp. |
|
Compute the type of e.
Implements CVCL::ExprManager::TypeComputer. Definition at line 78 of file theory_core.cpp. References CVCL::Theory::computeType(), d_core, CVCL::Theory::getEM(), CVCL::Type::getExpr(), CVCL::Expr::getKind(), CVCL::ExprManager::getKindName(), CVCL::Theory::getName(), CVCL::Expr::getType(), CVCL::Expr::isApply(), CVCL::Expr::isNull(), CVCL::Expr::isVar(), CVCL::Expr::lookupType(), CVCL::Theory::theoryOf(), CVCL::Expr::toString(), and CVCL::TRACE. |
|
Check that e is a valid Type expr.
Implements CVCL::ExprManager::TypeComputer. Definition at line 88 of file theory_core.cpp. References CVCL::Theory::checkType(), d_core, CVCL::Expr::isType(), CVCL::Theory::theoryOf(), and CVCL::Expr::toString(). |
|
Definition at line 75 of file theory_core.cpp. Referenced by checkType(), and computeType(). |