2 files changed, 70 insertions, 1 deletions
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 76836d838..0409e5f91 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -171,6 +171,66 @@ Node TermDbSygus::mkGeneric(const Datatype& dt, int c)
   return mkGeneric(dt, c, pre);
 }
 
+struct CanonizeBuiltinAttributeId
+{
+};
+using CanonizeBuiltinAttribute =
+    expr::Attribute<CanonizeBuiltinAttributeId, Node>;
+
+Node TermDbSygus::canonizeBuiltin(Node n)
+{
+  std::map<TypeNode, int> var_count;
+  return canonizeBuiltin(n, var_count);
+}
+
+Node TermDbSygus::canonizeBuiltin(Node n,
+                                  std::map<TypeNode, int>& var_count)
+{
+  // has it already been computed?
+  bool var_count_empty = var_count.empty();
+  if (var_count_empty && n.hasAttribute(CanonizeBuiltinAttribute()))
+  {
+    return n.getAttribute(CanonizeBuiltinAttribute());
+  }
+  Trace("sygus-db-canon") << "  CanonizeBuiltin : compute for " << n << "\n";
+  Node ret = n;
+  // it is symbolic if it represents "any constant"
+  if (n.getKind() == APPLY_SELECTOR_TOTAL)
+  {
+    ret = getFreeVarInc(n[0].getType(), var_count, true);
+  }
+  else if (n.getKind() != APPLY_CONSTRUCTOR)
+  {
+    ret = n;
+  }
+  else
+  {
+    Assert(n.getKind() == APPLY_CONSTRUCTOR);
+    bool childChanged = false;
+    std::vector<Node> children;
+    children.push_back(n.getOperator());
+    for (unsigned j = 0, size = n.getNumChildren(); j < size; ++j)
+    {
+      Node child = canonizeBuiltin(n[j], var_count);
+      children.push_back(child);
+      childChanged = childChanged || child != n[j];
+    }
+    if (childChanged)
+    {
+      ret = NodeManager::currentNM()->mkNode(APPLY_CONSTRUCTOR, children);
+    }
+  }
+  // cache if we had a fresh variable count
+  if (var_count_empty)
+  {
+    n.setAttribute(CanonizeBuiltinAttribute(), ret);
+  }
+  Trace("sygus-db-canon") << "  ...normalized " << n << " --> " << ret
+                          << std::endl;
+  Assert(ret.getType().isComparableTo(n.getType()));
+  return ret;
+}
+
 struct SygusToBuiltinAttributeId
 {
 };
@@ -179,7 +239,7 @@ typedef expr::Attribute<SygusToBuiltinAttributeId, Node>
 
 Node TermDbSygus::sygusToBuiltin(Node n, TypeNode tn)
 {
-  Assert( n.getType()==tn );
+  Assert(n.getType().isComparableTo(tn));
   if (!tn.isDatatype())
   {
     return n;
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index c4a035e2c..bff059190 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -168,6 +168,15 @@ class TermDbSygus {
   Node mkGeneric(const Datatype& dt, int c, std::map<int, Node>& pre);
   /** same as above, but with empty pre */
   Node mkGeneric(const Datatype& dt, int c);
+  /** makes a symbolic term concrete
+   *
+   * 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 canonizeBuiltin(Node n);
+  Node canonizeBuiltin(Node n, std::map<TypeNode, int>& var_count);
   /** sygus to builtin
    *
    * Given a sygus datatype term n of type tn, this function returns its analog,