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

diff --git a/src/parser/parser.h b/src/parser/parser.h
index d6c0e0e158cc7688f36c143f50144e7d6f7396eb..72e175a58b56a1fb56956cfacff85df61be02649 100644 (file)
--- 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 69f21acb779a64110f163e5b02bfc081299e349f..0c42678aa31ba65cf7a2eb76601d395edc63678f 100644 (file)
--- 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];
   };