CVC3  2.4.1
Public Member Functions | Private Attributes | List of all members
CVC3::TypeComputerCore Class Reference
Inheritance diagram for CVC3::TypeComputerCore:
CVC3::ExprManager::TypeComputer

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...
 
- Public Member Functions inherited from CVC3::ExprManager::TypeComputer
 TypeComputer ()
 
virtual ~TypeComputer ()
 

Private Attributes

TheoryCored_core
 

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)
inlinevirtual
void CVC3::TypeComputerCore::checkType ( const Expr e)
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().

Cardinality CVC3::TypeComputerCore::finiteTypeInfo ( Expr e,
Unsigned n,
bool  enumerate,
bool  computeSize 
)
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().

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: