Initial support for parametric datatypes in sygus (#6304)

Fixes #6298.

Enables parsing of par in the sygus parser, and adds support for default grammar construction.

Also fixes a bug related to single invocation for non-function types.

diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp
index 927c48dda80e1454a2eca9550b66840882816ac2..c358aa2e89af4e4471d65a10190ef55afd8d425c 100644 (file)
--- a/src/expr/dtype_cons.cpp
+++ b/src/expr/dtype_cons.cpp
@@ -120,15 +120,20 @@ TypeNode DTypeConstructor::getSpecializedConstructorType(
       << "DTypeConstructor::getSpecializedConstructorType: expected datatype, "
          "got "
       << returnType;
+  TypeNode ctn = d_constructor.getType();
   const DType& dt = DType::datatypeOf(d_constructor);
-  Assert(dt.isParametric());
+  if (!dt.isParametric())
+  {
+    // if the datatype is not parametric, then no specialization is needed
+    return ctn;
+  }
   TypeNode dtt = dt.getTypeNode();
   TypeMatcher m(dtt);
   m.doMatching(dtt, returnType);
   std::vector<TypeNode> subst;
   m.getMatches(subst);
   std::vector<TypeNode> params = dt.getParameters();
-  return d_constructor.getType().substitute(
+  return ctn.substitute(
       params.begin(), params.end(), subst.begin(), subst.end());
 }
 

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 3302533e653550bc9ca17b801f918534dadf6675..00cf8e75a8979c25fdc38cf27ae957e7407c3e95 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2217,7 +2217,7 @@ DECLARE_DATATYPES_2_5_TOK : { !( PARSER_STATE->v2_6() || PARSER_STATE->sygus() )
 DECLARE_DATATYPES_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }?'declare-datatypes';
 DECLARE_CODATATYPES_2_5_TOK : { !( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) }?'declare-codatatypes';
 DECLARE_CODATATYPES_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }?'declare-codatatypes';
-PAR_TOK : { PARSER_STATE->v2_6() }?'par';
+PAR_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }?'par';
 COMPREHENSION_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_SETS) }?'comprehension';
 TESTER_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }?'is';
 MATCH_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }?'match';

