Enumerate shapes feature in fast sygus enumerator (#4742)

This adds the feature of enumerating shapes in the fast sygus enumerator, which is required for a new algorithm for sygus solution reconstruction.

This also adds a builtinToSygus backwards mapping that is required for that algorithm as well.

Note this also changes the implementation of mkFreeVar in sygus term database from skolem to bound variable, which is required to do proper caching for expr::hasBoundVar.

5 files changed, 215 insertions, 5 deletions

diff --git a/src/theory/datatypes/sygus_datatype_utils.cpp b/src/theory/datatypes/sygus_datatype_utils.cpp
index 8ff0f8db2..bd14f8a2c 100644
--- a/src/theory/datatypes/sygus_datatype_utils.cpp
+++ b/src/theory/datatypes/sygus_datatype_utils.cpp
@@ -335,6 +335,16 @@ struct SygusToBuiltinVarAttributeId
 typedef expr::Attribute<SygusToBuiltinVarAttributeId, Node>
     SygusToBuiltinVarAttribute;
 
+// A variant of the above attribute for cases where we introduce a fresh
+// variable. This is to support sygusToBuiltin on non-constant sygus terms,
+// where sygus variables should be mapped to canonical builtin variables.
+// It is important to cache this so that sygusToBuiltin is deterministic.
+struct BuiltinVarToSygusAttributeId
+{
+};
+typedef expr::Attribute<BuiltinVarToSygusAttributeId, Node>
+    BuiltinVarToSygusAttribute;
+
 Node sygusToBuiltin(Node n, bool isExternal)
 {
   std::unordered_map<TNode, Node, TNodeHashFunction> visited;
@@ -388,6 +398,9 @@ Node sygusToBuiltin(Node n, bool isExternal)
           SygusToBuiltinVarAttribute stbv;
           cur.setAttribute(stbv, var);
           visited[cur] = var;
+          // create backwards mapping
+          BuiltinVarToSygusAttribute bvtsa;
+          var.setAttribute(bvtsa, cur);
         }
       }
       else
@@ -549,6 +562,16 @@ Node sygusToBuiltinEval(Node n, const std::vector<Node>& args)
   return visited[n];
 }
 
