Move Lazy trie datastructure to its own file (#1871)

Preparation for further developing CegisUnif

4 files changed, 168 insertions, 114 deletions

diff --git a/src/theory/quantifiers/lazy_trie.cpp b/src/theory/quantifiers/lazy_trie.cpp
new file mode 100644
index 000000000..5a63024b8
--- /dev/null
+++ b/src/theory/quantifiers/lazy_trie.cpp
@@ -0,0 +1,65 @@
+/*********************                                                        */
+/*! \file lazy_trie.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of lazy trie
+ **/
+
+#include "theory/quantifiers/lazy_trie.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+Node LazyTrie::add(Node n,
+                   LazyTrieEvaluator* ev,
+                   unsigned index,
+                   unsigned ntotal,
+                   bool forceKeep)
+{
+  LazyTrie* lt = this;
+  while (lt != NULL)
+  {
+    if (index == ntotal)
+    {
+      // lazy child holds the leaf data
+      if (lt->d_lazy_child.isNull() || forceKeep)
+      {
+        lt->d_lazy_child = n;
+      }
+      return lt->d_lazy_child;
+    }
+    std::vector<Node> ex;
+    if (lt->d_children.empty())
+    {
+      if (lt->d_lazy_child.isNull())
+      {
+        // no one has been here, we are done
+        lt->d_lazy_child = n;
+        return lt->d_lazy_child;
+      }
+      // evaluate the lazy child
+      Node e_lc = ev->evaluate(lt->d_lazy_child, index);
+      // store at next level
+      lt->d_children[e_lc].d_lazy_child = lt->d_lazy_child;
+      // replace
+      lt->d_lazy_child = Node::null();
+    }
+    // recurse
+    Node e = ev->evaluate(n, index);
+    lt = &lt->d_children[e];
+    index = index + 1;
+  }
+  return Node::null();
+}
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
diff --git a/src/theory/quantifiers/lazy_trie.h b/src/theory/quantifiers/lazy_trie.h
new file mode 100644
index 000000000..b114f55df
--- /dev/null
+++ b/src/theory/quantifiers/lazy_trie.h
@@ -0,0 +1,101 @@
+/*********************                                                        */
+/*! \file lazy_trie.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief lazy trie
+ **/
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__LAZY_TRIE_H
+#define __CVC4__THEORY__QUANTIFIERS__LAZY_TRIE_H
+
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** abstract evaluator class
+ *
+ * This class is used for the LazyTrie data structure below.
+ */
+class LazyTrieEvaluator
+{
+ public:
+  virtual ~LazyTrieEvaluator() {}
+  virtual Node evaluate(Node n, unsigned index) = 0;
+};
+
+/** LazyTrie
+ *
+ * This is a trie where terms are added in a lazy fashion. This data structure
+ * is useful, for instance, when we are only interested in when two terms
+ * map to the same node in the trie but we need not care about computing
+ * exactly where they are.
+ *
+ * In other words, when a term n is added to this trie, we do not insist
+ * that n is placed at the maximal depth of the trie. Instead, we place n at a
+ * minimal depth node that has no children. In this case we say n is partially
+ * evaluated in this trie.
+ *
+ * This class relies on an abstract evaluator interface above, which evaluates
+ * nodes for indices.
+ *
+ * For example, say we have terms a, b, c and an evaluator ev where:
+ *   ev->evaluate( a, 0,1,2 ) = 0, 5, 6
+ *   ev->evaluate( b, 0,1,2 ) = 1, 3, 0
+ *   ev->evaluate( c, 0,1,2 ) = 1, 3, 2
+ * After adding a to the trie, we get:
+ *   root: a
+ * After adding b to the resulting trie, we get:
+ *   root: null
+ *     d_children[0]: a
+ *     d_children[1]: b
+ * After adding c to the resulting trie, we get:
+ *   root: null
+ *     d_children[0]: a
+ *     d_children[1]: null
+ *       d_children[3]: null
+ *         d_children[0] : b
+ *         d_children[2] : c
+ * Notice that we need not call ev->evalute( a, 1 ) and ev->evalute( a, 2 ).
+ */
+class LazyTrie
+{
+ public:
+  LazyTrie() {}
+  ~LazyTrie() {}
+  /** the data at this node, which may be partially evaluated */
+  Node d_lazy_child;
+  /** the children of this node */
+  std::map<Node, LazyTrie> d_children;
+  /** clear the trie */
+  void clear() { d_children.clear(); }
+  /** add n to the trie
+   *
+   * This function returns a node that is mapped to the same node in the trie
+   * if one exists, or n otherwise.
+   *
+   * ev is an evaluator which determines where n is placed in the trie
+   * index is the depth of this node
+   * ntotal is the maximal depth of the trie
+   * forceKeep is whether we wish to force that n is chosen as a representative
+   */
+  Node add(Node n,
+           LazyTrieEvaluator* ev,
+           unsigned index,
+           unsigned ntotal,
+           bool forceKeep);
+};
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__LAZY_TRIE_H */
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index 757256fc3..fb4f7e831 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -17,6 +17,7 @@
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
+#include "theory/quantifiers/lazy_trie.h"
 #include "util/bitvector.h"
 #include "util/random.h"
 
