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 \
--- /dev/null
+/********************* */
+/*! \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 = <->d_children[e];
+ index = index + 1;
+ }
+ return Node::null();
+}
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \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 */
#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"
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 = <->d_children[e];
- index = index + 1;
- }
- return Node::null();
-}
-
SygusSampler::SygusSampler()
: d_tds(nullptr), d_use_sygus_type(false), d_is_valid(false)
{
#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
*
projects / cvc5.git / commitdiff