19 #ifndef __CVC4__TYPE_H 20 #define __CVC4__TYPE_H 43 template <
bool ref_count>
54 class ConstructorType;
62 class SortConstructorType;
93 friend class NodeManager;
94 friend class TypeNode;
111 Type makeType(
const TypeNode& typeNode)
const;
118 Type(NodeManager* em, TypeNode* typeNode);
151 bool isWellFounded()
const;
157 Expr mkGroundTerm()
const;
162 bool isSubtypeOf(
Type t)
const;
168 bool isComparableTo(
Type t)
const;
173 Type getBaseType()
const;
178 Type substitute(
const Type& type,
const Type& replacement)
const;
183 Type substitute(
const std::vector<Type>& types,
184 const std::vector<Type>& replacements)
const;
220 bool operator<(
const Type& t)
const;
225 bool operator<=(
const Type& t)
const;
230 bool operator>(
const Type& t)
const;
235 bool operator>=(
const Type& t)
const;
241 bool isBoolean()
const;
247 bool isInteger()
const;
259 bool isString()
const;
265 bool isBitVector()
const;
271 bool isFunction()
const;
278 bool isPredicate()
const;
284 bool isTuple()
const;
290 bool isRecord()
const;
296 bool isSExpr()
const;
302 bool isArray()
const;
314 bool isDatatype()
const;
320 bool isConstructor()
const;
326 bool isSelector()
const;
332 bool isTester()
const;
344 bool isSortConstructor()
const;
357 bool isSubrange()
const;
363 void toStream(std::ostream& out)
const;
368 std::string toString()
const;
426 size_t getArity()
const;
429 std::vector<Type> getArgTypes()
const;
432 Type getRangeType()
const;
446 size_t getLength()
const;
449 std::vector<Type> getTypes()
const;
464 const Record& getRecord()
const;
478 std::vector<Type> getTypes()
const;
492 Type getIndexType()
const;
495 Type getConstituentType()
const;
509 Type getElementType()
const;
523 std::string getName()
const;
526 bool isParameterized()
const;
529 std::vector<Type> getParamTypes()
const;
544 std::string getName()
const;
547 size_t getArity()
const;
550 SortType instantiate(
const std::vector<Type>& params)
const;
559 class CVC4_PUBLIC PredicateSubtype :
public Type {
567 Expr getPredicate()
const;
573 Type getParentType()
const;
607 unsigned getSize()
const;
623 const Datatype& getDatatype()
const;
626 bool isParametric()
const;
632 Expr getConstructor(std::string name)
const;
640 bool isInstantiated()
const;
645 bool isParameterInstantiated(
unsigned n)
const;
648 std::vector<Type> getParamTypes()
const;
651 size_t getArity()
const;
654 DatatypeType instantiate(
const std::vector<Type>& params)
const;
672 std::vector<Type> getArgTypes()
const;
675 size_t getArity()
const;
694 Type getRangeType()
const;
Singleton class encapsulating the real type.
Class encapsulating the Selector type.
Class encapsulating CVC4 expressions and methods for constructing new expressions.
Singleton class encapsulating the integer type.
Class encapsulating a user-defined sort.
Class encapsulating an set type.
Class encapsulating a tuple type.
The representation of an inductive datatype.
A simple representation of a cardinality.
Class encapsulating CVC4 expression types.
static TypeNode * getTypeNode(const Type &t)
Accessor for derived classes.
TypeNode * d_typeNode
The internal expression representation.
Class encapsulating the Tester type.
Singleton class encapsulating the Boolean type.
Representation of subrange bounds.
Representation of cardinality.
Class encapsulating an array type.
Class encapsulating a function type.
std::ostream & operator<<(std::ostream &out, TypeConstant typeConstant)
Class encapsulating a user-defined sort constructor.
Class encapsulating the datatype type.
Macros that should be defined everywhere during the building of the libraries and driver binary...
Class encapsulating a record type.
NodeManager * d_nodeManager
The responsible expression manager.
TypeNode exportTypeInternal(TypeNode n, NodeManager *from, NodeManager *nm, ExprManagerMapCollection &vmap)
Class encapsulating a tuple type.
Singleton class encapsulating the string type.
struct CVC4::options::out__option_t out
Class encapsulating an integer subrange type.
Class encapsulating the constructor type.
Class encapsulating the bit-vector type.
bool operator!=(enum Result::Sat s, const Result &r)
bool operator==(enum Result::Sat s, const Result &r)