CVC3::TypeComputerCore Class Reference

Inheritance diagram for CVC3::TypeComputerCore:

[legend]Collaboration diagram for CVC3::TypeComputerCore:

[legend]List of all members.

Public Member Functions

• TypeComputerCore (TheoryCore *core)
• void computeType (const Expr &e)

  Compute the type of e.
  

• void checkType (const Expr &e)

  Check that e is a valid Type expr.
  

Private Attributes

• TheoryCore * d_core

---

Detailed Description

Definition at line 68 of file theory_core.cpp.

---

Constructor & Destructor Documentation

CVC3::TypeComputerCore::TypeComputerCore

(

TheoryCore *

core

)

[inline]

Definition at line 71 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 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().

---

Member Data Documentation

TheoryCore* CVC3::TypeComputerCore::d_core [private]

Definition at line 69 of file theory_core.cpp.

Referenced by checkType(), and computeType().

---

The documentation for this class was generated from the following file:

• theory_core.cpp

---