From: ajreynol Date: Mon, 15 May 2017 14:07:21 +0000 (-0500) Subject: Make conflict-based instantiation abort if a ground conflict is found in the master... X-Git-Tag: cvc5-1.0.0~5804 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0369b8325e9f631c77d479e5e9103cdb450bf650;p=cvc5.git Make conflict-based instantiation abort if a ground conflict is found in the master equality engine during term indexing, fixes bug 801. --- diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 420a3d2f7..008514dcc 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -2079,70 +2079,76 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { //try to make a matches making the body false Trace("qcf-check-debug") << "Get next match..." << std::endl; while( qi->getNextMatch( this ) ){ - Trace("qcf-inst") << "*** Produced match at effort " << e << " : " << std::endl; - qi->debugPrintMatch("qcf-inst"); - Trace("qcf-inst") << std::endl; - if( !qi->isMatchSpurious( this ) ){ - std::vector< int > assigned; - if( qi->completeMatch( this, assigned ) ){ - std::vector< Node > terms; - qi->getMatch( terms ); - bool tcs = qi->isTConstraintSpurious( this, terms ); - if( !tcs ){ - //for debugging - if( Debug.isOn("qcf-check-inst") ){ - Node inst = d_quantEngine->getInstantiation( q, terms ); - Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl; - Assert( !getTermDatabase()->isEntailed( inst, true ) ); - Assert( getTermDatabase()->isEntailed( inst, false ) || e>effort_conflict ); - } - if( d_quantEngine->addInstantiation( q, terms ) ){ - Trace("qcf-check") << " ... Added instantiation" << std::endl; - Trace("qcf-inst") << "*** Was from effort " << e << " : " << std::endl; - qi->debugPrintMatch("qcf-inst"); - Trace("qcf-inst") << std::endl; - ++addedLemmas; - if( e==effort_conflict ){ - d_quantEngine->markRelevant( q ); - ++(d_quantEngine->d_statistics.d_instantiations_qcf); - if( options::qcfAllConflict() ){ - isConflict = true; - }else{ - d_conflict.set( true ); + if( d_quantEngine->inConflict() ){ + Trace("qcf-check") << " ... Quantifiers engine discovered conflict, "; + Trace("qcf-check") << "probably related to disequal congruent terms in master equality engine" << std::endl; + break; + }else{ + Trace("qcf-inst") << "*** Produced match at effort " << e << " : " << std::endl; + qi->debugPrintMatch("qcf-inst"); + Trace("qcf-inst") << std::endl; + if( !qi->isMatchSpurious( this ) ){ + std::vector< int > assigned; + if( qi->completeMatch( this, assigned ) ){ + std::vector< Node > terms; + qi->getMatch( terms ); + bool tcs = qi->isTConstraintSpurious( this, terms ); + if( !tcs ){ + //for debugging + if( Debug.isOn("qcf-check-inst") ){ + Node inst = d_quantEngine->getInstantiation( q, terms ); + Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl; + Assert( !getTermDatabase()->isEntailed( inst, true ) ); + Assert( getTermDatabase()->isEntailed( inst, false ) || e>effort_conflict ); + } + if( d_quantEngine->addInstantiation( q, terms ) ){ + Trace("qcf-check") << " ... Added instantiation" << std::endl; + Trace("qcf-inst") << "*** Was from effort " << e << " : " << std::endl; + qi->debugPrintMatch("qcf-inst"); + Trace("qcf-inst") << std::endl; + ++addedLemmas; + if( e==effort_conflict ){ + d_quantEngine->markRelevant( q ); + ++(d_quantEngine->d_statistics.d_instantiations_qcf); + if( options::qcfAllConflict() ){ + isConflict = true; + }else{ + d_conflict.set( true ); + } + break; + }else if( e==effort_prop_eq ){ + d_quantEngine->markRelevant( q ); + ++(d_quantEngine->d_statistics.d_instantiations_qcf); } + }else{ + Trace("qcf-inst") << " ... Failed to add instantiation" << std::endl; + //this should only happen if the algorithm generates the same propagating instance twice this round + //in this case, break to avoid exponential behavior break; - }else if( e==effort_prop_eq ){ - d_quantEngine->markRelevant( q ); - ++(d_quantEngine->d_statistics.d_instantiations_qcf); } }else{ - Trace("qcf-inst") << " ... Failed to add instantiation" << std::endl; - //this should only happen if the algorithm generates the same propagating instance twice this round - //in this case, break to avoid exponential behavior - break; + Trace("qcf-inst") << " ... Spurious instantiation (match is T-inconsistent)" << std::endl; } + //clean up assigned + qi->revertMatch( this, assigned ); + d_tempCache.clear(); }else{ - Trace("qcf-inst") << " ... Spurious instantiation (match is T-inconsistent)" << std::endl; + Trace("qcf-inst") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl; } - //clean up assigned - qi->revertMatch( this, assigned ); - d_tempCache.clear(); }else{ - Trace("qcf-inst") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl; + Trace("qcf-inst") << " ... Spurious instantiation (match is inconsistent)" << std::endl; } - }else{ - Trace("qcf-inst") << " ... Spurious instantiation (match is inconsistent)" << std::endl; } } Trace("qcf-check") << "Done, conflict = " << d_conflict << std::endl; - if( d_conflict ){ + if( d_conflict || d_quantEngine->inConflict() ){ break; } } } } } - if( addedLemmas>0 ){ + if( addedLemmas>0 || d_quantEngine->inConflict() ){ break; } } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 5ac5ae0cc..30b17d42c 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -278,10 +278,12 @@ void TermDb::computeUfTerms( TNode f ) { Trace("term-db-lemma") << "Disequal congruent terms : " << at << " " << n << "!!!!" << std::endl; if( !d_quantEngine->getTheoryEngine()->needCheck() ){ Trace("term-db-lemma") << " all theories passed with no lemmas." << std::endl; + // we should be a full effort check, prior to theory combination } Trace("term-db-lemma") << " add lemma : " << lem << std::endl; } d_quantEngine->addLemma( lem ); + d_quantEngine->setConflict(); d_consistent_ee = false; return; } diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index db0efd988..55b1af83c 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -80,6 +80,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* d_util.push_back( d_term_db ); if( options::instPropagate() ){ + // notice that this option is incompatible with options::qcfAllConflict() d_inst_prop = new quantifiers::InstPropagator( this ); d_util.push_back( d_inst_prop ); d_inst_notify.push_back( d_inst_prop->getInstantiationNotify() ); @@ -1250,8 +1251,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo for( unsigned j=0; jnotifyInstantiation( d_curr_effort_level, q, lem, terms, body ) ){ Trace("inst-add-debug") << "...we are in conflict." << std::endl; - d_conflict = true; - d_conflict_c = true; + setConflict(); Assert( !d_lemmas_waiting.empty() ); break; } @@ -1319,6 +1319,11 @@ void QuantifiersEngine::markRelevant( Node q ) { d_model->markRelevant( q ); } +void QuantifiersEngine::setConflict() { + d_conflict = true; + d_conflict_c = true; +} + bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) { Trace("quant-engine-debug2") << "Get inst when needs check, counts=" << d_ierCounter << ", " << d_ierCounter_lc << std::endl; //determine if we should perform check, based on instWhenMode diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index bb38e5e4a..7405241b7 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -39,11 +39,6 @@ namespace theory { class QuantifiersEngine; -namespace quantifiers { - class TermDb; - class TermDbSygus; -} - class InstantiationNotify { public: InstantiationNotify(){} @@ -53,6 +48,8 @@ public: }; namespace quantifiers { + class TermDb; + class TermDbSygus; class FirstOrderModel; //modules class InstantiationEngine; @@ -343,6 +340,8 @@ public: bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; } /** is in conflict */ bool inConflict() { return d_conflict; } + /** set conflict */ + void setConflict(); /** get number of waiting lemmas */ unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); } /** get needs check */