Make mkGroundTerm deterministic (#5347)

This ensures mkGroundTerm is deterministic using attributes.

This was uncovered by failures in the proof checker for datatypes.

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 7f89b4de3e2d31f035989ca4385322c3a6285827..1a06e936692298c1c6ec28c02dcb0be12a1e7058 100644 (file)
--- 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 (file)
index 0000000..59c1ecd
--- /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 03dc7e415dcce5e9602ae06342805fc2a4456515..1b251f8e08ea7b17947e58b84f5dd3c0e9f187d7 100644 (file)
--- 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 {