CVC3
2.4.1
|
Public Member Functions | |
TypeComputerCore (TheoryCore *core) | |
void | computeType (const Expr &e) |
Compute the type of e. More... | |
void | checkType (const Expr &e) |
Check that e is a valid Type expr. More... | |
Cardinality | finiteTypeInfo (Expr &e, Unsigned &n, bool enumerate, bool computeSize) |
Get information related to finiteness of a type. More... | |
![]() | |
TypeComputer () | |
virtual | ~TypeComputer () |
Private Attributes | |
TheoryCore * | d_core |
Definition at line 70 of file theory_core.cpp.
|
inline |
Definition at line 73 of file theory_core.cpp.
|
inlinevirtual |
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().
|
inlinevirtual |
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().
|
inlinevirtual |
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().
|
private |
Definition at line 71 of file theory_core.cpp.