From b35ed9dd0e1c8361338ba11d2b1532301f540945 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Thu, 3 May 2018 21:40:30 -0500 Subject: [PATCH] Move Lazy trie datastructure to its own file (#1871) Preparation for further developing CegisUnif --- src/Makefile.am | 2 + src/theory/quantifiers/lazy_trie.cpp | 65 +++++++++++++++ src/theory/quantifiers/lazy_trie.h | 101 +++++++++++++++++++++++ src/theory/quantifiers/sygus_sampler.cpp | 43 +--------- src/theory/quantifiers/sygus_sampler.h | 73 +--------------- 5 files changed, 170 insertions(+), 114 deletions(-) create mode 100644 src/theory/quantifiers/lazy_trie.cpp create mode 100644 src/theory/quantifiers/lazy_trie.h diff --git a/src/Makefile.am b/src/Makefile.am index 6cb179b1d..168e1e3b8 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -431,6 +431,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/inst_propagator.h \ theory/quantifiers/inst_strategy_enumerative.cpp \ theory/quantifiers/inst_strategy_enumerative.h \ + theory/quantifiers/lazy_trie.cpp \ + theory/quantifiers/lazy_trie.h \ theory/quantifiers/local_theory_ext.cpp \ theory/quantifiers/local_theory_ext.h \ theory/quantifiers/macros.cpp \ 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 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 = <->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 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 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 = <->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 #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 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 * -- 2.30.2