diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/ematching/inst_match_generator.cpp | 13 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_conflict_find.cpp | 45 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_conflict_find.h | 8 |
3 files changed, 48 insertions, 18 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 ); } diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 02c9aedf5..92a355348 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -268,7 +268,10 @@ bool QuantInfo::reset_round( QuantConflictFind * p ) { d_mg->reset_round( p ); for( std::map< int, MatchGen * >::iterator it = d_var_mg.begin(); it != d_var_mg.end(); ++it ){ - it->second->reset_round( p ); + if (!it->second->reset_round(p)) + { + return false; + } } //now, reset for matching d_mg->reset( p, false, this ); @@ -1178,11 +1181,14 @@ void MatchGen::determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars } } - -void MatchGen::reset_round( QuantConflictFind * p ) { +bool MatchGen::reset_round(QuantConflictFind* p) +{ d_wasSet = false; for( unsigned i=0; i<d_children.size(); i++ ){ - d_children[i].reset_round( p ); + if (!d_children[i].reset_round(p)) + { + return false; + } } for( std::map< int, TNode >::iterator it = d_qni_gterm.begin(); it != d_qni_gterm.end(); ++it ){ d_qni_gterm_rep[it->first] = p->getRepresentative( it->second ); @@ -1194,18 +1200,31 @@ void MatchGen::reset_round( QuantConflictFind * p ) { //}else if( e==-1 ){ // d_ground_eval[0] = p->d_false; //} - //modified - for( unsigned i=0; i<2; i++ ){ - if( p->getTermDatabase()->isEntailed( d_n, i==0 ) ){ + //modified + TermDb* tdb = p->getTermDatabase(); + QuantifiersEngine* qe = p->getQuantifiersEngine(); + for( unsigned i=0; i<2; i++ ){ + if (tdb->isEntailed(d_n, i == 0)) + { d_ground_eval[0] = i==0 ? p->d_true : p->d_false; } + if (qe->inConflict()) + { + return false; + } } }else if( d_type==typ_eq ){ - for (unsigned i = 0; i < d_n.getNumChildren(); i++) + TermDb* tdb = p->getTermDatabase(); + QuantifiersEngine* qe = p->getQuantifiersEngine(); + for (unsigned i = 0, size = d_n.getNumChildren(); i < size; i++) { if (!expr::hasBoundVar(d_n[i])) { - TNode t = p->getTermDatabase()->getEntailedTerm(d_n[i]); + TNode t = tdb->getEntailedTerm(d_n[i]); + if (qe->inConflict()) + { + return false; + } if (t.isNull()) { d_ground_eval[i] = d_n[i]; @@ -1220,6 +1239,7 @@ void MatchGen::reset_round( QuantConflictFind * p ) { d_qni_bound_cons.clear(); d_qni_bound_cons_var.clear(); d_qni_bound.clear(); + return true; } void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) { @@ -2038,9 +2058,10 @@ void QuantConflictFind::check(Theory::Effort level, QEffort quant_e) } } Trace("qcf-check") << "Done, conflict = " << d_conflict << std::endl; - if( d_conflict || d_quantEngine->inConflict() ){ - break; - } + } + if (d_conflict || d_quantEngine->inConflict()) + { + break; } } } diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index d76495b52..0469e958b 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -90,7 +90,13 @@ public: std::vector< MatchGen > d_children; short d_type; bool d_type_not; - void reset_round( QuantConflictFind * p ); + /** reset round + * + * Called once at the beginning of each full/last-call effort, prior to + * processing this match generator. This method returns false if the reset + * failed, e.g. if a conflict was encountered during term indexing. + */ + bool reset_round(QuantConflictFind* p); void reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ); bool getNextMatch( QuantConflictFind * p, QuantInfo * qi ); bool isValid() { return d_type!=typ_invalid; } |