Stop printing datatype declaration for Sygus V1 grammar. (#4168)

2 files changed, 21 insertions, 2 deletions

diff --git a/src/parser/parser.h b/src/parser/parser.h
index d6c0e0e15..72e175a58 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -273,6 +273,9 @@ public:
     return d_input;
   }
 
+  /** Get unresolved sorts */
+  inline std::set<api::Sort>& getUnresolvedSorts() { return d_unresolved; }
+
   /** Deletes and replaces the current parser input. */
   void setInput(Input* input)  {
     delete d_input;
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 69f21acb7..0c42678aa 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -782,8 +782,24 @@ sygusGrammarV1[CVC4::api::Sort & ret,
       Debug("parser-sygus") << "  " << i << " : " << datatypes[i].getName()
                             << std::endl;
     }
-    std::vector<api::Sort> datatypeTypes =
-        PARSER_STATE->bindMutualDatatypeTypes(datatypes, false);
+
+    std::vector<CVC4::Datatype> dtypes;
+    dtypes.reserve(ndatatypes);
+
+    for (api::DatatypeDecl i : datatypes)
+    {
+      dtypes.push_back(i.getDatatype());
+    }
+
+    std::set<Type> tset =
+        api::sortSetToTypes(PARSER_STATE->getUnresolvedSorts());
+
+    std::vector<DatatypeType> datatypeTypes =
+        SOLVER->getExprManager()->mkMutualDatatypeTypes(
+            dtypes, tset, ExprManager::DATATYPE_FLAG_PLACEHOLDER);
+
+    PARSER_STATE->getUnresolvedSorts().clear();
+
     ret = datatypeTypes[0];
   };