diff --git a/src/theory/quantifiers/single_inv_partition.cpp b/src/theory/quantifiers/single_inv_partition.cpp
index 7a1a6fb452a4289d4bbaf7e025aba163a6487b58..6885bb01b3bb056ad0bf236c72c086808e110ad6 100644 (file)
--- a/src/theory/quantifiers/single_inv_partition.cpp
+++ b/src/theory/quantifiers/single_inv_partition.cpp
@@ -139,7 +139,7 @@ bool SingleInvocationPartition::init(std::vector<Node>& funcs, Node n)
   if (!funcs.empty())
   {
     TypeNode tn0 = funcs[0].getType();
-    if (tn0.getNumChildren() > 0)
+    if (tn0.isFunction())
     {
       for (unsigned i = 0, nargs = tn0.getNumChildren() - 1; i < nargs; i++)
       {
@@ -155,7 +155,7 @@ bool SingleInvocationPartition::init(std::vector<Node>& funcs, Node n)
         Trace("si-prt") << "...type mismatch" << std::endl;
         return false;
       }
-      else if (tni.getNumChildren() > 0)
+      else if (tni.isFunction())
       {
         for (unsigned j = 0, nargs = tni.getNumChildren() - 1; j < nargs; j++)
         {

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 1c96b134612083b0a809153fdf087a0f8407d904..d1a1315c97e1598afd1e69375666064fee44f7b4 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -458,11 +458,13 @@ void CegGrammarConstructor::collectSygusGrammarTypesFor(
         const DType& dt = range.getDType();
         for (unsigned i = 0, size = dt.getNumConstructors(); i < size; ++i)
         {
-          for (unsigned j = 0, size_args = dt[i].getNumArgs(); j < size_args;
-               ++j)
+          // get the specialized constructor type, which accounts for
+          // parametric datatypes
+          TypeNode ctn = dt[i].getSpecializedConstructorType(range);
+          std::vector<TypeNode> argTypes = ctn.getArgTypes();
+          for (size_t j = 0, nargs = argTypes.size(); j < nargs; ++j)
           {
-            TypeNode tn = dt[i][j].getRangeType();
-            collectSygusGrammarTypesFor(tn, types);
+            collectSygusGrammarTypesFor(argTypes[j], types);
           }
         }
       }
@@ -988,6 +990,13 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       {
         Trace("sygus-grammar-def") << "...for " << dt[l].getName() << std::endl;
         Node cop = dt[l].getConstructor();
+        TypeNode tspec = dt[l].getSpecializedConstructorType(types[i]);
+        // must specialize if a parametric datatype
+        if (dt.isParametric())
+        {
+          cop = nm->mkNode(
+              APPLY_TYPE_ASCRIPTION, nm->mkConst(AscriptionType(tspec)), cop);
+        }
         if (dt[l].getNumArgs() == 0)
         {
           // Nullary constructors are interpreted as terms, not operators.
@@ -996,11 +1005,15 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
         }
         std::vector<TypeNode> cargsCons;
         Trace("sygus-grammar-def") << "...add for selectors" << std::endl;
-        for (unsigned j = 0, size_j = dt[l].getNumArgs(); j < size_j; ++j)
+        // iterate over the arguments of the specialized constructor type,
+        // which accounts for parametric datatypes
+        std::vector<TypeNode> tsargs = tspec.getArgTypes();
+        TypeNode selDomain = type_to_unres[types[i]];
+        for (unsigned j = 0, size_j = tsargs.size(); j < size_j; ++j)
         {
           Trace("sygus-grammar-def")
               << "...for " << dt[l][j].getName() << std::endl;
-          TypeNode crange = dt[l][j].getRangeType();
+          TypeNode crange = tsargs[j];
           Assert(type_to_unres.find(crange) != type_to_unres.end());
           cargsCons.push_back(type_to_unres[crange]);
           // add to the selector type the selector operator
@@ -1008,11 +1021,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
           Assert(std::find(types.begin(), types.end(), crange) != types.end());
           unsigned i_selType = std::distance(
               types.begin(), std::find(types.begin(), types.end(), crange));
-          TypeNode arg_type = dt[l][j].getType();
-          arg_type = arg_type.getSelectorDomainType();
-          Assert(type_to_unres.find(arg_type) != type_to_unres.end());
           std::vector<TypeNode> cargsSel;
-          cargsSel.push_back(type_to_unres[arg_type]);
+          cargsSel.push_back(selDomain);
           Node sel = dt[l][j].getSelector();
           sdts[i_selType].addConstructor(sel, dt[l][j].getName(), cargsSel);
         }

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index c7c311079db14790d358cd13bffacc164769b1d9..83f1c7d84d82462e937264fb786fc8a7a263d3b8 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1172,6 +1172,7 @@ set(regress_0_tests
   regress0/sygus/issue4383-cache-fv-id.sy
   regress0/sygus/issue4790-dtd.sy
   regress0/sygus/issue5512-vvv.sy
+  regress0/sygus/issue6298-par.sy
   regress0/sygus/let-ringer.sy
   regress0/sygus/let-simp.sy
   regress0/sygus/no-logic.sy

diff --git a/test/regress/regress0/sygus/issue6298-par.sy b/test/regress/regress0/sygus/issue6298-par.sy
new file mode 100644 (file)
index 0000000..bffa02b
--- /dev/null
+++ b/test/regress/regress0/sygus/issue6298-par.sy
@@ -0,0 +1,6 @@
+; EXPECT: unsat
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
+(set-logic ALL)
+(declare-datatypes (( List 1)) ( (par (T) ((nil) (cons (head T) (tail (List T)))))))
+(synth-fun f () (List Int))
+(check-synth)