diff options
Diffstat (limited to 'src/theory/quantifiers/ematching')
3 files changed, 16 insertions, 15 deletions
diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp index 3f404c17f..612a1938a 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.cpp +++ b/src/theory/quantifiers/ematching/candidate_generator.cpp @@ -57,7 +57,7 @@ void CandidateGeneratorQE::reset( Node eqc ){ }else{ eq::EqualityEngine* ee = d_qe->getEqualityQuery()->getEngine(); if( ee->hasTerm( eqc ) ){ - quantifiers::TermArgTrie * tat = d_qe->getTermDatabase()->getTermArgTrie( eqc, d_op ); + TNodeTrie* tat = d_qe->getTermDatabase()->getTermArgTrie(eqc, d_op); if( tat ){ //create an equivalence class iterator in eq class eqc Node rep = ee->getRepresentative( eqc ); diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index 646208ec6..f26df5b79 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -1028,7 +1028,7 @@ int InstMatchGeneratorSimple::addInstantiations(Node q, Trigger* tparent) { int addedLemmas = 0; - quantifiers::TermArgTrie* tat; + TNodeTrie* tat; if( d_eqc.isNull() ){ tat = qe->getTermDatabase()->getTermArgTrie( d_op ); }else{ @@ -1040,10 +1040,12 @@ int InstMatchGeneratorSimple::addInstantiations(Node q, if (tat && !qe->inConflict()) { Node r = qe->getEqualityQuery()->getRepresentative(d_eqc); - for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){ - if( it->first!=r ){ + for (std::pair<const TNode, TNodeTrie>& t : tat->d_data) + { + if (t.first != r) + { InstMatch m( q ); - addInstantiations( m, qe, addedLemmas, 0, &(it->second) ); + addInstantiations(m, qe, addedLemmas, 0, &(t.second)); if( qe->inConflict() ){ break; } @@ -1066,13 +1068,13 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, unsigned argIndex, - quantifiers::TermArgTrie* tat) + TNodeTrie* tat) { Debug("simple-trigger-debug") << "Add inst " << argIndex << " " << d_match_pattern << std::endl; if (argIndex == d_match_pattern.getNumChildren()) { Assert( !tat->d_data.empty() ); - TNode t = tat->getNodeData(); + TNode t = tat->getData(); Debug("simple-trigger") << "Actual term is " << t << std::endl; //convert to actual used terms for (std::map<unsigned, int>::iterator it = d_var_num.begin(); @@ -1096,14 +1098,15 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m, if( d_match_pattern[argIndex].getKind()==INST_CONSTANT ){ int v = d_var_num[argIndex]; if( v!=-1 ){ - for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){ - Node t = it->first; + for (std::pair<const TNode, TNodeTrie>& tt : tat->d_data) + { + Node t = tt.first; Node prev = m.get( v ); //using representatives, just check if equal Assert( t.getType().isComparableTo( d_match_pattern_arg_types[argIndex] ) ); if( prev.isNull() || prev==t ){ m.setValue( v, t); - addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) ); + addInstantiations(m, qe, addedLemmas, argIndex + 1, &(tt.second)); m.setValue( v, prev); if( qe->inConflict() ){ break; @@ -1115,7 +1118,7 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m, //inst constant from another quantified formula, treat as ground term TODO: remove this? } Node r = qe->getEqualityQuery()->getRepresentative( d_match_pattern[argIndex] ); - std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.find( r ); + std::map<TNode, TNodeTrie>::iterator it = tat->d_data.find(r); if( it!=tat->d_data.end() ){ addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) ); } diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h index abf269f3e..83d4ce82e 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.h +++ b/src/theory/quantifiers/ematching/inst_match_generator.h @@ -18,15 +18,13 @@ #define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H #include <map> +#include "expr/node_trie.h" #include "theory/quantifiers/inst_match_trie.h" namespace CVC4 { namespace theory { class QuantifiersEngine; -namespace quantifiers{ - class TermArgTrie; -} namespace inst { @@ -662,7 +660,7 @@ class InstMatchGeneratorSimple : public IMGenerator { QuantifiersEngine* qe, int& addedLemmas, unsigned argIndex, - quantifiers::TermArgTrie* tat); + TNodeTrie* tat); };/* class InstMatchGeneratorSimple */ } } |