diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-11-27 15:39:13 -0600 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-11-27 13:39:13 -0800 |
commit | a2bba0806dab0e0d4728bbba8e4e6b4160335eeb (patch) | |
tree | 76a9508f241908561176d2105a59195137944ec6 /src/theory/quantifiers/term_database.h | |
parent | 711234e01a17289d1fa4af3574ddf5d6de2405a1 (diff) |
Make (T)NodeTrie a general utility (#2489)
This moves quantifiers::TermArgTrie in src/theory/quantifiers/term_database to (T)NodeTrie in src/expr, and cleans up all references to it.
Diffstat (limited to 'src/theory/quantifiers/term_database.h')
-rw-r--r-- | src/theory/quantifiers/term_database.h | 78 |
1 files changed, 8 insertions, 70 deletions
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 7e3806e8c..cc9a24d08 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -21,9 +21,10 @@ #include <unordered_set> #include "expr/attribute.h" +#include "expr/node_trie.h" +#include "theory/quantifiers/quant_util.h" #include "theory/theory.h" #include "theory/type_enumerator.h" -#include "theory/quantifiers/quant_util.h" namespace CVC4 { namespace theory { @@ -37,69 +38,6 @@ namespace inst{ namespace quantifiers { -/** Term arg trie class -* -* This also referred to as a "term index" or a "signature table". -* -* This data structure stores a set expressions, indexed by representatives of -* their arguments. -* -* For example, consider the equivalence classes : -* -* { a, d, f( d, c ), f( a, c ) } -* { b, f( b, d ) } -* { c, f( b, b ) } -* -* where the first elements ( a, b, c ) are the representatives of these classes. -* The TermArgTrie t we may build for f is : -* -* t : -* t.d_data[a] : -* t.d_data[a].d_data[c] : -* t.d_data[a].d_data[c].d_data[f(d,c)] : (leaf) -* t.d_data[b] : -* t.d_data[b].d_data[b] : -* t.d_data[b].d_data[b].d_data[f(b,b)] : (leaf) -* t.d_data[b].d_data[d] : -* t.d_data[b].d_data[d].d_data[f(b,d)] : (leaf) -* -* Leaf nodes store the terms that are indexed by the arguments, for example -* term f(d,c) is indexed by the representative arguments (a,c), and is stored -* as a the (single) key in the data of t.d_data[a].d_data[c]. -*/ -class TermArgTrie { -public: - /** the data */ - std::map< TNode, TermArgTrie > d_data; -public: - /** for leaf nodes : does this trie have data? */ - bool hasNodeData() { return !d_data.empty(); } - /** for leaf nodes : get term corresponding to this leaf */ - TNode getNodeData() { return d_data.begin()->first; } - /** exists term - * Returns the term that is indexed by reps, if one exists, or - * or returns null otherwise. - */ - TNode existsTerm(std::vector<TNode>& reps, int argIndex = 0); - /** add or get term - * Returns the term that is previously indexed by reps, if one exists, or - * Adds n to the trie, indexed by reps, and returns n. - */ - TNode addOrGetTerm(TNode n, std::vector<TNode>& reps, int argIndex = 0); - /** add term - * Returns false if a term is previously indexed by reps. - * Returns true if no term is previously indexed by reps, - * and adds n to the trie, indexed by reps, and returns n. - */ - bool addTerm(TNode n, std::vector<TNode>& reps, int argIndex = 0); - /** debug print this trie */ - void debugPrint(const char* c, Node n, unsigned depth = 0); - /** clear all data from this trie */ - void clear() { d_data.clear(); } - /** is empty */ - bool empty() { return d_data.empty(); } -};/* class TermArgTrie */ - namespace fmcheck { class FullModelChecker; } @@ -121,12 +59,12 @@ class TermGenEnv; * The primary responsibilities for this class are to : * (1) Maintain a list of all ground terms that exist in the quantifier-free * solvers, as notified through the master equality engine. - * (2) Build TermArgTrie objects that index all ground terms, per operator. + * (2) Build TNodeTrie objects that index all ground terms, per operator. * * Like other utilities, its reset(...) function is called * at the beginning of full or last call effort checks. * This initializes the database for the round. However, - * notice that TermArgTrie objects are computed + * notice that TNodeTrie objects are computed * lazily for performance reasons. */ class TermDb : public QuantifiersUtil { @@ -213,10 +151,10 @@ class TermDb : public QuantifiersUtil { */ Node getMatchOperator(Node n); /** get term arg index for all f-applications in the current context */ - TermArgTrie* getTermArgTrie(Node f); + TNodeTrie* getTermArgTrie(Node f); /** get the term arg trie for f-applications in the equivalence class of eqc. */ - TermArgTrie* getTermArgTrie(Node eqc, Node f); + TNodeTrie* getTermArgTrie(Node eqc, Node f); /** get congruent term * If possible, returns a term t such that: * (1) t is a term that is currently indexed by this database, @@ -358,8 +296,8 @@ class TermDb : public QuantifiersUtil { /** mapping from terms to representatives of their arguments */ std::map< TNode, std::vector< TNode > > d_arg_reps; /** map from operators to trie */ - std::map< Node, TermArgTrie > d_func_map_trie; - std::map< Node, TermArgTrie > d_func_map_eqc_trie; + std::map<Node, TNodeTrie> d_func_map_trie; + std::map<Node, TNodeTrie> d_func_map_eqc_trie; /** mapping from operators to their representative relevant domains */ std::map< Node, std::map< unsigned, std::vector< Node > > > d_func_map_rel_dom; /** has map */ |