/*! \file type.h
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Dejan Jovanovic, Martin Brain
+ ** Morgan Deters, Dejan Jovanovic, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
#include "cvc4_public.h"
-#ifndef __CVC4__TYPE_H
-#define __CVC4__TYPE_H
+#ifndef CVC4__TYPE_H
+#define CVC4__TYPE_H
+#include <climits>
+#include <cstdint>
#include <string>
#include <vector>
-#include <limits.h>
-#include <stdint.h>
#include "util/cardinality.h"
class SExprType;
class SortType;
class SortConstructorType;
-// not in release 1.0
-//class PredicateSubtype;
-class SubrangeType;
class Type;
/** Hash function for Types */
Type(NodeManager* em, TypeNode* typeNode);
/** Accessor for derived classes */
- static TypeNode* getTypeNode(const Type& t) throw() { return t.d_typeNode; }
-
-public:
-
+ static TypeNode* getTypeNode(const Type& t) { return t.d_typeNode; }
+ public:
/** Force a virtual destructor for safety. */
virtual ~Type();
*/
Cardinality getCardinality() const;
+ /**
+ * Is this type finite? This assumes uninterpreted sorts have infinite
+ * cardinality.
+ */
+ bool isFinite() const;
+
+ /**
+ * Is this type interpreted as being finite.
+ * If finite model finding is enabled, this assumes all uninterpreted sorts
+ * are interpreted as finite.
+ */
+ bool isInterpretedFinite() const;
+
/**
* Is this a well-founded type?
*/
bool isWellFounded() const;
+ /**
+ * Is this a first-class type?
+ *
+ * First-class types are types for which:
+ * (1) we handle equalities between terms of that type, and
+ * (2) they are allowed to be parameters of parametric types (e.g. index or
+ * element types of arrays).
+ *
+ * Examples of types that are not first-class include constructor types,
+ * selector types, tester types, regular expressions and SExprs.
+ */
+ bool isFirstClass() const;
+
+ /**
+ * Is this a function-LIKE type?
+ *
+ * Anything function-like except arrays (e.g., datatype selectors) is
+ * considered a function here. Function-like terms can not be the argument
+ * or return value for any term that is function-like.
+ * This is mainly to avoid higher order.
+ *
+ * Note that arrays are explicitly not considered function-like here.
+ *
+ * @return true if this is a function-like type
+ */
+ bool isFunctionLike() const;
+
/**
* Construct and return a ground term for this Type. Throws an
* exception if this type is not well-founded.
*/
Expr mkGroundTerm() const;
+ /**
+ * Construct and return a ground value for this Type. Throws an
+ * exception if this type is not well-founded.
+ *
+ * This is the same as mkGroundTerm, but constructs a constant value instead
+ * of a canonical ground term. These two notions typically coincide. However,
+ * for uninterpreted sorts, they do not: mkGroundTerm returns a fresh variable
+ * whereas mkValue returns an uninterpreted constant. The motivation for
+ * mkGroundTerm is that unintepreted constants should never appear in lemmas.
+ * The motivation for mkGroundValue is for e.g. type enumeration and model
+ * construction.
+ */
+ Expr mkGroundValue() const;
+
/**
* Is this type a subtype of the given type?
*/
*/
bool isSet() const;
- /**
+ /**
+ * Is this a Sequence type?
+ * @return true if the type is a Sequence type
+ */
+ bool isSequence() const;
+
+ /**
* Is this a datatype type?
* @return true if the type is a datatype type
*/
std::string toString() const;
};/* class Type */
-/**
- * Singleton class encapsulating the Boolean type.
- */
+/** Singleton class encapsulating the Boolean type. */
class CVC4_PUBLIC BooleanType : public Type {
-
-public:
-
+ public:
/** Construct from the base type */
- BooleanType(const Type& type = Type()) throw(IllegalArgumentException);
+ BooleanType(const Type& type = Type());
};/* class BooleanType */
-/**
- * Singleton class encapsulating the integer type.
- */
+/** Singleton class encapsulating the integer type. */
class CVC4_PUBLIC IntegerType : public Type {
-
-public:
-
+ public:
/** Construct from the base type */
- IntegerType(const Type& type = Type()) throw(IllegalArgumentException);
+ IntegerType(const Type& type = Type());
};/* class IntegerType */
-/**
- * Singleton class encapsulating the real type.
- */
+/** Singleton class encapsulating the real type. */
class CVC4_PUBLIC RealType : public Type {
-
-public:
-
+ public:
/** Construct from the base type */
- RealType(const Type& type = Type()) throw(IllegalArgumentException);
+ RealType(const Type& type = Type());
};/* class RealType */
-/**
- * Singleton class encapsulating the string type.
- */
+/** Singleton class encapsulating the string type. */
class CVC4_PUBLIC StringType : public Type {
-
-public:
-
+ public:
/** Construct from the base type */
- StringType(const Type& type) throw(IllegalArgumentException);
+ StringType(const Type& type);
};/* class StringType */
-/**
- * Singleton class encapsulating the string type.
- */
+/** Singleton class encapsulating the string type. */
class CVC4_PUBLIC RegExpType : public Type {
-
-public:
-
+ public:
/** Construct from the base type */
- RegExpType(const Type& type) throw(IllegalArgumentException);
+ RegExpType(const Type& type);
};/* class RegExpType */
-
-/**
- * Singleton class encapsulating the rounding mode type.
- */
+/** Singleton class encapsulating the rounding mode type. */
class CVC4_PUBLIC RoundingModeType : public Type {
-
-public:
-
+ public:
/** Construct from the base type */
- RoundingModeType(const Type& type = Type()) throw(IllegalArgumentException);
+ RoundingModeType(const Type& type = Type());
};/* class RoundingModeType */
-
-
-/**
- * Class encapsulating a function type.
- */
+/** Class encapsulating a function type. */
class CVC4_PUBLIC FunctionType : public Type {
-
-public:
-
+ public:
/** Construct from the base type */
- FunctionType(const Type& type = Type()) throw(IllegalArgumentException);
+ FunctionType(const Type& type = Type());
/** Get the arity of the function type */
size_t getArity() const;
Type getRangeType() const;
};/* class FunctionType */
-/**
- * Class encapsulating a sexpr type.
- */
+/** Class encapsulating a sexpr type. */
class CVC4_PUBLIC SExprType : public Type {
-
-public:
-
+ public:
/** Construct from the base type */
- SExprType(const Type& type = Type()) throw(IllegalArgumentException);
+ SExprType(const Type& type = Type());
/** Get the constituent types */
std::vector<Type> getTypes() const;
};/* class SExprType */
-/**
- * Class encapsulating an array type.
- */
+/** Class encapsulating an array type. */
class CVC4_PUBLIC ArrayType : public Type {
-
-public:
-
+ public:
/** Construct from the base type */
- ArrayType(const Type& type = Type()) throw(IllegalArgumentException);
+ ArrayType(const Type& type = Type());
/** Get the index type */
Type getIndexType() const;
Type getConstituentType() const;
};/* class ArrayType */
-/**
- * Class encapsulating an set type.
- */
+/** Class encapsulating a set type. */
class CVC4_PUBLIC SetType : public Type {
+ public:
+ /** Construct from the base type */
+ SetType(const Type& type = Type());
-public:
+ /** Get the element type */
+ Type getElementType() const;
+}; /* class SetType */
+/** Class encapsulating a sequence type. */
+class CVC4_PUBLIC SequenceType : public Type
+{
+ public:
/** Construct from the base type */
- SetType(const Type& type = Type()) throw(IllegalArgumentException);
+ SequenceType(const Type& type = Type());
- /** Get the index type */
+ /** Get the element type */
Type getElementType() const;
-};/* class SetType */
+}; /* class SetType */
-/**
- * Class encapsulating a user-defined sort.
- */
+/** Class encapsulating a user-defined sort. */
class CVC4_PUBLIC SortType : public Type {
-
-public:
-
+ public:
/** Construct from the base type */
- SortType(const Type& type = Type()) throw(IllegalArgumentException);
+ SortType(const Type& type = Type());
/** Get the name of the sort */
std::string getName() const;
};/* class SortType */
-/**
- * Class encapsulating a user-defined sort constructor.
- */
+/** Class encapsulating a user-defined sort constructor. */
class CVC4_PUBLIC SortConstructorType : public Type {
-
-public:
-
+ public:
/** Construct from the base type */
- SortConstructorType(const Type& type = Type()) throw(IllegalArgumentException);
+ SortConstructorType(const Type& type = Type());
/** Get the name of the sort constructor */
std::string getName() const;
};/* class SortConstructorType */
-// not in release 1.0
-#if 0
-/**
- * Class encapsulating a predicate subtype.
- */
-class CVC4_PUBLIC PredicateSubtype : public Type {
-
-public:
-
- /** Construct from the base type */
- PredicateSubtype(const Type& type = Type()) throw(IllegalArgumentException);
-
- /** Get the LAMBDA defining this predicate subtype */
- Expr getPredicate() const;
-
- /**
- * Get the parent type of this predicate subtype; note that this
- * could be another predicate subtype.
- */
- Type getParentType() const;
-
-};/* class PredicateSubtype */
-#endif /* 0 */
-
-/**
- * Class encapsulating the bit-vector type.
- */
+/** Class encapsulating the bit-vector type. */
class CVC4_PUBLIC BitVectorType : public Type {
-
-public:
-
+ public:
/** Construct from the base type */
- BitVectorType(const Type& type = Type()) throw(IllegalArgumentException);
+ BitVectorType(const Type& type = Type());
/**
* Returns the size of the bit-vector type.
};/* class BitVectorType */
-
-/**
- * Class encapsulating the floating point type.
- */
+/** Class encapsulating the floating point type. */
class CVC4_PUBLIC FloatingPointType : public Type {
-
-public:
-
+ public:
/** Construct from the base type */
- FloatingPointType(const Type& type = Type()) throw(IllegalArgumentException);
+ FloatingPointType(const Type& type = Type());
/**
* Returns the size of the floating-point exponent type.
};/* class FloatingPointType */
-
-/**
- * Class encapsulating the datatype type
- */
+/** Class encapsulating the datatype type */
class CVC4_PUBLIC DatatypeType : public Type {
-
-public:
-
+ public:
/** Construct from the base type */
- DatatypeType(const Type& type = Type()) throw(IllegalArgumentException);
+ DatatypeType(const Type& type = Type());
/** Get the underlying datatype */
const Datatype& getDatatype() const;
/** Is this datatype parametric? */
bool isParametric() const;
-
- /**
- * Get the constructor operator associated to the given constructor
- * name in this datatype.
- */
- Expr getConstructor(std::string name) const;
-
/**
* Has this datatype been fully instantiated ?
*
*/
bool isInstantiated() const;
- /**
- * Has this datatype been instantiated for parameter N ?
- */
+ /** Has this datatype been instantiated for parameter `n` ? */
bool isParameterInstantiated(unsigned n) const;
/** Get the parameter types */
/** Get the constituent types of a tuple type */
std::vector<Type> getTupleTypes() const;
- /** Get the description of the record type */
- const Record& getRecord() const;
-
};/* class DatatypeType */
-/**
- * Class encapsulating the constructor type
- */
+/** Class encapsulating the constructor type. */
class CVC4_PUBLIC ConstructorType : public Type {
-
-public:
-
+ public:
/** Construct from the base type */
- ConstructorType(const Type& type = Type()) throw(IllegalArgumentException);
+ ConstructorType(const Type& type = Type());
/** Get the range type */
DatatypeType getRangeType() const;
};/* class ConstructorType */
-
-/**
- * Class encapsulating the Selector type
- */
+/** Class encapsulating the Selector type. */
class CVC4_PUBLIC SelectorType : public Type {
-
-public:
-
+ public:
/** Construct from the base type */
- SelectorType(const Type& type = Type()) throw(IllegalArgumentException);
+ SelectorType(const Type& type = Type());
/** Get the domain type for this selector (the datatype type) */
DatatypeType getDomain() const;
};/* class SelectorType */
-/**
- * Class encapsulating the Tester type
- */
+/** Class encapsulating the Tester type. */
class CVC4_PUBLIC TesterType : public Type {
-
-public:
-
+ public:
/** Construct from the base type */
- TesterType(const Type& type = Type()) throw(IllegalArgumentException);
+ TesterType(const Type& type = Type());
/** Get the type that this tester tests (the datatype type) */
DatatypeType getDomain() const;
}/* CVC4 namespace */
-#endif /* __CVC4__TYPE_H */
+#endif /* CVC4__TYPE_H */