diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-18 11:27:45 -0600 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-18 11:27:58 -0600 |
commit | c6f7c7e36c7897e9c9e6fd556bcdddcb9574d881 (patch) | |
tree | d20273d6d0fc91e5a5986225956cf6b191cc2ac7 /src/theory/quantifiers/candidate_generator.cpp | |
parent | 302a83176187b666d781c3509ea8869981cf06a7 (diff) |
Performance optimization for E-matching, working on using QCF module for propagations.
Diffstat (limited to 'src/theory/quantifiers/candidate_generator.cpp')
-rw-r--r-- | src/theory/quantifiers/candidate_generator.cpp | 66 |
1 files changed, 44 insertions, 22 deletions
diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index 783f6284d..60fa672b3 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -68,35 +68,57 @@ void CandidateGeneratorQE::resetInstantiationRound(){ void CandidateGeneratorQE::reset( Node eqc ){ d_term_iter = 0; if( eqc.isNull() ){ - d_using_term_db = true; + d_mode = cand_term_db; }else{ //create an equivalence class iterator in eq class eqc - d_eqc.clear(); - d_qe->getEqualityQuery()->getEquivalenceClass( eqc, d_eqc ); - d_using_term_db = false; + //d_qe->getEqualityQuery()->getEquivalenceClass( eqc, d_eqc ); + + eq::EqualityEngine* ee = d_qe->getEqualityQuery()->getEngine(); + if( ee->hasTerm( eqc ) ){ + Node rep = ee->getRepresentative( eqc ); + d_eqc_iter = eq::EqClassIterator( rep, ee ); + d_mode = cand_term_eqc; + }else{ + d_n = eqc; + d_mode = cand_term_ident; + } + //a should be in its equivalence class + //Assert( std::find( eqc.begin(), eqc.end(), a )!=eqc.end() ); + } +} +bool CandidateGeneratorQE::isLegalOpCandidate( Node n ) { + if( n.hasOperator() && n.getOperator()==d_op ){ + if( isLegalCandidate( n ) ){ + return true; + } } + return false; } Node CandidateGeneratorQE::getNextCandidate(){ - if( d_term_iter>=0 ){ - if( d_using_term_db ){ - //get next candidate term in the uf term database - while( d_term_iter<d_term_iter_limit ){ - Node n = d_qe->getTermDatabase()->d_op_map[d_op][d_term_iter]; - d_term_iter++; - if( isLegalCandidate( n ) ){ - return n; - } + if( d_mode==cand_term_db ){ + //get next candidate term in the uf term database + while( d_term_iter<d_term_iter_limit ){ + Node n = d_qe->getTermDatabase()->d_op_map[d_op][d_term_iter]; + d_term_iter++; + if( isLegalCandidate( n ) ){ + return n; } - }else{ - while( d_term_iter<(int)d_eqc.size() ){ - Node n = d_eqc[d_term_iter]; - d_term_iter++; - if( n.hasOperator() && n.getOperator()==d_op ){ - if( isLegalCandidate( n ) ){ - return n; - } - } + } + }else if( d_mode==cand_term_eqc ){ + while( !d_eqc_iter.isFinished() ){ + Node n = *d_eqc_iter; + ++d_eqc_iter; + if( isLegalOpCandidate( n ) ){ + return n; + } + } + }else if( d_mode==cand_term_ident ){ + if( !d_n.isNull() ){ + Node n = d_n; + d_n = Node::null(); + if( isLegalOpCandidate( n ) ){ + return n; } } } |