theory_datatype.h File Reference

#include "theory.h"
#include "smartcdo.h"
#include "cdmap.h"

Go to the source code of this file.

Classes

• class CVC3::TheoryDatatype

  This theory handles datatypes. More...
  

Namespaces

• namespace CVC3

Enumerations

• enum CVC3::DatatypeKinds {
    CVC3::DATATYPE_DECL = 600, CVC3::DATATYPE, CVC3::CONSTRUCTOR, CVC3::SELECTOR,
    CVC3::TESTER
  }

  Local kinds for datatypes.

  More...
  

Functions

• bool CVC3::isDatatype (const Type &t)
• bool CVC3::isConstructor (const Expr &e)
• bool CVC3::isSelector (const Expr &e)
• bool CVC3::isTester (const Expr &e)
• Expr CVC3::getConstructor (const Expr &e)

---

Detailed Description

Author: Clark Barrett

Created: Wed Dec 1 22:24:32 2004

---

License to use, copy, modify, sell and/or distribute this software and its documentation for any purpose is hereby granted without royalty, subject to the terms and conditions defined in the LICENSE file provided with this distribution.

---

Definition in file theory_datatype.h.