Fix sygus grammar construction for parametric datatypes (cvc5#10085)

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())
   {

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

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))))