Fix `TypeNode::substitute()` for type constants (#7920)

Fixes cvc5/cvc5-projects#395. The
TypeNode::substitute() method did not account for type constants such
as the Boolean type and was trying to use a NodeBuilder to build such
constants instead. This commit fixes the issue by adding a special case
for types without children.

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index b03e9bc457f87a797db92cc43da39e5356be1603..de85dfb06b51eb32dc03ffb01102b986b34e698a 100644 (file)
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -42,6 +42,15 @@ TypeNode TypeNode::substitute(
   if(i != cache.end()) {
     return (*i).second;
   }
+  else if (*this == type)
+  {
+    return replacement;
+  }
+
+  if (d_nv->getNumChildren() == 0)
+  {
+    return *this;
+  }
 
   // otherwise compute
   NodeBuilder nb(getKind());

diff --git a/test/api/cpp/CMakeLists.txt b/test/api/cpp/CMakeLists.txt
index 8b860ec1d3466897246995d5c44c3667f9776646..0c9bcc463718ad447e2650d58b8f27dc8bc28d86 100644 (file)
--- a/test/api/cpp/CMakeLists.txt
+++ b/test/api/cpp/CMakeLists.txt
@@ -56,4 +56,5 @@ cvc5_add_api_test(proj-issue306)
 cvc5_add_api_test(proj-issue334)
 cvc5_add_api_test(proj-issue344)
 cvc5_add_api_test(proj-issue345)
+cvc5_add_api_test(proj-issue395)
 cvc5_add_api_test(proj-issue399)

diff --git a/test/api/cpp/proj-issue395.cpp b/test/api/cpp/proj-issue395.cpp
new file mode 100644 (file)
index 0000000..17cac8c
--- /dev/null
+++ b/test/api/cpp/proj-issue395.cpp
@@ -0,0 +1,30 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andres Noetzli
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Test for project issue #395
+ *
+ */
+
+#include <cassert>
+
+#include "api/cpp/cvc5.h"
+
+using namespace cvc5::api;
+
+int main(void)
+{
+  Solver slv;
+  Sort s1 = slv.getBooleanSort();
+  Sort s2 = slv.getIntegerSort();
+  Sort s5 = slv.mkFunctionSort({s2}, s1);
+  (void) s5.substitute({s1}, {s1});
+}