+Node builtinVarToSygus(Node v)
+{
+  BuiltinVarToSygusAttribute bvtsa;
+  if (v.hasAttribute(bvtsa))
+  {
+    return v.getAttribute(bvtsa);
+  }
+  return Node::null();
+}
+
 void getFreeSymbolsSygusType(TypeNode sdt,
                              std::unordered_set<Node, NodeHashFunction>& syms)
 {
diff --git a/src/theory/datatypes/sygus_datatype_utils.h b/src/theory/datatypes/sygus_datatype_utils.h
index 88ee6d33b..d3d9a6210 100644
--- a/src/theory/datatypes/sygus_datatype_utils.h
+++ b/src/theory/datatypes/sygus_datatype_utils.h
@@ -154,12 +154,21 @@ Node applySygusArgs(const DType& dt,
  * that was provided. This includes the use of defined functions. This argument
  * should typically be false, unless we are e.g. exporting the value of the
  * term as a final solution.
- * 
+ *
  * If n is not constant, then its non-constant subterms that have sygus
  * datatype types are replaced by fresh variables (of the same name, if that
  * subterm is a variable, and having arbitrary name otherwise).
  */
 Node sygusToBuiltin(Node n, bool isExternal = false);
+
+/**
+ * Builtin variable to sygus. Converts from builtin variables introduced by
+ * the method above to their source, which is a sygus variable. It should
+ * be the case that v is a variable introduced by the above method, or otherwise
+ * null is returned.
+ */
+Node builtinVarToSygus(Node v);
+
 /** Sygus to builtin eval
  *
  * This method returns the rewritten form of (DT_SYGUS_EVAL n args). Notice that
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
index 86bf53b23..dcdf0b187 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/sygus/sygus_enumerator.h"
 
+#include "expr/node_algorithm.h"
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
@@ -27,8 +28,14 @@ namespace quantifiers {
 
 SygusEnumerator::SygusEnumerator(TermDbSygus* tds,
                                  SynthConjecture* p,
-                                 SygusStatistics& s)
-    : d_tds(tds), d_parent(p), d_stats(s), d_tlEnum(nullptr), d_abortSize(-1)
+                                 SygusStatistics& s,
+                                 bool enumShapes)
+    : d_tds(tds),
+      d_parent(p),
+      d_stats(s),
+      d_enumShapes(enumShapes),
+      d_tlEnum(nullptr),
+      d_abortSize(-1)
 {
 }
 
@@ -142,6 +149,8 @@ Node SygusEnumerator::getCurrent()
   return ret;
 }
 
+bool SygusEnumerator::isEnumShapes() const { return d_enumShapes; }
+
 SygusEnumerator::TermCache::TermCache()
     : d_tds(nullptr),
       d_eec(nullptr),
@@ -595,6 +604,8 @@ SygusEnumerator::TermEnum* SygusEnumerator::getMasterEnumForType(TypeNode tn)
 
 SygusEnumerator::TermEnumMaster::TermEnumMaster()
     : TermEnum(),
+      d_enumShapes(false),
+      d_enumShapesInit(false),
       d_isIncrementing(false),
       d_currTermSet(false),
       d_consClassNum(0),
@@ -609,6 +620,7 @@ bool SygusEnumerator::TermEnumMaster::initialize(SygusEnumerator* se,
                                                  TypeNode tn)
 {
   Trace("sygus-enum-debug") << "master(" << tn << "): init...\n";
+  d_tds = se->d_tds;
   d_se = se;
   d_tn = tn;
 
@@ -617,6 +629,8 @@ bool SygusEnumerator::TermEnumMaster::initialize(SygusEnumerator* se,
   d_consClassNum = 0;
   d_currChildSize = 0;
   d_ccCons.clear();
+  d_enumShapes = se->isEnumShapes();
+  d_enumShapesInit = false;
   d_isIncrementing = false;
   d_currTermSet = false;
   bool ret = increment();
@@ -651,6 +665,11 @@ Node SygusEnumerator::TermEnumMaster::getCurrent()
     }
     children.push_back(cc);
   }
+  if (d_enumShapes)
+  {
+    // ensure all variables are unique
+    childrenToShape(children);
+  }
   d_currTerm = NodeManager::currentNM()->mkNode(APPLY_CONSTRUCTOR, children);
   return d_currTerm;
 }
@@ -693,6 +712,17 @@ bool SygusEnumerator::TermEnumMaster::incrementInternal()
   unsigned ncc = tc.getLastConstructorClassIndexForWeight(d_currSize);
   Trace("sygus-enum-debug2") << "Last constructor class " << d_currSize << ": "
                              << ncc << std::endl;
+  // If we are enumerating shapes, the first enumerated term is a free variable.
+  if (d_enumShapes && !d_enumShapesInit)
+  {
+    Node fv = d_tds->getFreeVar(d_tn, 0);
+    d_enumShapesInit = true;
+    d_currTermSet = true;
+    d_currTerm = fv;
+    // must add to term cache
+    tc.addTerm(fv);
+    return true;
+  }
 
   // have we initialized the current constructor class?
   while (d_ccCons.empty() && d_consClassNum < ncc)
@@ -995,6 +1025,117 @@ bool SygusEnumerator::TermEnumMaster::initializeChild(unsigned i,
   return true;
 }
 
+void SygusEnumerator::TermEnumMaster::childrenToShape(
+    std::vector<Node>& children)
+{
+  if (children.size() <= 2)
+  {
+    // don't need to convert constants and unary applications
+    return;
+  }
+  std::map<TypeNode, int> vcounter;
+  // Buffered child, so that we only compute vcounter if there are more than
+  // one children with free variables, since otherwise there is no change.
+  // For example, if we are given { C, (+ x1 x2), 1 }, we buffer child (+ x1 x2)
+  // noting that it has free variables. We proceed with processing the remaining
+  // children, and note that no other child contains free variables, and hence
+  // no change is necessary (since by construction, all children have the
+  // property of having unique variable subterms). On the other hand if the
+  // last child above was x1, then this would trigger us to convert (+ x1 x2)
+  // while computing vcounter, and subsequently update x1 to x3 to obtain
+  // { C, (+ x1 x2), x3 }.
+  // Have we set the buffer child index
+  bool bufferChildSet = false;
+  // Have we processed the buffer child index
+  bool bufferChildProcessed = false;
+  // The buffer child index
+  size_t bufferChild = 0;
+  for (size_t i = 1, nchildren = children.size(); i < nchildren; i++)
+  {
+    if (!expr::hasBoundVar(children[i]))
+    {
+      // don't need to care about expressions with no bound variables
+      continue;
+    }
+    else if (!bufferChildSet)
+    {
+      bufferChild = i;
+      bufferChildSet = true;
+      continue;
+    }
+    else if (!bufferChildProcessed)
+    {
+      // process the buffer child
+      children[bufferChild] = convertShape(children[bufferChild], vcounter);
+      bufferChildProcessed = true;
+    }
+    children[i] = convertShape(children[i], vcounter);
+  }
+}
+
+Node SygusEnumerator::TermEnumMaster::convertShape(
+    Node n, std::map<TypeNode, int>& vcounter)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  std::unordered_map<TNode, Node, TNodeHashFunction> visited;
+  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+  std::vector<TNode> visit;
+  TNode cur;
+  visit.push_back(n);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    it = visited.find(cur);
+
+    if (it == visited.end())
+    {
+      if (cur.isVar())
+      {
+        // do the conversion
+        visited[cur] = d_tds->getFreeVarInc(cur.getType(), vcounter);
+      }
+      else if (!expr::hasBoundVar(cur))
+      {
+        // no bound variables, no change
+        visited[cur] = cur;
+      }
+      else
+      {
+        visited[cur] = Node::null();
+        visit.push_back(cur);
+        visit.insert(visit.end(), cur.begin(), cur.end());
+      }
+    }
+    else if (it->second.isNull())
+    {
+      Node ret = cur;
+      bool childChanged = false;
+      std::vector<Node> children;
+      if (cur.getMetaKind() == metakind::PARAMETERIZED)
+      {
+        children.push_back(cur.getOperator());
+      }
+      for (const Node& cn : cur)
+      {
+        it = visited.find(cn);
+        Assert(it != visited.end());
+        Assert(!it->second.isNull());
+        childChanged = childChanged || cn != it->second;
+        children.push_back(it->second);
+      }
+      if (childChanged)
+      {
+        ret = nm->mkNode(cur.getKind(), children);
+      }
+      visited[cur] = ret;
+    }
+  } while (!visit.empty());
+  Assert(visited.find(n) != visited.end());
+  Assert(!visited.find(n)->second.isNull());
+  return visited[n];
+}
+
 SygusEnumerator::TermEnumMasterInterp::TermEnumMasterInterp(TypeNode tn)
     : TermEnum(), d_te(tn), d_currNumConsts(0), d_nextIndexEnd(0)
 {
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.h b/src/theory/quantifiers/sygus/sygus_enumerator.h
index 4bf4fb332..1c56b24ef 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator.h
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.h
@@ -40,11 +40,25 @@ class SygusPbe;
  * builtin terms (TermDb::sygusToBuiltin) can be shown to be equivalent via
  * rewriting. It enumerates terms in order of sygus term size
  * (TermDb::getSygusTermSize).
+ *
+ * It also can be configured to enumerates sygus terms with free variables,
+ * (as opposed to variables bound in the formal arguments list of the
+ * function-to-synthesize), where each free variable appears in exactly one
+ * subterm. For grammar:
+ *   S -> 0 | 1 | x | S+S
+ * this enumerator will generate the stream:
+ *   z1, C_0, C_1, C_x, C_+(z1, z2), C_+(z1, C_1), C_+(C_1, C_1) ...
+ * and so on, where z1 and z2 are variables of sygus datatype type S. We call
+ * these "shapes". This feature can be enabled by setting enumShapes to true
+ * in the constructor below.
  */
 class SygusEnumerator : public EnumValGenerator
 {
  public:
-  SygusEnumerator(TermDbSygus* tds, SynthConjecture* p, SygusStatistics& s);
+  SygusEnumerator(TermDbSygus* tds,
+                  SynthConjecture* p,
+                  SygusStatistics& s,
+                  bool enumShapes = false);
   ~SygusEnumerator() {}
   /** initialize this class with enumerator e */
   void initialize(Node e) override;
@@ -54,6 +68,8 @@ class SygusEnumerator : public EnumValGenerator
   bool increment() override;
   /** Get the next concrete value generated by this class. */
   Node getCurrent() override;
+  /** Are we enumerating shapes? */
+  bool isEnumShapes() const;
 
  private:
   /** pointer to term database sygus */
@@ -62,6 +78,8 @@ class SygusEnumerator : public EnumValGenerator
   SynthConjecture* d_parent;
   /** reference to the statistics of parent */
   SygusStatistics& d_stats;
+  /** Whether we are enumerating shapes */
+  bool d_enumShapes;
   /** Term cache
    *
    * This stores a list of terms for a given sygus type. The key features of
@@ -340,6 +358,12 @@ class SygusEnumerator : public EnumValGenerator
     bool increment() override;
 
    private:
+    /** pointer to term database sygus */
+    TermDbSygus* d_tds;
+    /** are we enumerating shapes? */
+    bool d_enumShapes;
+    /** have we initialized the shape enumeration? */
+    bool d_enumShapesInit;
     /** are we currently inside a increment() call? */
     bool d_isIncrementing;
     /** cache for getCurrent() */
@@ -393,6 +417,19 @@ class SygusEnumerator : public EnumValGenerator
     bool initializeChild(unsigned i, unsigned sizeMin);
     /** increment internal, helper for increment() */
     bool incrementInternal();
+    /**
+     * The vector children is a set of terms given to
+     *    NodeManager::mkNode(APPLY_CONSTRUCTOR, children)
+     * This converts children so that all sygus free variables are unique. Note
+     * that the first child is a constructor operator and should be skipped.
+     */
+    void childrenToShape(std::vector<Node>& children);
+    /**
+     * Convert n into shape based on the variable counters. For example if
+     * vcounter is { Int -> 7 }, then (+ x1 x2) is converted to (+ x7 x8) and
+     * vouncter is updated to { Int -> 9 }.
+     */
+    Node convertShape(Node n, std::map<TypeNode, int>& vcounter);
   };
   /** an interpreted value enumerator
    *
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index c2a02e715..ff1b172e9 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -89,7 +89,7 @@ TNode TermDbSygus::getFreeVar( TypeNode tn, int i, bool useSygusType ) {
       ss << "fv_" << tn << "_" << i;
     }
     Assert(!vtn.isNull());
-    Node v = nm->mkSkolem(ss.str(), vtn, "for sygus invariance testing");
+    Node v = nm->mkBoundVar(ss.str(), vtn);
     // store its id, which is unique per builtin type, regardless of how it is
     // otherwise cached.
     d_fvId[v] = d_fvTypeIdCounter[builtinType];