1 files changed, 1 insertions, 42 deletions
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)
 {