Use TypeNode in UninterpretedConstant (#4748)

This commit changes UninterpretedConstant to use TypeNode instead of
Type.

9 files changed, 87 insertions, 50 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index fcf0c028e..c4ba701b9 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -3596,7 +3596,7 @@ Term Solver::mkUninterpretedConst(Sort sort, int32_t index) const
   CVC4_API_SOLVER_CHECK_SORT(sort);
 
   return mkValHelper<CVC4::UninterpretedConstant>(
-      CVC4::UninterpretedConstant(*sort.d_type, index));
+      CVC4::UninterpretedConstant(TypeNode::fromType(*sort.d_type), index));
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
diff --git a/src/expr/uninterpreted_constant.cpp b/src/expr/uninterpreted_constant.cpp
index 2b66a3b7a..c9cbcba20 100644
--- a/src/expr/uninterpreted_constant.cpp
+++ b/src/expr/uninterpreted_constant.cpp
@@ -22,18 +22,57 @@
 #include <string>
 
 #include "base/check.h"
+#include "expr/type_node.h"
 
 using namespace std;
 
 namespace CVC4 {
 
-UninterpretedConstant::UninterpretedConstant(Type type, Integer index)
-    : d_type(type), d_index(index)
+UninterpretedConstant::UninterpretedConstant(const TypeNode& type,
+                                             Integer index)
+    : d_type(new TypeNode(type)), d_index(index)
 {
   //PrettyCheckArgument(type.isSort(), type, "uninterpreted constants can only be created for uninterpreted sorts, not `%s'", type.toString().c_str());
   PrettyCheckArgument(index >= 0, index, "index >= 0 required for uninterpreted constant index, not `%s'", index.toString().c_str());
 }
 
+UninterpretedConstant::~UninterpretedConstant() {}
+
+UninterpretedConstant::UninterpretedConstant(const UninterpretedConstant& other)
+    : d_type(new TypeNode(other.getType())), d_index(other.getIndex())
+{
+}
+
+const TypeNode& UninterpretedConstant::getType() const { return *d_type; }
+const Integer& UninterpretedConstant::getIndex() const { return d_index; }
+bool UninterpretedConstant::operator==(const UninterpretedConstant& uc) const
+{
+  return getType() == uc.getType() && d_index == uc.d_index;
+}
+bool UninterpretedConstant::operator!=(const UninterpretedConstant& uc) const
+{
+  return !(*this == uc);
+}
+
+bool UninterpretedConstant::operator<(const UninterpretedConstant& uc) const
+{
+  return getType() < uc.getType()
+         || (getType() == uc.getType() && d_index < uc.d_index);
+}
+bool UninterpretedConstant::operator<=(const UninterpretedConstant& uc) const
+{
+  return getType() < uc.getType()
+         || (getType() == uc.getType() && d_index <= uc.d_index);
+}
+bool UninterpretedConstant::operator>(const UninterpretedConstant& uc) const
+{
+  return !(*this <= uc);
+}
+bool UninterpretedConstant::operator>=(const UninterpretedConstant& uc) const
+{
+  return !(*this < uc);
+}
+
 std::ostream& operator<<(std::ostream& out, const UninterpretedConstant& uc) {
   std::stringstream ss;
   ss << uc.getType();
@@ -49,4 +88,11 @@ std::ostream& operator<<(std::ostream& out, const UninterpretedConstant& uc) {
   return out << "uc_" << st.c_str() << "_" << uc.getIndex();
 }
 
+size_t UninterpretedConstantHashFunction::operator()(
+    const UninterpretedConstant& uc) const
+{
+  return TypeNodeHashFunction()(uc.getType())
+         * IntegerHashFunction()(uc.getIndex());
+}
+
 }/* CVC4 namespace */
diff --git a/src/expr/uninterpreted_constant.h b/src/expr/uninterpreted_constant.h
index 46d9a2800..eb6cc203a 100644
--- a/src/expr/uninterpreted_constant.h
+++ b/src/expr/uninterpreted_constant.h
@@ -16,62 +16,50 @@
 
 #include "cvc4_public.h"
 
-#pragma once
+#ifndef CVC4__UNINTERPRETED_CONSTANT_H
+#define CVC4__UNINTERPRETED_CONSTANT_H
 
 #include <iosfwd>
+#include <memory>
 
-#include "expr/type.h"
+#include "util/integer.h"
 
 namespace CVC4 {
 
-class CVC4_PUBLIC UninterpretedConstant {
+class TypeNode;
+
+class UninterpretedConstant
+{
  public:
-  UninterpretedConstant(Type type, Integer index);
+  UninterpretedConstant(const TypeNode& type, Integer index);
+  ~UninterpretedConstant();
 
-  Type getType() const { return d_type; }
-  const Integer& getIndex() const { return d_index; }
-  bool operator==(const UninterpretedConstant& uc) const
-  {
-    return d_type == uc.d_type && d_index == uc.d_index;
-  }
-  bool operator!=(const UninterpretedConstant& uc) const
-  {
-    return !(*this == uc);
-  }
+  UninterpretedConstant(const UninterpretedConstant& other);
 
-  bool operator<(const UninterpretedConstant& uc) const
-  {
-    return d_type < uc.d_type ||
-           (d_type == uc.d_type && d_index < uc.d_index);
-  }
-  bool operator<=(const UninterpretedConstant& uc) const
-  {
-    return d_type < uc.d_type ||
-           (d_type == uc.d_type && d_index <= uc.d_index);
-  }
-  bool operator>(const UninterpretedConstant& uc) const
-  {
-    return !(*this <= uc);
-  }
-  bool operator>=(const UninterpretedConstant& uc) const
-  {
-    return !(*this < uc);
-  }
+  const TypeNode& getType() const;
+  const Integer& getIndex() const;
+  bool operator==(const UninterpretedConstant& uc) const;
+  bool operator!=(const UninterpretedConstant& uc) const;
+  bool operator<(const UninterpretedConstant& uc) const;
+  bool operator<=(const UninterpretedConstant& uc) const;
+  bool operator>(const UninterpretedConstant& uc) const;
+  bool operator>=(const UninterpretedConstant& uc) const;
 
  private:
-  const Type d_type;
+  std::unique_ptr<TypeNode> d_type;
   const Integer d_index;
-};/* class UninterpretedConstant */
+}; /* class UninterpretedConstant */
 
-std::ostream& operator<<(std::ostream& out, const UninterpretedConstant& uc) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out, const UninterpretedConstant& uc);
 
 /**
  * Hash function for the BitVector constants.
  */
-struct CVC4_PUBLIC UninterpretedConstantHashFunction {
-  inline size_t operator()(const UninterpretedConstant& uc) const {
-    return TypeHashFunction()(uc.getType()) * IntegerHashFunction()(uc.getIndex());
-  }
-};/* struct UninterpretedConstantHashFunction */
+struct CVC4_PUBLIC UninterpretedConstantHashFunction
+{
+  size_t operator()(const UninterpretedConstant& uc) const;
+}; /* struct UninterpretedConstantHashFunction */
+
+}  // namespace CVC4
 
