Improve interface for sygus datatype, fix utilities (#3473)

2 files changed, 37 insertions, 5 deletions

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
index 40046ef15..019abc28a 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
@@ -495,6 +495,7 @@ TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn,
                                              const Datatype& dt,
                                              std::vector<unsigned>& op_pos)
 {
+  Assert(tn.isDatatype());
   /* Corresponding type node to tn with the given operator positions. To be
    * retrieved (if cached) or defined (otherwise) */
   TypeNode unres_tn;
@@ -591,8 +592,19 @@ TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn,
 
 TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn)
 {
+  if (!tn.isDatatype())
+  {
+    // Might not be a sygus datatype, e.g. if the input grammar had the
+    // any constant constructor.
+    return tn;
+  }
   /* Collect all operators for normalization */
-  const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+  const Datatype& dt = tn.getDatatype();
+  if (!dt.isSygus())
+  {
+    // datatype but not sygus datatype case
+    return tn;
+  }
   std::vector<unsigned> op_pos(dt.getNumConstructors());
   std::iota(op_pos.begin(), op_pos.end(), 0);
   return normalizeSygusRec(tn, dt, op_pos);
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
index 6bf8c56fb..b1b1ea62c 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/sygus/sygus_grammar_red.h"
 
+#include "expr/sygus_datatype.h"
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
@@ -41,18 +42,37 @@ void SygusRedundantCons::initialize(QuantifiersEngine* qe, TypeNode tn)
   {
     Trace("sygus-red") << "  Is " << dt[i].getName() << " a redundant operator?"
                        << std::endl;
+    Node sop = Node::fromExpr(dt[i].getSygusOp());
+    if (sop.getAttribute(SygusAnyConstAttribute()))
+    {
+      // the any constant constructor is never redundant
+      d_sygus_red_status.push_back(0);
+      continue;
+    }
     std::map<int, Node> pre;
     // We do not do beta reduction, since we want the arguments to match the
     // the types of the datatype.
     Node g = tds->mkGeneric(dt, i, pre, false);
     Trace("sygus-red-debug") << "  ...pre-rewrite : " << g << std::endl;
     d_gen_terms[i] = g;
-    for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
+    // a list of variants of the generic term (see getGenericList).
+    std::vector<Node> glist;
+    if (sop.isConst() || sop.getKind() == LAMBDA)
+    {
+      Assert(g.getNumChildren() == dt[i].getNumArgs());
+      for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
+      {
+        pre[j] = g[j];
+      }
+      getGenericList(tds, dt, i, 0, pre, glist);
+    }
+    else
     {
-      pre[j] = g[j];
+      // It is a builtin (possibly) ground term. Its children do not correspond
+      // one-to-one with the arugments of the constructor. Hence, we consider
+      // only g itself as a variant.
+      glist.push_back(g);
     }
-    std::vector<Node> glist;
-    getGenericList(tds, dt, i, 0, pre, glist);
     // call the extended rewriter
     bool red = false;
     for (const Node& gr : glist)