From a8d9b88e3a73edcbe845203842dcb85e241927e6 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 23 Oct 2023 17:22:17 -0500
Subject: [PATCH] Fix sygus grammar construction for parametric datatypes
 (#10085)

---
 .../quantifiers/sygus/sygus_grammar_cons.cpp      |  8 +++++---
 test/regress/cli/CMakeLists.txt                   |  1 +
 test/regress/cli/regress1/abduction/param-dt.smt2 | 15 +++++++++++++++
 3 files changed, 21 insertions(+), 3 deletions(-)
 create mode 100644 test/regress/cli/regress1/abduction/param-dt.smt2

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 9357e1c28aa..9e15cf381e1 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -694,11 +694,11 @@ void SygusGrammarCons::collectTypes(const TypeNode& range,
   {
     return;
   }
+  types.insert(range);
   if (range.isDatatype())
   {
     // special case: datatypes we add itself and its subfield types, taking
     // into account parametric datatypes
-    types.insert(range);
     const DType& dt = range.getDType();
     for (size_t i = 0, size = dt.getNumConstructors(); i < size; ++i)
     {
@@ -717,11 +717,13 @@ void SygusGrammarCons::collectTypes(const TypeNode& range,
   {
     // special case: uninterpreted sorts (which include sorts constructed
     // from uninterpreted sort constructors), we only add the sort itself.
-    types.insert(range);
     return;
   }
   // otherwise, get the component types
-  expr::getComponentTypes(range, types);
+  for (unsigned i = 0, nchild = range.getNumChildren(); i < nchild; i++)
+  {
+    collectTypes(range[i], types);
+  }
   // add further types based on theory symbols
   if (range.isStringLike())
   {
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 98986fece1f..2720525b55e 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -1926,6 +1926,7 @@ set(regress_1_tests
   regress1/abduction/issue6605-1.smt2
   regress1/abduction/issue9001-sample-fail.smt2
   regress1/abduction/multiple-get-abduct-uc.smt2
+  regress1/abduction/param-dt.smt2
   regress1/abduction/simple-incremental.smt2
   regress1/abduction/simple-incremental-push-pop.smt2
   regress1/abduction/sygus-abduct-ex1-grammar.smt2
diff --git a/test/regress/cli/regress1/abduction/param-dt.smt2 b/test/regress/cli/regress1/abduction/param-dt.smt2
new file mode 100644
index 00000000000..71a161353ba
--- /dev/null
+++ b/test/regress/cli/regress1/abduction/param-dt.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --produce-abducts
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic QF_UFLIA)
+(set-option :produce-abducts true)
+(set-option :sygus-core-connective false)
+(declare-sort A 0)
+(declare-datatype List (par (E)
+  ((nil)
+   (cons (hd E) (tl (List E))))))
+(declare-fun a () A) ;a
+(declare-fun app ((List A) (List A)) (List A)) ;++
+(declare-fun y () (List A)) ;y
+(declare-fun x () (List A)) ;x
+(get-abduct X (not (= (as nil (List A)) (app x y))))