-}/* CVC4 namespace */
+#endif /* CVC4__UNINTERPRETED_CONSTANT_H */
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 3a6b9bfff..29ac4f2d1 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -96,7 +96,7 @@ class SExprTypeRule {
 class UninterpretedConstantTypeRule {
  public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
-    return TypeNode::fromType(n.getConst<UninterpretedConstant>().getType());
+    return n.getConst<UninterpretedConstant>().getType();
   }
 };/* class UninterpretedConstantTypeRule */
 
diff --git a/src/theory/builtin/type_enumerator.h b/src/theory/builtin/type_enumerator.h
index edac15d86..18dcf4521 100644
--- a/src/theory/builtin/type_enumerator.h
+++ b/src/theory/builtin/type_enumerator.h
@@ -60,7 +60,8 @@ class UninterpretedSortEnumerator : public TypeEnumeratorBase<UninterpretedSortE
     if(isFinished()) {
       throw NoMoreValuesException(getType());
     }
-    return NodeManager::currentNM()->mkConst(UninterpretedConstant(getType().toType(), d_count));
+    return NodeManager::currentNM()->mkConst(
+        UninterpretedConstant(getType(), d_count));
   }
 
   UninterpretedSortEnumerator& operator++() override
diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
index 699e26d21..450a0fd37 100644
--- a/src/theory/datatypes/datatypes_rewriter.cpp
+++ b/src/theory/datatypes/datatypes_rewriter.cpp
@@ -720,7 +720,7 @@ Node DatatypesRewriter::normalizeCodatatypeConstantEqc(
     {
       int debruijn = depth - it->second - 1;
       return NodeManager::currentNM()->mkConst(
-          UninterpretedConstant(n.getType().toType(), debruijn));
+          UninterpretedConstant(n.getType(), debruijn));
     }
     std::vector<Node> children;
     bool childChanged = false;
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index d6cb3b37e..505d08c38 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -1642,7 +1642,8 @@ Node TheoryDatatypes::getCodatatypesValue( Node n, std::map< Node, Node >& eqc_c
   std::map< Node, int >::iterator itv = vmap.find( n );
   if( itv!=vmap.end() ){
     int debruijn = depth - 1 - itv->second;
-    return NodeManager::currentNM()->mkConst(UninterpretedConstant(n.getType().toType(), debruijn));
+    return NodeManager::currentNM()->mkConst(
+        UninterpretedConstant(n.getType(), debruijn));
   }else if( n.getType().isDatatype() ){
     Node nc = eqc_cons[n];
     if( !nc.isNull() ){
diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp
index ccaba009d..3dca74b19 100644
--- a/src/theory/datatypes/type_enumerator.cpp
+++ b/src/theory/datatypes/type_enumerator.cpp
@@ -107,7 +107,7 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){
      if (d_child_enum)
      {
        ret = NodeManager::currentNM()->mkConst(
-           UninterpretedConstant(d_type.toType(), d_size_limit));
+           UninterpretedConstant(d_type, d_size_limit));
      }
      else
      {
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index d77f6fe83..f2e13d1e0 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -333,7 +333,8 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId,
 #ifdef CVC4_ASSERTIONS
           RewriteResponse r2 =
               d_theoryRewriters[newTheoryId]->postRewrite(response.d_node);
-          Assert(r2.d_node == response.d_node);
+          Assert(r2.d_node == response.d_node)
+              << r2.d_node << " != " << response.d_node;
 #endif
           rewriteStackTop.d_node = response.d_node;
           break;