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

Preparation for further developing CegisUnif

1 files changed, 1 insertions, 72 deletions

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
  *