diff options
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r-- | src/expr/node_manager.h | 52 |
1 files changed, 28 insertions, 24 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index cbfcdd110..39c1c91b9 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -311,10 +311,6 @@ public: template <class NodeClass, class T> NodeClass mkConstInternal(const T&); - /** Create a type-variable */ - TypeNode mkTypeVar(); - TypeNode mkTypeVar(const std::string& name); - /** Create a node with no children. */ TypeNode mkTypeNode(Kind kind, const std::vector<TypeNode>& children); @@ -446,9 +442,15 @@ public: const AttrKind& attr, const typename AttrKind::value_type& value); - /** Get the (singleton) type for booleans. */ + /** Get the (singleton) type for Booleans. */ inline TypeNode booleanType(); + /** Get the (singleton) type for integers. */ + inline TypeNode integerType(); + + /** Get the (singleton) type for booleans. */ + inline TypeNode realType(); + /** Get the (singleton) type for sorts. */ inline TypeNode kindType(); @@ -607,6 +609,16 @@ inline TypeNode NodeManager::booleanType() { return TypeNode(mkTypeConst<TypeConstant>(BOOLEAN_TYPE)); } +/** Get the (singleton) type for integers. */ +inline TypeNode NodeManager::integerType() { + return TypeNode(mkTypeConst<TypeConstant>(INTEGER_TYPE)); +} + +/** Get the (singleton) type for reals. */ +inline TypeNode NodeManager::realType() { + return TypeNode(mkTypeConst<TypeConstant>(REAL_TYPE)); +} + /** Get the (singleton) type for sorts. */ inline TypeNode NodeManager::kindType() { return TypeNode(mkTypeConst<TypeConstant>(KIND_TYPE)); @@ -648,14 +660,6 @@ NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) { return mkTypeNode(kind::FUNCTION_TYPE, sortNodes); } -inline TypeNode NodeManager::mkSort() { - return mkTypeVar(); -} - -inline TypeNode NodeManager::mkSort(const std::string& name) { - return mkTypeVar(name); -} - inline TypeNode NodeManager::getType(TNode n) { TypeNode typeNode; getAttribute(n, TypeAttr(), typeNode); @@ -749,6 +753,17 @@ inline bool NodeManager::hasOperator(Kind k) { } } +inline TypeNode NodeManager::mkSort() { + TypeNode type = NodeBuilder<0>(this, kind::VARIABLE).constructTypeNode(); + return type; +} + +inline TypeNode NodeManager::mkSort(const std::string& name) { + TypeNode type = mkSort(); + type.setAttribute(expr::VarNameAttr(), name); + return type; +} + inline Node NodeManager::mkNode(Kind kind) { return NodeBuilder<0>(this, kind); } @@ -854,17 +869,6 @@ inline Node NodeManager::mkVar(const TypeNode& type) { return n; } -inline TypeNode NodeManager::mkTypeVar(const std::string& name) { - TypeNode type = mkTypeVar(); - type.setAttribute(expr::VarNameAttr(), name); - return type; -} - -inline TypeNode NodeManager::mkTypeVar() { - TypeNode type = NodeBuilder<0>(this, kind::VARIABLE).constructTypeNode(); - return type; -} - inline Node* NodeManager::mkVarPtr(const TypeNode& type) { Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr(); n->setAttribute(TypeAttr(), type); |