diff options
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 47 |
1 files changed, 30 insertions, 17 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index e8b753768..9da6fd277 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -24,7 +24,6 @@ #include "smt/logic_exception.h" #include "smt/smt_statistics_registry.h" #include "theory/ext_theory.h" -#include "theory/quantifiers/term_database.h" #include "theory/rewriter.h" #include "theory/strings/theory_strings_rewriter.h" #include "theory/strings/type_enumerator.h" @@ -1118,11 +1117,15 @@ void TheoryStrings::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { } } -void TheoryStrings::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth ) { +void TheoryStrings::addCarePairs(TNodeTrie* t1, + TNodeTrie* t2, + unsigned arity, + unsigned depth) +{ if( depth==arity ){ if( t2!=NULL ){ - Node f1 = t1->getNodeData(); - Node f2 = t2->getNodeData(); + Node f1 = t1->getData(); + Node f2 = t2->getData(); if( !d_equalityEngine.areEqual( f1, f2 ) ){ Trace("strings-cg-debug") << "TheoryStrings::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl; vector< pair<TNode, TNode> > currentPairs; @@ -1151,13 +1154,17 @@ void TheoryStrings::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::Te if( t2==NULL ){ if( depth<(arity-1) ){ //add care pairs internal to each child - for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){ - addCarePairs( &it->second, NULL, arity, depth+1 ); + for (std::pair<const TNode, TNodeTrie>& tt : t1->d_data) + { + addCarePairs(&tt.second, nullptr, arity, depth + 1); } } //add care pairs based on each pair of non-disequal arguments - for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){ - std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = it; + for (std::map<TNode, TNodeTrie>::iterator it = t1->d_data.begin(); + it != t1->d_data.end(); + ++it) + { + std::map<TNode, TNodeTrie>::iterator it2 = it; ++it2; for( ; it2 != t1->d_data.end(); ++it2 ){ if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){ @@ -1169,11 +1176,15 @@ void TheoryStrings::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::Te } }else{ //add care pairs based on product of indices, non-disequal arguments - for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){ - for( std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = t2->d_data.begin(); it2 != t2->d_data.end(); ++it2 ){ - if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){ - if( !areCareDisequal(it->first, it2->first) ){ - addCarePairs( &it->second, &it2->second, arity, depth+1 ); + for (std::pair<const TNode, TNodeTrie>& tt1 : t1->d_data) + { + for (std::pair<const TNode, TNodeTrie>& tt2 : t2->d_data) + { + if (!d_equalityEngine.areDisequal(tt1.first, tt2.first, false)) + { + if (!areCareDisequal(tt1.first, tt2.first)) + { + addCarePairs(&tt1.second, &tt2.second, arity, depth + 1); } } } @@ -1185,7 +1196,7 @@ void TheoryStrings::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::Te void TheoryStrings::computeCareGraph(){ //computing the care graph here is probably still necessary, due to operators that take non-string arguments TODO: verify Trace("strings-cg") << "TheoryStrings::computeCareGraph(): Build term indices..." << std::endl; - std::map< Node, quantifiers::TermArgTrie > index; + std::map<Node, TNodeTrie> index; std::map< Node, unsigned > arity; unsigned functionTerms = d_functionsTerms.size(); for (unsigned i = 0; i < functionTerms; ++ i) { @@ -1206,9 +1217,11 @@ void TheoryStrings::computeCareGraph(){ } } //for each index - for( std::map< Node, quantifiers::TermArgTrie >::iterator itii = index.begin(); itii != index.end(); ++itii ){ - Trace("strings-cg") << "TheoryStrings::computeCareGraph(): Process index " << itii->first << "..." << std::endl; - addCarePairs( &itii->second, NULL, arity[ itii->first ], 0 ); + for (std::pair<const Node, TNodeTrie>& tt : index) + { + Trace("strings-cg") << "TheoryStrings::computeCareGraph(): Process index " + << tt.first << "..." << std::endl; + addCarePairs(&tt.second, nullptr, arity[tt.first], 0); } } |