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.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/quant_conflict_find.cpp')
-rw-r--r-- | src/theory/quantifiers/quant_conflict_find.cpp | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 95ec24df9..5b57af14c 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1293,7 +1293,7 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) { Assert( isHandledUfTerm( d_n ) ); TNode f = getMatchOperator( p, d_n ); Debug("qcf-match-debug") << " reset: Var will match operators of " << f << std::endl; - TermArgTrie * qni = p->getTermDatabase()->getTermArgTrie( Node::null(), f ); + TNodeTrie* qni = p->getTermDatabase()->getTermArgTrie(Node::null(), f); if (qni == nullptr || qni->empty()) { //inform irrelevant quantifiers @@ -1672,7 +1672,8 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) { }else{ //binding a variable d_qni_bound[index] = repVar; - std::map< TNode, TermArgTrie >::iterator it = d_qn[index]->d_data.begin(); + std::map<TNode, TNodeTrie>::iterator it = + d_qn[index]->d_data.begin(); if( it != d_qn[index]->d_data.end() ) { d_qni.push_back( it ); //set the match @@ -1699,7 +1700,8 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) { } if( !val.isNull() ){ //constrained by val - std::map< TNode, TermArgTrie >::iterator it = d_qn[index]->d_data.find( val ); + std::map<TNode, TNodeTrie>::iterator it = + d_qn[index]->d_data.find(val); if( it!=d_qn[index]->d_data.end() ){ Debug("qcf-match-debug") << " Match" << std::endl; d_qni.push_back( it ); |