diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-07-14 07:33:01 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-14 09:33:01 -0500 |
commit | c13527bfa6b47ff4675b429b5e7bb7c6f43ff595 (patch) | |
tree | f182e942b3bc4ad99a8fdf765959781f1a2570dd /src/expr | |
parent | 1cd3c3c5dad84093aa6b2db164798c8fff473fec (diff) |
Use TypeNode in EmptySet (#4740)
This commit changes EmptySet to use TypeNode instead of Type.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/emptyset.cpp | 21 | ||||
-rw-r--r-- | src/expr/emptyset.h | 37 | ||||
-rw-r--r-- | src/expr/expr_template.cpp | 4 | ||||
-rw-r--r-- | src/expr/node_manager.h | 5 |
4 files changed, 29 insertions, 38 deletions
diff --git a/src/expr/emptyset.cpp b/src/expr/emptyset.cpp index 1c8950b55..6260e4373 100644 --- a/src/expr/emptyset.cpp +++ b/src/expr/emptyset.cpp @@ -17,10 +17,9 @@ #include "expr/emptyset.h" -#include <iosfwd> +#include <iostream> -#include "expr/expr.h" -#include "expr/type.h" +#include "expr/type_node.h" namespace CVC4 { @@ -29,30 +28,24 @@ std::ostream& operator<<(std::ostream& out, const EmptySet& asa) { } size_t EmptySetHashFunction::operator()(const EmptySet& es) const { - return TypeHashFunction()(es.getType()); + return TypeNodeHashFunction()(es.getType()); } /** * Constructs an emptyset of the specified type. Note that the argument * is the type of the set itself, NOT the type of the elements. */ -EmptySet::EmptySet(const SetType& setType) - : d_type(new SetType(setType)) -{ } +EmptySet::EmptySet(const TypeNode& setType) : d_type(new TypeNode(setType)) {} -EmptySet::EmptySet(const EmptySet& es) - : d_type(new SetType(es.getType())) -{ } +EmptySet::EmptySet(const EmptySet& es) : d_type(new TypeNode(es.getType())) {} EmptySet& EmptySet::operator=(const EmptySet& es) { (*d_type) = es.getType(); return *this; } -EmptySet::~EmptySet() { delete d_type; } -const SetType& EmptySet::getType() const { - return *d_type; -} +EmptySet::~EmptySet() {} +const TypeNode& EmptySet::getType() const { return *d_type; } bool EmptySet::operator==(const EmptySet& es) const { return getType() == es.getType(); diff --git a/src/expr/emptyset.h b/src/expr/emptyset.h index 55e07747e..1b5bc6897 100644 --- a/src/expr/emptyset.h +++ b/src/expr/emptyset.h @@ -17,33 +17,29 @@ #include "cvc4_public.h" -#pragma once +#ifndef CVC4__EMPTY_SET_H +#define CVC4__EMPTY_SET_H #include <iosfwd> +#include <memory> namespace CVC4 { - // messy; Expr needs EmptySet (because it's the payload of a - // CONSTANT-kinded expression), EmptySet needs SetType, and - // SetType needs Expr. Using a forward declaration here in - // order to break the build cycle. - // Uses of SetType need to be as an incomplete type throughout - // this header. - class SetType; -}/* CVC4 namespace */ -namespace CVC4 { -class CVC4_PUBLIC EmptySet { +class TypeNode; + +class CVC4_PUBLIC EmptySet +{ public: /** * Constructs an emptyset of the specified type. Note that the argument * is the type of the set itself, NOT the type of the elements. */ - EmptySet(const SetType& setType); + EmptySet(const TypeNode& setType); ~EmptySet(); EmptySet(const EmptySet& other); EmptySet& operator=(const EmptySet& other); - const SetType& getType() const; + const TypeNode& getType() const; bool operator==(const EmptySet& es) const; bool operator!=(const EmptySet& es) const; bool operator<(const EmptySet& es) const; @@ -52,17 +48,18 @@ class CVC4_PUBLIC EmptySet { bool operator>=(const EmptySet& es) const; private: - /** Pointer to the SetType node. This is never NULL. */ - SetType* d_type; - EmptySet(); -};/* class EmptySet */ + std::unique_ptr<TypeNode> d_type; +}; /* class EmptySet */ std::ostream& operator<<(std::ostream& out, const EmptySet& es) CVC4_PUBLIC; -struct CVC4_PUBLIC EmptySetHashFunction { +struct CVC4_PUBLIC EmptySetHashFunction +{ size_t operator()(const EmptySet& es) const; -};/* struct EmptySetHashFunction */ +}; /* struct EmptySetHashFunction */ + +} // namespace CVC4 -}/* CVC4 namespace */ +#endif /* CVC4__EMPTY_SET_H */ diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 132d4bfaa..226736e8f 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -181,8 +181,8 @@ private: if(n.getMetaKind() == metakind::CONSTANT) { if(n.getKind() == kind::EMPTYSET) { Type type = d_from->exportType( - n.getConst< ::CVC4::EmptySet>().getType(), d_to, d_vmap); - return d_to->mkConst(::CVC4::EmptySet(type)); + n.getConst< ::CVC4::EmptySet>().getType().toType(), d_to, d_vmap); + return d_to->mkConst(::CVC4::EmptySet(TypeNode::fromType(type))); } return exportConstant(n, NodeManager::fromExprManager(d_to), d_vmap); } else if(n.getMetaKind() == metakind::NULLARY_OPERATOR ){ diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 499cba457..1a28a16eb 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -959,7 +959,7 @@ public: /** * Convert a type node to a type. */ - inline Type toType(TypeNode tn); + inline Type toType(const TypeNode& tn); /** * Convert a type to a type node. @@ -1184,7 +1184,8 @@ inline NodeManager* NodeManager::fromExprManager(ExprManager* exprManager) { return exprManager->getNodeManager(); } -inline Type NodeManager::toType(TypeNode tn) { +inline Type NodeManager::toType(const TypeNode& tn) +{ return Type(this, new TypeNode(tn)); } |