From 032bee9200bf64af0851832c97ce20b87a6f8e0f Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 10 Nov 2020 14:09:10 -0600
Subject: [PATCH] Make mkGroundTerm deterministic (#5347)

This ensures mkGroundTerm is deterministic using attributes.

This was uncovered by failures in the proof checker for datatypes.
---
 src/CMakeLists.txt                            |  1 +
 .../builtin/theory_builtin_type_rules.cpp     | 50 +++++++++++++++++++
 .../builtin/theory_builtin_type_rules.h       |  5 +-
 3 files changed, 52 insertions(+), 4 deletions(-)
 create mode 100644 src/theory/builtin/theory_builtin_type_rules.cpp

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 7f89b4de3..1a06e9366 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -475,6 +475,7 @@ libcvc4_add_sources(
   theory/builtin/theory_builtin.h
   theory/builtin/theory_builtin_rewriter.cpp
   theory/builtin/theory_builtin_rewriter.h
+  theory/builtin/theory_builtin_type_rules.cpp
   theory/builtin/theory_builtin_type_rules.h
   theory/builtin/type_enumerator.cpp
   theory/builtin/type_enumerator.h
diff --git a/src/theory/builtin/theory_builtin_type_rules.cpp b/src/theory/builtin/theory_builtin_type_rules.cpp
new file mode 100644
index 000000000..59c1ecd65
--- /dev/null
+++ b/src/theory/builtin/theory_builtin_type_rules.cpp
@@ -0,0 +1,50 @@
+/*********************                                                        */
+/*! \file theory_builtin_type_rules.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** 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 Type rules for the builtin theory
+ **
+ ** Type rules for the builtin theory.
+ **/
+
+#include "theory/builtin/theory_builtin_type_rules.h"
+
+#include "expr/attribute.h"
+
+namespace CVC4 {
+namespace theory {
+namespace builtin {
+
+/**
+ * Attribute for caching the ground term for each type. Maps TypeNode to the
+ * skolem to return for mkGroundTerm.
+ */
+struct GroundTermAttributeId
+{
+};
+typedef expr::Attribute<GroundTermAttributeId, Node> GroundTermAttribute;
+
+Node SortProperties::mkGroundTerm(TypeNode type)
+{
+  Assert(type.getKind() == kind::SORT_TYPE);
+  GroundTermAttribute gta;
+  if (type.hasAttribute(gta))
+  {
+    return type.getAttribute(gta);
+  }
+  Node k = NodeManager::currentNM()->mkSkolem(
+      "groundTerm", type, "a ground term created for type " + type.toString());
+  type.setAttribute(gta, k);
+  return k;
+}
+
+}  // namespace builtin
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 03dc7e415..1b251f8e0 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -199,10 +199,7 @@ class SortProperties {
   inline static bool isWellFounded(TypeNode type) {
     return true;
   }
-  inline static Node mkGroundTerm(TypeNode type) {
-    Assert(type.getKind() == kind::SORT_TYPE);
-    return NodeManager::currentNM()->mkSkolem("groundTerm", type, "a ground term created for type " + type.toString());
-  }
+  static Node mkGroundTerm(TypeNode type);
 };/* class SortProperties */
 
 class FunctionProperties {
-- 
2.30.2