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.
  

• Cardinality finiteTypeInfo (Expr &e, Unsigned &n, bool enumerate, bool computeSize)

  Get information related to finiteness of a type.
  

Private Attributes

• TheoryCore * d_core

---

Detailed Description

Definition at line 69 of file theory_core.cpp.

---

Constructor & Destructor Documentation

CVC3::TypeComputerCore::TypeComputerCore

(

TheoryCore *

core

)

[inline]

Definition at line 72 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::ExprManager::TypeComputer.

Definition at line 73 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::ExprManager::TypeComputer.

Definition at line 81 of file theory_core.cpp.

References CVC3::Theory::checkType(), d_core, CVC3::Expr::isType(), CVC3::Expr::setValidType(), CVC3::Theory::theoryOf(), 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::ExprManager::TypeComputer.

Definition at line 88 of file theory_core.cpp.

References d_core, DebugAssert, CVC3::Theory::finiteTypeInfo(), CVC3::Expr::isType(), and CVC3::Theory::theoryOf().

---

Member Data Documentation

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

Definition at line 70 of file theory_core.cpp.

Referenced by checkType(), computeType(), and finiteTypeInfo().

---

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

• theory_core.cpp