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/quant_conflict_find.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/quant_conflict_find.h')
| -rw-r--r-- | src/theory/quantifiers/quant_conflict_find.h | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 0469e958b..9fa37a96c 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -22,7 +22,7 @@ #include "context/cdhashmap.h" #include "context/cdlist.h" -#include "theory/quantifiers/term_database.h" +#include "expr/node_trie.h" #include "theory/quantifiers_engine.h" namespace CVC4 { @@ -45,8 +45,8 @@ private: MatchGen * getChild( int i ) { return &d_children[d_children_order[i]]; } //MatchGen * getChild( int i ) { return &d_children[i]; } //current matching information - std::vector< TermArgTrie * > d_qn; - std::vector< std::map< TNode, TermArgTrie >::iterator > d_qni; + std::vector<TNodeTrie*> d_qn; + std::vector<std::map<TNode, TNodeTrie>::iterator> d_qni; bool doMatching( QuantConflictFind * p, QuantInfo * qi ); //for matching : each index is either a variable or a ground term unsigned d_qni_size; |