diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-09-04 14:34:21 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-09-04 14:34:21 -0500 |
commit | d367c9f9b299a15fb970d62df04d3df22b7ca08d (patch) | |
tree | 6629e5c12cc8629398e81bcf15608f5493536b6b /src/theory/quantifiers/ematching | |
parent | 32530dad5747665df4086abd2c4fabff15bb7d12 (diff) |
Make quantifiers strategies exit immediately when in conflict (#2099)
Diffstat (limited to 'src/theory/quantifiers/ematching')
-rw-r--r-- | src/theory/quantifiers/ematching/inst_match_generator.cpp | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index eb3f6232d..78fb987f1 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -426,6 +426,7 @@ int InstMatchGenerator::getNextMatch(Node f, Node t = d_curr_first_candidate; do{ Trace("matching-debug2") << "Matching candidate : " << t << std::endl; + Assert(!qe->inConflict()); //if t not null, try to fit it into match m if( !t.isNull() ){ if( d_curr_exclude_match.find( t )==d_curr_exclude_match.end() ){ @@ -439,7 +440,7 @@ int InstMatchGenerator::getNextMatch(Node f, } //get the next candidate term t if( success<0 ){ - t = d_cg->getNextCandidate(); + t = qe->inConflict() ? Node::null() : d_cg->getNextCandidate(); }else{ d_curr_first_candidate = d_cg->getNextCandidate(); } @@ -1029,10 +1030,11 @@ int InstMatchGeneratorSimple::addInstantiations(Node q, if( d_pol ){ tat = qe->getTermDatabase()->getTermArgTrie( d_eqc, d_op ); }else{ - Node r = qe->getEqualityQuery()->getRepresentative( d_eqc ); //iterate over all classes except r tat = qe->getTermDatabase()->getTermArgTrie( Node::null(), d_op ); - if( tat ){ + 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 ){ InstMatch m( q ); @@ -1042,12 +1044,13 @@ int InstMatchGeneratorSimple::addInstantiations(Node q, } } } - tat = NULL; } + tat = nullptr; } } Debug("simple-trigger-debug") << "Adding instantiations based on " << tat << " from " << d_op << " " << d_eqc << std::endl; - if( tat ){ + if (tat && !qe->inConflict()) + { InstMatch m( q ); addInstantiations( m, qe, addedLemmas, 0, tat ); } |