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/conjecture_generator.cpp | |
| 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/conjecture_generator.cpp')
| -rw-r--r-- | src/theory/quantifiers/conjecture_generator.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 1d2f9a322..7408678e7 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -1630,7 +1630,7 @@ bool TermGenerator::getNextMatch( TermGenEnv * s, TNode eqc, std::map< TypeNode, //initial binding TNode f = s->getTgFunc( d_typ, d_status_num ); Assert( !eqc.isNull() ); - TermArgTrie * tat = s->getTermDatabase()->getTermArgTrie( eqc, f ); + TNodeTrie* tat = s->getTermDatabase()->getTermArgTrie(eqc, f); if( tat ){ d_match_children.push_back( tat->d_data.begin() ); d_match_children_end.push_back( tat->d_data.end() ); |