From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 6 Mar 2020 16:18:39 +0000 (-0600)
Subject: Make sygus datatype building independent of parser in sygus v2 (#3923)
X-Git-Tag: cvc5-1.0.0~3556
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f3a773dc772cc3ef0590f01e7ce2ebe0ce87bfd3;p=cvc5.git

Make sygus datatype building independent of parser in sygus v2 (#3923)

The current sygus v2 called the parser's mkMututalDatatypeTypes function, which unecessarily created the datatype and bound its (internally generated) constructor/selector symbols in the symbol tables of the parser. This resolves this dependency.

The same issue also exists in the sygus v1 parser but is harder to resolve; I am leaving this for now since that code will be deleted in the next version of CVC4.

This is work towards the SyGuS API.
---

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index cd661364d..14396c771 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -943,7 +943,7 @@ sygusGrammar[CVC4::api::Sort & ret,
   std::string name;
   CVC4::api::Term e, e2;
   std::vector<CVC4::Datatype> datatypes;
-  std::vector<api::Sort> unresTypes;
+  std::set<api::Sort> unresTypes;
   std::map<CVC4::api::Term, CVC4::api::Sort> ntsToUnres;
   unsigned dtProcessed = 0;
   std::unordered_set<unsigned> allowConst;
@@ -964,7 +964,7 @@ sygusGrammar[CVC4::api::Sort & ret,
       // the datatype
       PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT);
       api::Sort urt = PARSER_STATE->mkUnresolvedType(dname);
-      unresTypes.push_back(urt);
+      unresTypes.insert(urt);
       // make the non-terminal symbol, which will be parsed as an ordinary
       // free variable.
       api::Term nts = PARSER_STATE->bindBoundVar(i.first, i.second);
@@ -1056,9 +1056,11 @@ sygusGrammar[CVC4::api::Sort & ret,
     PARSER_STATE->popScope();
     // now, make the sygus datatype
     Trace("parser-sygus2") << "Make the sygus datatypes..." << std::endl;
+    std::set<Type> utypes = api::sortSetToTypes(unresTypes);
     std::vector<DatatypeType> datatypeTypes =
-        PARSER_STATE->mkMutualDatatypeTypes(
-            datatypes, false, ExprManager::DATATYPE_FLAG_PLACEHOLDER);
+        SOLVER->getExprManager()->mkMutualDatatypeTypes(
+            datatypes, utypes,
+            ExprManager::DATATYPE_FLAG_PLACEHOLDER);
     // return is the first datatype
     ret = datatypeTypes[0];
   }