/********************* */
/*! \file type.h
** \verbatim
- ** Original author: cconway
- ** Major contributors: dejan, mdeters
- ** Minor contributors (to current version): ajreynol
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Top contributors (to current version):
+ ** Morgan Deters, Dejan Jovanovic, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** 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
**
** \brief Interface for expression types.
**
#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"
-#include "util/subrange_bound.h"
namespace CVC4 {
class CVC4_PUBLIC SmtEngine;
class CVC4_PUBLIC Datatype;
-class CVC4_PUBLIC Record;
+class Record;
template <bool ref_count>
class NodeTemplate;
class IntegerType;
class RealType;
class StringType;
+class RegExpType;
+class RoundingModeType;
class BitVectorType;
class ArrayType;
+class SetType;
class DatatypeType;
class ConstructorType;
class SelectorType;
class TesterType;
class FunctionType;
-class TupleType;
-class RecordType;
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 isString() const;
+ /**
+ * Is this the regexp type?
+ * @return true if the type is the regexp type
+ */
+ bool isRegExp() const;
+
+ /**
+ * Is this the rounding mode type?
+ * @return true if the type is the rounding mode type
+ */
+ bool isRoundingMode() const;
+
/**
* Is this the bit-vector type?
* @return true if the type is a bit-vector type
*/
bool isBitVector() const;
+ /**
+ * Is this the floating-point type?
+ * @return true if the type is a floating-point type
+ */
+ bool isFloatingPoint() const;
+
/**
* Is this a function type?
* @return true if the type is a function type
*/
bool isArray() const;
+ /**
+ * Is this a Set type?
+ * @return true if the type is a Set 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
* Is this an integer subrange type?
* @return true if this is an integer subrange type
*/
- bool isSubrange() const;
+ //bool isSubrange() const;
/**
* Outputs a string representation of this type to the stream.
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 */
-/**
- * Class encapsulating a function type.
- */
-class CVC4_PUBLIC FunctionType : public Type {
+/** Singleton class encapsulating the string type. */
+class CVC4_PUBLIC RegExpType : public Type {
+ public:
+ /** Construct from the base type */
+ RegExpType(const Type& type);
+};/* class RegExpType */
-public:
+/** Singleton class encapsulating the rounding mode type. */
+class CVC4_PUBLIC RoundingModeType : public Type {
+ public:
+ /** Construct from the base type */
+ RoundingModeType(const Type& type = Type());
+};/* class RoundingModeType */
+/** Class encapsulating a function type. */
+class CVC4_PUBLIC FunctionType : public Type {
+ 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;
/** Get the argument types */
std::vector<Type> getArgTypes() const;
Type getRangeType() const;
};/* class FunctionType */
-/**
- * Class encapsulating a tuple type.
- */
-class CVC4_PUBLIC TupleType : public Type {
-
-public:
-
- /** Construct from the base type */
- TupleType(const Type& type = Type()) throw(IllegalArgumentException);
-
- /** Get the length of the tuple. The same as getTypes().size(). */
- size_t getLength() const;
-
- /** Get the constituent types */
- std::vector<Type> getTypes() const;
-
-};/* class TupleType */
-
-/**
- * Class encapsulating a record type.
- */
-class CVC4_PUBLIC RecordType : public Type {
-
-public:
-
- /** Construct from the base type */
- RecordType(const Type& type = Type()) throw(IllegalArgumentException);
-
- /** Get the constituent types */
- const Record& getRecord() const;
-};/* class RecordType */
-
-/**
- * Class encapsulating a tuple 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 a user-defined sort.
- */
-class CVC4_PUBLIC SortType : public Type {
+/** Class encapsulating a set type. */
+class CVC4_PUBLIC SetType : public Type {
+ public:
+ /** Construct from the base type */
+ SetType(const Type& type = Type());
+
+ /** Get the element type */
+ Type getElementType() const;
+}; /* class SetType */
-public:
+/** Class encapsulating a sequence type. */
+class CVC4_PUBLIC SequenceType : public Type
+{
+ public:
+ /** Construct from the base type */
+ SequenceType(const Type& type = Type());
+ /** Get the element type */
+ Type getElementType() const;
+}; /* class SetType */
+
+/** Class encapsulating a user-defined sort. */
+class CVC4_PUBLIC SortType : public Type {
+ 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 an integer subrange type.
- */
-class CVC4_PUBLIC SubrangeType : public Type {
-
-public:
-
- /** Construct from the base type */
- SubrangeType(const Type& type = Type()) throw(IllegalArgumentException);
-
- /** Get the bounds defining this integer subrange */
- SubrangeBounds getSubrangeBounds() const;
-
-};/* class SubrangeType */
-
-/**
- * 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 CVC4_PUBLIC FloatingPointType : public Type {
+ public:
+ /** Construct from the base type */
+ FloatingPointType(const Type& type = Type());
-/**
- * Class encapsulating the datatype type
- */
-class CVC4_PUBLIC DatatypeType : public Type {
+ /**
+ * Returns the size of the floating-point exponent type.
+ * @return the width of the floating-point exponent type (> 0)
+ */
+ unsigned getExponentSize() const;
+
+ /**
+ * Returns the size of the floating-point significand type.
+ * @return the width of the floating-point significand type (> 0)
+ */
+ unsigned getSignificandSize() const;
-public:
+};/* class FloatingPointType */
+/** Class encapsulating the datatype type */
+class CVC4_PUBLIC DatatypeType : public Type {
+ 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 */
/** Instantiate a datatype using this datatype constructor */
DatatypeType instantiate(const std::vector<Type>& params) const;
-};/* class DatatypeType */
+ /** Get the length of a tuple type */
+ size_t getTupleLength() const;
-/**
- * Class encapsulating the constructor type
- */
-class CVC4_PUBLIC ConstructorType : public Type {
+ /** Get the constituent types of a tuple type */
+ std::vector<Type> getTupleTypes() const;
-public:
+};/* class DatatypeType */
+/** Class encapsulating the constructor type. */
+class CVC4_PUBLIC ConstructorType : public Type {
+ 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 */
projects / cvc5.git / blobdiff