From e10051079bc5a12e23f0d87447f29f0d3c6622cb Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Fri, 12 Nov 2021 08:25:01 -0800
Subject: [PATCH] Fix redundant definitions of `NodeValue::getConst` (#7636)

If multiple kinds have the same payload, cvc5 is currently generating
multiple copies of NodeValue::getConst() with the same template
argument, which results in a redefinition of the same function. This
commit modifies the mkmetakind script to avoid emitting redundant
definitions of NodeValue::getConst().
---
 src/expr/mkmetakind | 58 ++++++++++++++++++++++++++++++++-------------
 1 file changed, 41 insertions(+), 17 deletions(-)

diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index f8282a998..e651de433 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -57,6 +57,18 @@ metakind_operatorKinds=
 seen_theory=false
 seen_theory_builtin=false
 
+payloads_seen=()
+
+function contains {
+  elem=$1
+  shift
+  arr=("$@")
+  for e in "${arr[@]}"; do
+    [[ "$e" == "$elem" ]] && return 0
+  done
+  return 1
+}
+
 function theory {
   # theory ID T header
 
@@ -222,6 +234,13 @@ function constant {
     skip_const_map=false
   fi
 
+  if contains "${class}" "${payloads_seen[@]}"; then
+    payload_seen=true
+  else
+    payload_seen=false
+    payloads_seen=(${payloads_seen[@]} "${class}")
+  fi
+
   if [[ "$2" != "skip" ]]; then
     metakind_fwd_decls="${metakind_fwd_decls}
 $2 ${class};"
@@ -233,27 +252,14 @@ $2 ${class};"
 #include \"$5\""
   fi
   register_metakind CONSTANT "$1" 0
-  metakind_getConst_decls="${metakind_getConst_decls}
-template <>
-${class} const& NodeValue::getConst< ${class} >() const;
-"
-  if [ "${skip_const_map}" != true ]; then
-    metakind_constantMaps_decls="${metakind_constantMaps_decls}
-template <>
-struct ConstantMap< ${class} > {
-  static constexpr Kind kind = ::cvc5::kind::$1;
-};/* ConstantMap< ${class} > */
-"
-  fi
 
-  metakind_constantMaps_decls="${metakind_constantMaps_decls}
+  if [[ "${payload_seen}" != true ]]; then
+    metakind_getConst_decls="${metakind_getConst_decls}
 template <>
-struct ConstantMapReverse< ::cvc5::kind::$1 > {
-  using T = ${class};
-};/* ConstantMapReverse< ::cvc5::kind::$1 > */
+${class} const& NodeValue::getConst< ${class} >() const;
 "
 
-  metakind_constantMaps="${metakind_constantMaps}
+    metakind_constantMaps="${metakind_constantMaps}
 // The reinterpret_cast of d_children to \"${class} const*\"
 // flags a \"strict aliasing\" warning; it's okay, because we never access
 // the embedded constant as a NodeValue* child, and never access an embedded
@@ -276,6 +282,24 @@ ${class} const& NodeValue::getConst< ${class} >() const {
 #pragma GCC diagnostic warning \"-Wstrict-aliasing\"
 
 "
+  fi
+
+  if [ "${skip_const_map}" != true ]; then
+    metakind_constantMaps_decls="${metakind_constantMaps_decls}
+template <>
+struct ConstantMap< ${class} > {
+  static constexpr Kind kind = ::cvc5::kind::$1;
+};/* ConstantMap< ${class} > */
+"
+  fi
+
+  metakind_constantMaps_decls="${metakind_constantMaps_decls}
+template <>
+struct ConstantMapReverse< ::cvc5::kind::$1 > {
+  using T = ${class};
+};/* ConstantMapReverse< ::cvc5::kind::$1 > */
+"
+
   metakind_compares="${metakind_compares}
     case kind::$1:
       return NodeValueConstCompare< kind::$1, pool >::compare(nv1, nv2);
-- 
2.30.2