diff options
Diffstat (limited to 'src/theory/quantifiers/sygus_sampler.h')
-rw-r--r-- | src/theory/quantifiers/sygus_sampler.h | 73 |
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 * |