From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 27 Feb 2020 02:08:01 +0000 (-0600)
Subject: Move fix for vacuous sygus types out of the parser (#3820)
X-Git-Tag: cvc5-1.0.0~3588
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=80f7cf5cd02ff5bb277657fd0adb616020bb9f65;p=cvc5.git

Move fix for vacuous sygus types out of the parser (#3820)

This moves a fix for vacuous sygus types out of the parser and into the Expr-level datatype.

This is a temporary fix so that further progress can be made on parser migration (and to declutter the parser).

This will be refactored when an API for SyGuS is established (CVC4/cvc4-projects#38).
---

diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 5f43fb24f..dd5f12b28 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -223,6 +223,41 @@ void Datatype::addConstructor(const DatatypeConstructor& c) {
 void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){
   PrettyCheckArgument(
       !isResolved(), this, "cannot set sygus type to a finalized Datatype");
+  // We can be in a case where the only rule specified was
+  // (Constant T), in which case we have not yet added a constructor. We
+  // ensure an arbitrary constant is added in this case. We additionally
+  // add a constant if the grammar has only non-nullary constructors, since this
+  // ensures the datatype is well-founded (see 3423).
+  // Notice we only want to do this for sygus datatypes that are user-provided.
+  // At the moment, the condition !allow_all implies the grammar is
+  // user-provided and hence may require a default constant.
+  // TODO (https://github.com/CVC4/cvc4-projects/issues/38):
+  // In an API for SyGuS, it probably makes more sense for the user to
+  // explicitly add the "any constant" constructor with a call instead of
+  // passing a flag. This would make the block of code unnecessary.
+  if (allow_const && !allow_all)
+  {
+    // if i don't already have a constant (0-ary constructor)
+    bool hasConstant = false;
+    for (unsigned i = 0, ncons = getNumConstructors(); i < ncons; i++)
+    {
+      if ((*this)[i].getNumArgs() == 0)
+      {
+        hasConstant = true;
+        break;
+      }
+    }
+    if (!hasConstant)
+    {
+      // add an arbitrary one
+      Expr op = st.mkGroundTerm();
+      std::stringstream cname;
+      cname << op;
+      std::vector<Type> cargs;
+      addSygusConstructor(op, cname.str(), cargs);
+    }
+  }
+
   TypeNode stn = TypeNode::fromType(st);
   Node bvln = Node::fromExpr(bvl);
   d_internal->setSygus(stn, bvln, allow_const, allow_all);
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index eca32cb83..caa3e471f 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1036,18 +1036,7 @@ sygusGrammar[CVC4::Type & ret,
       // We can be in a case where the only rule specified was (Variable T)
       // and there are no variables of type T, in which case this is a bogus
       // grammar. This results in the error below.
-      // We can also be in a case where the only rule specified was
-      // (Constant T), in which case we have not yet added a constructor. We
-      // ensure an arbitrary constant is added in this case. We additionally
-      // add a constant if the grammar allows it regardless of whether the
-      // datatype has other constructors, since this ensures the datatype is
-      // well-founded (see 3423).
-      if (aci)
-      {
-        Expr c = btt.mkGroundTerm();
-        PARSER_STATE->addSygusConstructorTerm(datatypes[i], c, ntsToUnres);
-      }
-      else if (datatypes[i].getNumConstructors() == 0)
+      if (datatypes[i].getNumConstructors() == 0)
       {
         std::stringstream se;
         se << "Grouped rule listing for " << datatypes[i].getName()