Do not require sygus constructors to be flattened (#3049)

5 files changed, 48 insertions, 12 deletions

diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
index e44b604d0..7324add50 100644
--- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
+++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
@@ -133,7 +133,18 @@ void SygusEvalUnfold::registerModelValue(Node a,
         bool do_unfold = false;
         if (options::sygusEvalUnfoldBool())
         {
-          if (bTerm.getKind() == ITE || bTerm.getType().isBoolean())
+          Node bTermUse = bTerm;
+          if (bTerm.getKind() == APPLY_UF)
+          {
+            // if the builtin term is non-beta-reduced application of lambda,
+            // we look at the body of the lambda.
+            Node bTermOp = bTerm.getOperator();
+            if (bTermOp.getKind() == LAMBDA)
+            {
+              bTermUse = bTermOp[0];
+            }
+          }
+          if (bTermUse.getKind() == ITE || bTermUse.getType().isBoolean())
           {
             do_unfold = true;
           }
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 48da8e8e8..263c88d15 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -712,7 +712,14 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       for (unsigned k = 0, size_k = dt.getNumConstructors(); k < size_k; ++k)
       {
         Trace("sygus-grammar-def") << "...for " << dt[k].getName() << std::endl;
-        ops[i].push_back( dt[k].getConstructor() );
+        Expr cop = dt[k].getConstructor();
+        if (dt[k].getNumArgs() == 0)
+        {
+          // Nullary constructors are interpreted as terms, not operators.
+          // Thus, we apply them to no arguments here.
+          cop = nm->mkNode(APPLY_CONSTRUCTOR, Node::fromExpr(cop)).toExpr();
+        }
+        ops[i].push_back(cop);
         cnames[i].push_back(dt[k].getName());
         cargs[i].push_back(std::vector<Type>());
         Trace("sygus-grammar-def") << "...add for selectors" << std::endl;
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
index 6ad590f28..2b2c87f38 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
@@ -43,7 +43,6 @@ void SygusRedundantCons::initialize(QuantifiersEngine* qe, TypeNode tn)
     std::map<int, Node> pre;
     Node g = tds->mkGeneric(dt, i, pre);
     Trace("sygus-red-debug") << "  ...pre-rewrite : " << g << std::endl;
-    Assert(g.getNumChildren() == dt[i].getNumArgs());
     d_gen_terms[i] = g;
     for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
     {
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index af820b0fc..01d08dad8 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -411,6 +411,11 @@ void TermDbSygus::registerSygusType( TypeNode tn ) {
             Trace("sygus-db") << ", kind = " << sk;
             d_kinds[tn][sk] = i;
             d_arg_kind[tn][i] = sk;
+            if (sk == ITE)
+            {
+              // mark that this type has an ITE
+              d_hasIte[tn] = true;
+            }
           }
           else if (sop.isConst() && dt[i].getNumArgs() == 0)
           {
@@ -432,6 +437,11 @@ void TermDbSygus::registerSygusType( TypeNode tn ) {
                   << ", argument to a lambda constructor is not " << lat
                   << std::endl;
             }
+            if (sop[0].getKind() == ITE)
+            {
+              // mark that this type has an ITE
+              d_hasIte[tn] = true;
+            }
           }
           // symbolic constructors
           if (n.getAttribute(SygusAnyConstAttribute()))
@@ -602,7 +612,7 @@ void TermDbSygus::registerEnumerator(Node e,
         // solution" clauses.
         const Datatype& dt = et.getDatatype();
         if (options::sygusStream()
-            || (!hasKind(et, ITE) && !dt.getSygusType().isBoolean()))
+            || (!hasIte(et) && !dt.getSygusType().isBoolean()))
         {
           isActiveGen = true;
         }
@@ -1003,6 +1013,10 @@ int TermDbSygus::getOpConsNum( TypeNode tn, Node n ) {
 bool TermDbSygus::hasKind( TypeNode tn, Kind k ) {
   return getKindConsNum( tn, k )!=-1;
 }
+bool TermDbSygus::hasIte(TypeNode tn) const
+{
+  return d_hasIte.find(tn) != d_hasIte.end();
+}
 bool TermDbSygus::hasConst( TypeNode tn, Node n ) {
   return getConstConsNum( tn, n )!=-1;
 }
@@ -1502,14 +1516,9 @@ Node TermDbSygus::unfold( Node en, std::map< Node, Node >& vtm, std::vector< Nod
     pre[j] = nm->mkNode(DT_SYGUS_EVAL, cc);
   }
   Node ret = mkGeneric(dt, i, pre);
-  // if it is a variable, apply the substitution
-  if (ret.getKind() == kind::BOUND_VARIABLE)
-  {
-    Assert(ret.hasAttribute(SygusVarNumAttribute()));
-    int i = ret.getAttribute(SygusVarNumAttribute());
-    Assert(Node::fromExpr(dt.getSygusVarList())[i] == ret);
-    return args[i];
-  }
+  // apply the appropriate substitution to ret
+  ret = datatypes::DatatypesRewriter::applySygusArgs(dt, sop, ret, args);
+  // rewrite
   ret = Rewriter::rewrite(ret);
   return ret;
 }
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index 0f3d650d3..2854ecab6 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -393,6 +393,11 @@ class TermDbSygus {
   std::map<TypeNode, std::vector<Node> > d_var_list;
   std::map<TypeNode, std::map<int, Kind> > d_arg_kind;
   std::map<TypeNode, std::map<Kind, int> > d_kinds;
+  /**
+   * Whether this sygus type has a constructors whose sygus operator is ITE,
+   * or is a lambda whose body is ITE.
+   */
+  std::map<TypeNode, bool> d_hasIte;
   std::map<TypeNode, std::map<int, Node> > d_arg_const;
   std::map<TypeNode, std::map<Node, int> > d_consts;
   std::map<TypeNode, std::map<Node, int> > d_ops;
@@ -462,6 +467,11 @@ class TermDbSygus {
   int getConstConsNum( TypeNode tn, Node n );
   int getOpConsNum( TypeNode tn, Node n );
   bool hasKind( TypeNode tn, Kind k );
+  /**
+   * Returns true if this sygus type has a constructors whose sygus operator is
+   * ITE, or is a lambda whose body is ITE.
+   */
+  bool hasIte(TypeNode tn) const;
   bool hasConst( TypeNode tn, Node n );
   bool hasOp( TypeNode tn, Node n );
   Node getConsNumConst( TypeNode tn, int i );