Eagerly beta reduce during sygus to builtin term conversion (#3418)

diff --git a/src/theory/datatypes/theory_datatypes_utils.cpp b/src/theory/datatypes/theory_datatypes_utils.cpp
index c3b145b157930565f2afb0238b5835c3bdd65d49..bb62ab8aedd768aaaa742be894f34a30c2ae5eaa 100644 (file)
--- a/src/theory/datatypes/theory_datatypes_utils.cpp
+++ b/src/theory/datatypes/theory_datatypes_utils.cpp
@@ -116,7 +116,8 @@ Kind getOperatorKindForSygusBuiltin(Node op)
 
 Node mkSygusTerm(const Datatype& dt,
                  unsigned i,
-                 const std::vector<Node>& children)
+                 const std::vector<Node>& children,
+                 bool doBetaReduction)
 {
   Trace("dt-sygus-util") << "Make sygus term " << dt.getName() << "[" << i
                          << "] with children: " << children << std::endl;
@@ -138,26 +139,44 @@ Node mkSygusTerm(const Datatype& dt,
     Assert(children.size() == 1);
     return children[0];
   }
-  if (op.getKind() != BUILTIN)
+  // get the kind of the operator
+  Kind ok = op.getKind();
+  if (ok != BUILTIN)
   {
-    schildren.push_back(op);
+    if (ok == LAMBDA && doBetaReduction)
+    {
+      // Do immediate beta reduction. It suffices to use a normal substitution
+      // since neither op nor children have quantifiers, since they are
+      // generated by sygus grammars.
+      std::vector<Node> vars{op[0].begin(), op[0].end()};
+      Assert(vars.size() == children.size());
+      Node ret = op[1].substitute(
+          vars.begin(), vars.end(), children.begin(), children.end());
+      Trace("dt-sygus-util") << "...return (beta-reduce) " << ret << std::endl;
+      return ret;
+    }
+    else
+    {
+      schildren.push_back(op);
+    }
   }
   schildren.insert(schildren.end(), children.begin(), children.end());
   Node ret;
-  if (op.getKind() == BUILTIN)
+  if (ok == BUILTIN)
   {
     ret = NodeManager::currentNM()->mkNode(op, schildren);
     Trace("dt-sygus-util") << "...return (builtin) " << ret << std::endl;
     return ret;
   }
-  Kind ok = NodeManager::operatorToKind(op);
-  Trace("dt-sygus-util") << "operator kind is " << ok << std::endl;
-  if (ok != UNDEFINED_KIND)
+  // get the kind used for applying op
+  Kind otk = NodeManager::operatorToKind(op);
+  Trace("dt-sygus-util") << "operator kind is " << otk << std::endl;
+  if (otk != UNDEFINED_KIND)
   {
     // If it is an APPLY_UF operator, we should have at least an operator and
     // a child.
-    Assert(ok != APPLY_UF || schildren.size() != 1);
-    ret = NodeManager::currentNM()->mkNode(ok, schildren);
+    Assert(otk != APPLY_UF || schildren.size() != 1);
+    ret = NodeManager::currentNM()->mkNode(otk, schildren);
     Trace("dt-sygus-util") << "...return (op) " << ret << std::endl;
     return ret;
   }

diff --git a/src/theory/datatypes/theory_datatypes_utils.h b/src/theory/datatypes/theory_datatypes_utils.h
index ba0643567f991f5be016fff1026d7efac10466bd..92783c2f7decbb5d230acaa7150a0163abfcc8be 100644 (file)
--- a/src/theory/datatypes/theory_datatypes_utils.h
+++ b/src/theory/datatypes/theory_datatypes_utils.h
@@ -146,11 +146,13 @@ Kind getOperatorKindForSygusBuiltin(Node op);
  *
  * This function returns a builtin term f( children[0], ..., children[n] )
  * where f is the builtin op that the i^th constructor of sygus datatype dt
- * encodes.
+ * encodes. If doBetaReduction is true, then lambdas are eagerly eliminated
+ * via beta reduction.
  */
 Node mkSygusTerm(const Datatype& dt,
                  unsigned i,
-                 const std::vector<Node>& children);
+                 const std::vector<Node>& children,
+                 bool doBetaReduction = true);
 /**
  * n is a builtin term that is an application of operator op.
  *

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
index a566ebffff98582cf5890c68eda436ae00b6c39d..6bf8c56fb117cfbeae3c2b8acd6055bfea4bc69b 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
@@ -42,7 +42,9 @@ void SygusRedundantCons::initialize(QuantifiersEngine* qe, TypeNode tn)
     Trace("sygus-red") << "  Is " << dt[i].getName() << " a redundant operator?"
                        << std::endl;
     std::map<int, Node> pre;
-    Node g = tds->mkGeneric(dt, i, 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++)
@@ -73,6 +75,8 @@ void SygusRedundantCons::initialize(QuantifiersEngine* qe, TypeNode tn)
     }
     d_sygus_red_status.push_back(red ? 1 : 0);
   }
+  Trace("sygus-red") << "Compute redundant cons for " << tn << " finished"
+                     << std::endl;
 }
 
 void SygusRedundantCons::getRedundant(std::vector<unsigned>& indices)

diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 7fb54f14e5e9fb8a06ad7a9fa7fe36c3aef51c9c..d4ee1145318078aec07d663a65518e5fa57d6e68 100644 (file)
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -162,7 +162,8 @@ TypeNode TermDbSygus::getSygusTypeForVar( Node v ) {
 Node TermDbSygus::mkGeneric(const Datatype& dt,
                             unsigned c,
                             std::map<TypeNode, int>& var_count,
-                            std::map<int, Node>& pre)
+                            std::map<int, Node>& pre,
+                            bool doBetaRed)
 {
   Assert(c < dt.getNumConstructors());
   Assert(dt.isSygus());
@@ -176,6 +177,7 @@ Node TermDbSygus::mkGeneric(const Datatype& dt,
     std::map< int, Node >::iterator it = pre.find( i );
     if( it!=pre.end() ){
       a = it->second;
+      Trace("sygus-db-debug") << "From pre: " << a << std::endl;
     }else{
       TypeNode tna = TypeNode::fromType(dt[c].getArgType(i));
       a = getFreeVarInc( tna, var_count, true );
@@ -185,19 +187,24 @@ Node TermDbSygus::mkGeneric(const Datatype& dt,
     Assert(!a.isNull());
     children.push_back( a );
   }
-  return datatypes::utils::mkSygusTerm(dt, c, children);
+  Node ret = datatypes::utils::mkSygusTerm(dt, c, children, doBetaRed);
+  Trace("sygus-db-debug") << "mkGeneric returns " << ret << std::endl;
+  return ret;
 }
 
-Node TermDbSygus::mkGeneric(const Datatype& dt, int c, std::map<int, Node>& pre)
+Node TermDbSygus::mkGeneric(const Datatype& dt,
+                            int c,
+                            std::map<int, Node>& pre,
+                            bool doBetaRed)
 {
   std::map<TypeNode, int> var_count;
-  return mkGeneric(dt, c, var_count, pre);
+  return mkGeneric(dt, c, var_count, pre, doBetaRed);
 }
 
-Node TermDbSygus::mkGeneric(const Datatype& dt, int c)
+Node TermDbSygus::mkGeneric(const Datatype& dt, int c, bool doBetaRed)
 {
   std::map<int, Node> pre;
-  return mkGeneric(dt, c, pre);
+  return mkGeneric(dt, c, pre, doBetaRed);
 }
 
 struct CanonizeBuiltinAttributeId
@@ -293,6 +300,8 @@ Node TermDbSygus::sygusToBuiltin(Node n, TypeNode tn)
     for (unsigned j = 0, size = n.getNumChildren(); j < size; j++)
     {
       pre[j] = sygusToBuiltin(n[j], TypeNode::fromType(dt[i].getArgType(j)));
+      Trace("sygus-db-debug")
+          << "sygus to builtin " << n[j] << " is " << pre[j] << std::endl;
     }
     Node ret = mkGeneric(dt, i, pre);
     Trace("sygus-db-debug")

diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index 6c62d7a1bae137408ccc05331bb7b6b1550c8df9..68381fb2a83d8256c01d5a1be742ced410995a69 100644 (file)
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -223,15 +223,21 @@ class TermDbSygus {
    *   If i is in the domain of pre, then ti = pre[i].
    *   If i is not in the domain of pre, then ti = d_fv[1][ var_count[Ti ] ],
    *     and var_count[Ti] is incremented.
+   * If doBetaRed is true, then lambda operators are eagerly eliminated via
+   * beta reduction.
    */
   Node mkGeneric(const Datatype& dt,
                  unsigned c,
                  std::map<TypeNode, int>& var_count,
-                 std::map<int, Node>& pre);
+                 std::map<int, Node>& pre,
+                 bool doBetaRed = true);
   /** same as above, but with empty var_count */
-  Node mkGeneric(const Datatype& dt, int c, std::map<int, Node>& pre);
+  Node mkGeneric(const Datatype& dt,
+                 int c,
+                 std::map<int, Node>& pre,
+                 bool doBetaRed = true);
   /** same as above, but with empty pre */
-  Node mkGeneric(const Datatype& dt, int c);
+  Node mkGeneric(const Datatype& dt, int c, bool doBetaRed = true);
   /** makes a symbolic term concrete
    *
    * Given a sygus datatype term n of type tn with holes (symbolic constructor

diff --git a/src/theory/quantifiers/sygus/type_info.cpp b/src/theory/quantifiers/sygus/type_info.cpp
index 8f280c587d5c81ce52e0ca8905dd3697ea738d84..5f51d8dec60e5d7aa8914fc684deba05fc834129 100644 (file)
--- a/src/theory/quantifiers/sygus/type_info.cpp
+++ b/src/theory/quantifiers/sygus/type_info.cpp
@@ -187,6 +187,8 @@ void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn)
     }
     d_min_cons_term_size[i] = csize;
   }
+  Trace("sygus-db") << "Register type " << dt.getName() << " finished"
+                    << std::endl;
 }
 
 void SygusTypeInfo::initializeVarSubclasses()