From 1b2e6c81be2a8ab0656ff2ee3938ef4587e24e25 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 11 Apr 2016 09:17:06 -0500 Subject: [PATCH] Minor fixes for inst match generators. Updates to qip. --- .../quantifiers/inst_match_generator.cpp | 50 ++++++++++++------- src/theory/quantifiers/inst_propagator.cpp | 36 +++++++++++-- src/theory/quantifiers/inst_propagator.h | 2 +- src/theory/quantifiers_engine.cpp | 1 + test/regress/regress0/fmf/Makefile.am | 1 + 5 files changed, 69 insertions(+), 21 deletions(-) diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index 29754d3e6..791e36ce4 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -307,9 +307,6 @@ void InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){ } bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ){ - if( qe->inConflict() ){ - return false; - } if( d_needsReset ){ Trace("matching") << "Reset not done yet, must do the reset..." << std::endl; reset( d_eq_class, qe ); @@ -348,9 +345,15 @@ int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, Quantif m.add( baseMatch ); if( qe->addInstantiation( f, m, false ) ){ addedLemmas++; + if( qe->inConflict() ){ + break; + } } }else{ addedLemmas++; + if( qe->inConflict() ){ + break; + } } m.clear(); } @@ -368,7 +371,7 @@ int InstMatchGenerator::addTerm( Node f, Node t, QuantifiersEngine* qe ){ } } }else{ - for( int i=0; i<(int)d_children.size(); i++ ){ + for( unsigned i=0; iaddTerm( f, t, qe ); } } @@ -530,14 +533,14 @@ d_f( q ){ /** reset instantiation round (call this whenever equivalence classes have changed) */ void InstMatchGeneratorMulti::resetInstantiationRound( QuantifiersEngine* qe ){ - for( int i=0; i<(int)d_children.size(); i++ ){ + for( unsigned i=0; iresetInstantiationRound( qe ); } } /** reset, eqc is the equivalence class to search in (any if eqc=null) */ void InstMatchGeneratorMulti::reset( Node eqc, QuantifiersEngine* qe ){ - for( int i=0; i<(int)d_children.size(); i++ ){ + for( unsigned i=0; ireset( eqc, qe ); } } @@ -545,7 +548,7 @@ void InstMatchGeneratorMulti::reset( Node eqc, QuantifiersEngine* qe ){ int InstMatchGeneratorMulti::addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ){ int addedLemmas = 0; Debug("smart-multi-trigger") << "Process smart multi trigger" << std::endl; - for( int i=0; i<(int)d_children.size(); i++ ){ + for( unsigned i=0; i newMatches; InstMatch m( q ); @@ -555,8 +558,11 @@ int InstMatchGeneratorMulti::addInstantiations( Node q, InstMatch& baseMatch, Qu m.clear(); } Debug("smart-multi-trigger") << "Made " << newMatches.size() << " new matches for index " << i << std::endl; - for( int j=0; j<(int)newMatches.size(); j++ ){ + for( unsigned j=0; jinConflict() ){ + return addedLemmas; + } } } return addedLemmas; @@ -579,6 +585,7 @@ void InstMatchGeneratorMulti::processNewMatch( QuantifiersEngine* qe, InstMatch& void InstMatchGeneratorMulti::processNewInstantiations( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, InstMatchTrie* tr, std::vector< IndexedTrie >& unique_var_tries, int trieIndex, int childIndex, int endChildIndex, bool modEq ){ + Assert( !qe->inConflict() ); if( childIndex==endChildIndex ){ //now, process unique variables processNewInstantiations2( qe, m, addedLemmas, unique_var_tries, 0 ); @@ -600,6 +607,9 @@ void InstMatchGeneratorMulti::processNewInstantiations( QuantifiersEngine* qe, I mn.setValue( curr_index, it->first); processNewInstantiations( qe, mn, addedLemmas, &(it->second), unique_var_tries, trieIndex+1, childIndex, endChildIndex, modEq ); + if( qe->inConflict() ){ + break; + } } //} }else{ @@ -621,6 +631,9 @@ void InstMatchGeneratorMulti::processNewInstantiations( QuantifiersEngine* qe, I if( itc!=tr->d_data.end() ){ processNewInstantiations( qe, m, addedLemmas, &(itc->second), unique_var_tries, trieIndex+1, childIndex, endChildIndex, modEq ); + if( qe->inConflict() ){ + break; + } } } ++eqc; @@ -652,6 +665,9 @@ void InstMatchGeneratorMulti::processNewInstantiations2( QuantifiersEngine* qe, InstMatch mn( &m ); mn.setValue( curr_index, it->first); processNewInstantiations2( qe, mn, addedLemmas, unique_var_tries, uvtIndex, &(it->second), trieIndex+1 ); + if( qe->inConflict() ){ + break; + } } }else{ processNewInstantiations2( qe, m, addedLemmas, unique_var_tries, uvtIndex+1 ); @@ -727,6 +743,9 @@ int InstMatchGeneratorSimple::addInstantiations( Node q, InstMatch& baseMatch, Q InstMatch m( q ); m.add( baseMatch ); addInstantiations( m, qe, addedLemmas, 0, &(it->second) ); + if( qe->inConflict() ){ + break; + } } } tat = NULL; @@ -736,10 +755,8 @@ int InstMatchGeneratorSimple::addInstantiations( Node q, InstMatch& baseMatch, Q InstMatch m( q ); m.add( baseMatch ); addInstantiations( m, qe, addedLemmas, 0, tat ); - return addedLemmas; - }else{ - return 0; } + return addedLemmas; } void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat ){ @@ -777,13 +794,12 @@ void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngin } return; } + //inst constant from another quantified formula, treat as ground term TODO: remove this? } - if( !qe->inConflict() ){ - Node r = qe->getEqualityQuery()->getRepresentative( d_match_pattern[argIndex] ); - std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.find( r ); - if( it!=tat->d_data.end() ){ - addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) ); - } + Node r = qe->getEqualityQuery()->getRepresentative( d_match_pattern[argIndex] ); + std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.find( r ); + if( it!=tat->d_data.end() ){ + addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) ); } } } diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp index 863914567..c6f4affc5 100644 --- a/src/theory/quantifiers/inst_propagator.cpp +++ b/src/theory/quantifiers/inst_propagator.cpp @@ -156,8 +156,15 @@ bool EqualityQueryInstProp::areDisequalExp( Node a, Node b, std::vector< Node >& if( areDisequal( a, b ) ){ return true; }else{ - //TODO? - return false; + //Assert( getRepresentative( a )==a ); + //Assert( getRepresentative( b )==b ); + std::map< Node, std::vector< Node > >::iterator itd = d_diseq_list[a].find( b ); + if( itd!=d_diseq_list[a].end() ){ + exp.insert( exp.end(), itd->second.begin(), itd->second.end() ); + return true; + }else{ + return false; + } } } @@ -283,9 +290,27 @@ int EqualityQueryInstProp::setEqual( Node& a, Node& b, bool pol, std::vector< No Trace("qip-eq") << "EqualityQueryInstProp::setEqual : merge " << ar << " -> " << br << ", exp size = " << d_uf_exp[ar].size() << ", status = " << status << std::endl; a = ar; b = br; + + //carry disequality list + std::map< Node, std::map< Node, std::vector< Node > > >::iterator itd = d_diseq_list.find( ar ); + if( itd!=d_diseq_list.end() ){ + for( std::map< Node, std::vector< Node > >::iterator itdd = itd->second.begin(); itdd != itd->second.end(); ++itdd ){ + Node d = itdd->first; + if( d_diseq_list[br].find( d )==d_diseq_list[br].end() ){ + merge_exp( d_diseq_list[br][d], itdd->second ); + merge_exp( d_diseq_list[br][d], d_uf_exp[ar] ); + } + } + } + return status; }else{ - //TODO? + Trace("qip-eq") << "EqualityQueryInstProp::setEqual : disequal " << ar << " <> " << br << std::endl; + Assert( d_diseq_list[ar].find( br )==d_diseq_list[ar].end() ); + Assert( d_diseq_list[br].find( ar )==d_diseq_list[br].end() ); + + merge_exp( d_diseq_list[ar][br], reason ); + merge_exp( d_diseq_list[br][ar], reason ); return STATUS_NONE; } } @@ -556,6 +581,7 @@ bool InstPropagator::notifyInstantiation( unsigned quant_e, Node q, Node lem, st Trace("qip-prop") << "...finished notify instantiation." << std::endl; return !d_conflict; }else{ + Assert( false ); return true; } } @@ -688,14 +714,18 @@ void InstPropagator::conflict( std::vector< Node >& exp ) { addRelevantInstances( exp, "qip-propagate" ); //now, inform quantifiers engine which instances should be retracted + Trace("qip-prop-debug") << "...remove instantiation ids : "; for( std::map< unsigned, InstInfo >::iterator it = d_ii.begin(); it != d_ii.end(); ++it ){ if( d_relevant_inst.find( it->first )==d_relevant_inst.end() ){ if( !d_qe->removeInstantiation( it->second.d_q, it->second.d_lem, it->second.d_terms ) ){ Trace("qip-warn") << "WARNING : did not remove instantiation id " << it->first << std::endl; Assert( false ); + }else{ + Trace("qip-prop-debug") << it->first << " "; } } } + Trace("qip-prop-debug") << std::endl; //will interupt the quantifiers engine Trace("quant-engine-conflict") << "-----> InstPropagator::conflict with " << exp.size() << " instances." << std::endl; } diff --git a/src/theory/quantifiers/inst_propagator.h b/src/theory/quantifiers/inst_propagator.h index a6f76ef44..0c02c7f95 100644 --- a/src/theory/quantifiers/inst_propagator.h +++ b/src/theory/quantifiers/inst_propagator.h @@ -72,7 +72,7 @@ private: std::map< Node, std::vector< Node > > d_uf_exp; Node getUfRepresentative( Node a, std::vector< Node >& exp ); /** disequality list, stores explanations */ - std::map< Node, std::map< Node, Node > > d_diseq_list; + std::map< Node, std::map< Node, std::vector< Node > > > d_diseq_list; /** add arg */ void addArgument( std::vector< Node >& args, std::vector< Node >& props, Node n, bool is_prop, bool pol ); public: diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index f98a3fd75..4b95c75ed 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -1101,6 +1101,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo Trace("inst-add-debug") << "...we are in conflict." << std::endl; d_conflict = true; Assert( !d_lemmas_waiting.empty() ); + break; } } } diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index 91e0c37d4..575aa4159 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -38,6 +38,7 @@ TESTS = \ lst-no-self-rev-exp.smt2 \ fib-core.smt2 \ fore19-exp2-core.smt2 \ + with-ind-104-core.smt2 \ syn002-si-real-int.smt2 \ krs-sat.smt2 \ forall_unit_data2.smt2 \ -- 2.30.2