Inherits CVC3::ExprManager::TypeComputer.
Public Member Functions
- TypeComputerCore (TheoryCore *core)
- void computeType (const Expr &e)
- void checkType (const Expr &e)
- Check that e is a valid Type expr.
- Check that e is a valid Type expr.
- Cardinality finiteTypeInfo (Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Private Attributes
Detailed Description
Definition at line 70 of file theory_core.cpp.
Constructor & Destructor Documentation
| CVC3::TypeComputerCore::TypeComputerCore | ( | TheoryCore * | core | ) | [inline] |
Definition at line 73 of file theory_core.cpp.
Member Function Documentation
| 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().
Member Data Documentation
TheoryCore* CVC3::TypeComputerCore::d_core [private] |
Definition at line 71 of file theory_core.cpp.
The documentation for this class was generated from the following file:
