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