@@ -24,48 +25,6 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-Node LazyTrie::add(Node n,
-                   LazyTrieEvaluator* ev,
-                   unsigned index,
-                   unsigned ntotal,
-                   bool forceKeep)
-{
-  LazyTrie* lt = this;
-  while (lt != NULL)
-  {
-    if (index == ntotal)
-    {
-      // lazy child holds the leaf data
-      if (lt->d_lazy_child.isNull() || forceKeep)
-      {
-        lt->d_lazy_child = n;
-      }
-      return lt->d_lazy_child;
-    }
-    std::vector<Node> ex;
-    if (lt->d_children.empty())
-    {
-      if (lt->d_lazy_child.isNull())
-      {
-        // no one has been here, we are done
-        lt->d_lazy_child = n;
-        return lt->d_lazy_child;
-      }
-      // evaluate the lazy child
-      Node e_lc = ev->evaluate(lt->d_lazy_child, index);
-      // store at next level
-      lt->d_children[e_lc].d_lazy_child = lt->d_lazy_child;
-      // replace
-      lt->d_lazy_child = Node::null();
-    }
-    // recurse
-    Node e = ev->evaluate(n, index);
-    lt = &lt->d_children[e];
-    index = index + 1;
-  }
-  return Node::null();
-}
-
 SygusSampler::SygusSampler()
     : d_tds(nullptr), d_use_sygus_type(false), d_is_valid(false)
 {
diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h
index b741b60d4..5e0a24dd2 100644
--- a/src/theory/quantifiers/sygus_sampler.h
+++ b/src/theory/quantifiers/sygus_sampler.h
@@ -19,84 +19,13 @@
 
 #include <map>
 #include "theory/quantifiers/dynamic_rewrite.h"
+#include "theory/quantifiers/lazy_trie.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 
 namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-/** abstract evaluator class
- *
- * This class is used for the LazyTrie data structure below.
- */
-class LazyTrieEvaluator
-{
- public:
-  virtual ~LazyTrieEvaluator() {}
-  virtual Node evaluate(Node n, unsigned index) = 0;
-};
-
-/** LazyTrie
- *
- * This is a trie where terms are added in a lazy fashion. This data structure
- * is useful, for instance, when we are only interested in when two terms
- * map to the same node in the trie but we need not care about computing
- * exactly where they are.
- *
- * In other words, when a term n is added to this trie, we do not insist
- * that n is placed at the maximal depth of the trie. Instead, we place n at a
- * minimal depth node that has no children. In this case we say n is partially
- * evaluated in this trie.
- *
- * This class relies on an abstract evaluator interface above, which evaluates
- * nodes for indices.
- *
- * For example, say we have terms a, b, c and an evaluator ev where:
- *   ev->evaluate( a, 0,1,2 ) = 0, 5, 6
- *   ev->evaluate( b, 0,1,2 ) = 1, 3, 0
- *   ev->evaluate( c, 0,1,2 ) = 1, 3, 2
- * After adding a to the trie, we get:
- *   root: a
- * After adding b to the resulting trie, we get:
- *   root: null
- *     d_children[0]: a
- *     d_children[1]: b
- * After adding c to the resulting trie, we get:
- *   root: null
- *     d_children[0]: a
- *     d_children[1]: null
- *       d_children[3]: null
- *         d_children[0] : b
- *         d_children[2] : c
- * Notice that we need not call ev->evalute( a, 1 ) and ev->evalute( a, 2 ).
- */
-class LazyTrie
-{
- public:
-  LazyTrie() {}
-  ~LazyTrie() {}
-  /** the data at this node, which may be partially evaluated */
-  Node d_lazy_child;
-  /** the children of this node */
-  std::map<Node, LazyTrie> d_children;
-  /** clear the trie */
-  void clear() { d_children.clear(); }
-  /** add n to the trie
-   *
-   * This function returns a node that is mapped to the same node in the trie
-   * if one exists, or n otherwise.
-   *
-   * ev is an evaluator which determines where n is placed in the trie
-   * index is the depth of this node
-   * ntotal is the maximal depth of the trie
-   * forceKeep is whether we wish to force that n is chosen as a representative
-   */
-  Node add(Node n,
-           LazyTrieEvaluator* ev,
-           unsigned index,
-           unsigned ntotal,
-           bool forceKeep);
-};
 
 /** SygusSampler
  *