From b7ae36dbc1d0905a6e59d654431b4b7c0223665e Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 11 Nov 2014 11:38:35 +0100 Subject: [PATCH] Work on synchronizing decision=justification and E-matching. --- .../quantifiers/candidate_generator.cpp | 5 +- src/theory/quantifiers/term_database.cpp | 122 +++++++++++------- src/theory/quantifiers/term_database.h | 6 +- 3 files changed, 82 insertions(+), 51 deletions(-) diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index 29640e18f..a10181c51 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -101,10 +101,11 @@ Node CandidateGeneratorQE::getNextCandidate(){ //get next candidate term in the uf term database while( d_term_itergetTermDatabase()->d_op_map[d_op][d_term_iter]; - //Assert( d_qe->getEqualityQuery()->hasTerm( n ) ); d_term_iter++; if( isLegalCandidate( n ) ){ - return n; + if( d_qe->getTermDatabase()->hasTermCurrent( n ) ){ + return n; + } } } }else if( d_mode==cand_term_eqc ){ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index c35adef6a..ee39b55d9 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -124,7 +124,6 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ if( inst::Trigger::isAtomicTrigger( n ) ){ if( !TermDb::hasInstConstAttr(n) ){ Trace("term-db") << "register term in db " << n << std::endl; - //std::cout << "register trigger term " << n << std::endl; Node op = getOperator( n ); /* int occ = d_op_ccount[op]; @@ -174,10 +173,12 @@ void TermDb::computeUfEqcTerms( TNode f ) { eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine(); for( unsigned i=0; ihasTerm( n ) ? ee->getRepresentative( n ) : n; - d_func_map_eqc_trie[f].d_data[r].addTerm( n, d_arg_reps[n] ); + if( hasTermCurrent( n ) ){ + if( !n.getAttribute(NoMatchAttribute()) ){ + computeArgReps( n ); + TNode r = ee->hasTerm( n ) ? ee->getRepresentative( n ) : n; + d_func_map_eqc_trie[f].d_data[r].addTerm( n, d_arg_reps[n] ); + } } } } @@ -315,52 +316,77 @@ bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, return false; } +bool TermDb::hasTermCurrent( Node n ) { + //return d_quantEngine->getMasterEqualityEngine()->hasTerm( n ); + //return d_has_map.find( n )!=d_has_map.end(); + return true; +} + void TermDb::reset( Theory::Effort effort ){ - int nonCongruentCount = 0; - int congruentCount = 0; - int alreadyCongruentCount = 0; - d_op_nonred_count.clear(); - d_arg_reps.clear(); - d_func_map_trie.clear(); - d_func_map_eqc_trie.clear(); - //rebuild d_func/pred_map_trie for each operation, this will calculate all congruent terms - for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){ - d_op_nonred_count[ it->first ] = 0; - if( !it->second.empty() ){ - for( unsigned i=0; isecond.size(); i++ ){ - Node n = it->second[i]; - //Assert( d_quantEngine->getEqualityQuery()->hasTerm( n ) ); - computeModelBasisArgAttribute( n ); - if( !n.getAttribute(NoMatchAttribute()) ){ - computeArgReps( n ); - if( !d_func_map_trie[ it->first ].addTerm( n, d_arg_reps[n] ) ){ - NoMatchAttribute nma; - n.setAttribute(nma,true); - Debug("term-db-cong") << n << " is redundant." << std::endl; - congruentCount++; - }else{ - nonCongruentCount++; - d_op_nonred_count[ it->first ]++; - } - }else{ - congruentCount++; - alreadyCongruentCount++; - } - } - } - } - Debug("term-db-cong") << "TermDb: Reset" << std::endl; - Debug("term-db-cong") << "Congruent/Non-Congruent = "; - Debug("term-db-cong") << congruentCount << "(" << alreadyCongruentCount << ") / " << nonCongruentCount << std::endl; - if( Debug.isOn("term-db") ){ - Debug("term-db") << "functions : " << std::endl; - for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){ - if( it->second.size()>0 ){ - Debug("term-db") << "- " << it->first << std::endl; - d_func_map_trie[ it->first ].debugPrint("term-db", it->second[0]); + int nonCongruentCount = 0; + int congruentCount = 0; + int alreadyCongruentCount = 0; + int nonRelevantCount = 0; + d_op_nonred_count.clear(); + d_arg_reps.clear(); + d_func_map_trie.clear(); + d_func_map_eqc_trie.clear(); + /* + //compute has map + d_has_map.clear(); + eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); + while( !eqcs_i.isFinished() ){ + TNode r = (*eqcs_i); + eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); + while( !eqc_i.isFinished() ){ + d_has_map[(*eqc_i)] = true; + ++eqc_i; + } + ++eqcs_i; + } + */ + //rebuild d_func/pred_map_trie for each operation, this will calculate all congruent terms + for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){ + d_op_nonred_count[ it->first ] = 0; + if( !it->second.empty() ){ + for( unsigned i=0; isecond.size(); i++ ){ + Node n = it->second[i]; + computeModelBasisArgAttribute( n ); + if( hasTermCurrent( n ) ){ + if( !n.getAttribute(NoMatchAttribute()) ){ + computeArgReps( n ); + if( !d_func_map_trie[ it->first ].addTerm( n, d_arg_reps[n] ) ){ + NoMatchAttribute nma; + n.setAttribute(nma,true); + Trace("term-db-stats-debug") << n << " is redundant." << std::endl; + congruentCount++; + }else{ + nonCongruentCount++; + d_op_nonred_count[ it->first ]++; + } + }else{ + congruentCount++; + alreadyCongruentCount++; + } + }else{ + nonRelevantCount++; } } - } + } + } + Trace("term-db-stats") << "TermDb: Reset" << std::endl; + Trace("term-db-stats") << "Congruent/Non-Congruent/Non-Relevant = "; + Trace("term-db-stats") << congruentCount << "(" << alreadyCongruentCount << ") / " << nonCongruentCount << " / " << nonRelevantCount << std::endl; + if( Debug.isOn("term-db") ){ + Debug("term-db") << "functions : " << std::endl; + for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){ + if( it->second.size()>0 ){ + Debug("term-db") << "- " << it->first << std::endl; + d_func_map_trie[ it->first ].debugPrint("term-db", it->second[0]); + } + } + } } TermArgTrie * TermDb::getTermArgTrie( Node f ) { diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 1d3757d65..3d419ed5c 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -140,6 +140,8 @@ public: std::map< Node, int > d_op_nonred_count; /** map from APPLY_UF operators to ground terms for that operator */ std::map< Node, std::vector< Node > > d_op_map; + /** has map */ + std::map< Node, bool > d_has_map; /** map from APPLY_UF functions to trie */ std::map< Node, TermArgTrie > d_func_map_trie; std::map< Node, TermArgTrie > d_func_map_eqc_trie; @@ -170,7 +172,9 @@ public: TNode evaluateTerm( TNode n ); /** is entailed (incomplete check) */ bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol ); - + /** has term */ + bool hasTermCurrent( Node n ); + //for model basis private: //map from types to model basis terms -- 2.30.2