Fix `TypeNode::substitute()` (#7916)

Fixes cvc5/cvc5-projects#397. Fixes
cvc5/cvc5-projects#399. After performing the
substitution on the child node, the result was not added as a child to
the node under construction, resulting in nodes with too few children.
This commit fixes that issue.

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 8358facacc1f851e65704c6514a050ac384725b6..b03e9bc457f87a797db92cc43da39e5356be1603 100644 (file)
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -57,7 +57,7 @@ TypeNode TypeNode::substitute(
     }
     else
     {
-      (*j).substitute(type, replacement);
+      nb << (*j).substitute(type, replacement);
     }
   }
 

diff --git a/test/api/cpp/CMakeLists.txt b/test/api/cpp/CMakeLists.txt
index 929c5bef2b885753a95572fb2400e0604b045ad4..8b860ec1d3466897246995d5c44c3667f9776646 100644 (file)
--- a/test/api/cpp/CMakeLists.txt
+++ b/test/api/cpp/CMakeLists.txt
@@ -56,3 +56,4 @@ 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-issue399)

diff --git a/test/api/cpp/proj-issue399.cpp b/test/api/cpp/proj-issue399.cpp
new file mode 100644 (file)
index 0000000..03ed55c
--- /dev/null
+++ b/test/api/cpp/proj-issue399.cpp
@@ -0,0 +1,39 @@
+/******************************************************************************
+ * 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 #399
+ *
+ */
+
+#include <cassert>
+
+#include "api/cpp/cvc5.h"
+
+using namespace cvc5::api;
+
+int main(void)
+{
+  Solver slv;
+  Sort s1 = slv.mkUninterpretedSort("_u0");
+  Sort s2 = slv.getStringSort();
+  Sort _p2 = slv.mkParamSort("_p2");
+  Sort _p3 = slv.mkParamSort("_p3");
+  DatatypeDecl _dt1 = slv.mkDatatypeDecl("_dt1", {_p2, _p3});
+  DatatypeConstructorDecl _cons21 = slv.mkDatatypeConstructorDecl("_cons21");
+  _cons21.addSelector("_sel16", _p2);
+  _dt1.addConstructor(_cons21);
+  Sort s3 = slv.mkDatatypeSort(_dt1);
+  Sort s4 = slv.mkBagSort(s2);
+  Sort s5 = slv.mkArraySort(s1, s4);
+  Sort s9 = s3.instantiate({s4, s4});
+  (void)s5.substitute({s4}, {s9});
+}