revert

3 files changed, 49 insertions, 43 deletions

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 6f4fb6803..fabe9cbef 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -800,6 +800,8 @@ Node SygusSymBreakNew::registerSearchValue(
     }
   }
   Trace("sygus-sb-debug2") << "Registering search value " << n << " -> " << nv << std::endl;
+  nv = d_tds->canonizeBuiltin(nv, tn);
+  Trace("sygus-sb-debug") << "  ...canonized value is " << nv << std::endl;
   // must do this for all nodes, regardless of top-level
   if( d_cache[a].d_search_val_proc.find( nv )==d_cache[a].d_search_val_proc.end() ){
     d_cache[a].d_search_val_proc.insert(nv);
@@ -810,10 +812,8 @@ Node SygusSymBreakNew::registerSearchValue(
     Trace("sygus-sb-debug") << "  ...register search value " << nv << ", type=" << tn << std::endl;
     Node bv = d_tds->sygusToBuiltin( nv, tn );
     Trace("sygus-sb-debug") << "  ......builtin is " << bv << std::endl;
-    // Node rv = d_tds->reify(bv);
-    // Trace("sygus-sb-debug") << "  ......reified is " << rv << std::endl;
-    // Node bvr = d_tds->getExtRewriter()->extendedRewrite(rv);
     Node bvr = d_tds->getExtRewriter()->extendedRewrite(bv);
+    // Node bvr = d_tds->getExtRewriter()->extendedRewrite(bv);
     Trace("sygus-sb-debug") << "  ......rewrites to " << bvr << std::endl;
     Trace("dt-sygus") << "  * DT builtin : " << n << " -> " << bvr << std::endl;
     unsigned sz = d_tds->getSygusTermSize( nv );      
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 3fd2e0e90..d734a3346 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -171,63 +171,68 @@ Node TermDbSygus::mkGeneric(const Datatype& dt, int c)
   return mkGeneric(dt, c, pre);
 }
 
-
-struct ReifyAttributeId
+struct CanonizeBuiltinAttributeId
 {
 };
-using ReifyAttribute = expr::Attribute<ReifyAttributeId, Node>;
+using CanonizeBuiltinAttribute =
+    expr::Attribute<CanonizeBuiltinAttributeId, Node>;
 
-Node TermDbSygus::reify(Node n)
+Node TermDbSygus::canonizeBuiltin(Node n, TypeNode tn)
 {
+  std::map<TypeNode, int> var_count;
+  return canonizeBuiltin(n, tn, var_count);
+}
+
+Node TermDbSygus::canonizeBuiltin(Node n,
+                                  TypeNode tn,
+                                  std::map<TypeNode, int>& var_count)
+{
+  // not a datatype
+  if (n.getKind() != APPLY_CONSTRUCTOR)
+  {
+    return n;
+  }
   // has it already been computed?
-  if (n.hasAttribute(ReifyAttribute()))
+  bool var_count_empty = var_count.empty();
+  if (var_count_empty && n.hasAttribute(CanonizeBuiltinAttribute()))
   {
-    return n.getAttribute(ReifyAttribute());
+    return n.getAttribute(CanonizeBuiltinAttribute());
   }
-  Trace("sygus-db-reify") << "Reify : compute for " << n << ", type "
-                          << n.getType() << "\n";
+  Trace("sygus-db-canon") << "  CanonizeBuiltin : compute for " << n
+                          << ", type = " << tn << std::endl;
   Node ret = n;
-  if (n.getKind() == APPLY_SELECTOR_TOTAL)
+  const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+  Assert(dt.isSygus());
+  unsigned i = datatypes::DatatypesRewriter::indexOf(n.getOperator());
+  // it is symbolic if it represents "any constant"
+  if (Node::fromExpr(dt[i].getSygusOp()).getAttribute(SygusAnyConstAttribute()))
   {
-    // map to builtin variable type
-    ret = getFreeVar(n.getType(), getVarNum(n));
+    ret = getFreeVarInc(n[0].getType(), var_count);
   }
   else
   {
+    Assert(n.getNumChildren() == dt[i].getNumArgs());
     bool childChanged = false;
     std::vector<Node> children;
-    if (n.getMetaKind() == metakind::PARAMETERIZED)
-    {
-      children.push_back(n.getOperator());
-    }
-    for (unsigned i = 0, size = n.getNumChildren(); i < size; ++i)
+    children.push_back(n.getOperator());
+    for (unsigned j = 0, size = n.getNumChildren(); j < size; ++j)
     {
-      Node child;
-      // if the child is a selection chain, create a free variable
-      if (n[i].getKind() == APPLY_SELECTOR_TOTAL)
-      {
-        // map to builtin variable type
-        child = getFreeVar(n[i].getType(), getVarNum(n[i]));
-        Trace("sygus-db-reify") << "...symb const " << n[i] << " into " << child
-                                << std::endl;
-      }
-      else
-      {
-        Trace("sygus-db-reify") << "...not symb const : " << n[i] << std::endl;
-        child = reify(n[i]);
-      }
+      Node child = canonizeBuiltin(
+          n[j], TypeNode::fromType(dt[i].getArgType(j)), var_count);
+
       children.push_back(child);
-      childChanged = childChanged || child != n[i];
+      childChanged = childChanged || child != n[j];
     }
     if (childChanged)
     {
-      ret = NodeManager::currentNM()->mkNode(n.getKind(), children);
-      Trace("sygus-db-reify") << "Reify : Normalized " << n << " to " << ret
-                              << std::endl;
+      ret = NodeManager::currentNM()->mkNode(APPLY_CONSTRUCTOR, children);
     }
   }
   // cache if we had a fresh variable count
-  n.setAttribute(ReifyAttribute(), ret);
+  if (var_count_empty)
+  {
+    n.setAttribute(CanonizeBuiltinAttribute(), ret);
+  }
   return ret;
 }
 
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index 1ccca358b..e0d98dc80 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -170,12 +170,13 @@ class TermDbSygus {
   Node mkGeneric(const Datatype& dt, int c);
   /** makes a symbolic term concrete
    *
-   * Given a builtin term n of type tn with holes (selection chains), this
-   * function returns a term in which holes are replaced by unique variables. To
-   * track counters for introducing unique variables, we use the var_count map.
+   * Given a sygus datatype term n of type tn with holes (symbolic constructor
+   * applications), this function returns a term in which holes are replaced by
+   * unique variables. To track counters for introducing unique variables, we
+   * use the var_count map.
    */
-  Node reify(Node n);
-  Node reify(Node n, std::map<TypeNode, int>& var_count);
+  Node canonizeBuiltin(Node n, TypeNode tn);
+  Node canonizeBuiltin(Node n, TypeNode tn, std::map<TypeNode, int>& var_count);
   /** sygus to builtin
    *
    * Given a sygus datatype term n of type tn, this function returns its analog,