From 199cf857baa106545196503cc4029e2b7771d1af Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 13 Apr 2016 15:02:31 -0500 Subject: [PATCH] Minor improvements for alpha equivalence and partial quantifier elimination in incremental mode. Change defaults to addInstantiation method. --- src/smt/smt_engine.cpp | 2 +- src/theory/quantifiers/alpha_equivalence.cpp | 15 ++-- src/theory/quantifiers/alpha_equivalence.h | 8 +-- src/theory/quantifiers/ambqi_builder.cpp | 2 +- .../quantifiers/ce_guided_instantiation.cpp | 2 +- src/theory/quantifiers/full_model_check.cpp | 4 +- src/theory/quantifiers/inst_match.cpp | 16 ++--- src/theory/quantifiers/inst_match.h | 32 ++++----- .../quantifiers/inst_match_generator.cpp | 12 ++-- src/theory/quantifiers/inst_strategy_cbqi.cpp | 4 +- .../quantifiers/inst_strategy_e_matching.cpp | 14 +--- src/theory/quantifiers/model_builder.cpp | 4 +- src/theory/quantifiers/model_engine.cpp | 2 +- .../quantifiers/quant_conflict_find.cpp | 2 +- src/theory/quantifiers/rewrite_engine.cpp | 2 +- src/theory/quantifiers_engine.cpp | 72 +++++++++++-------- src/theory/quantifiers_engine.h | 11 +-- 17 files changed, 105 insertions(+), 99 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index bd67af466..771195a38 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -5152,7 +5152,7 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict) //ensure all instantiations were accounted for for( std::map< Node, std::vector< Node > >::iterator it = insts.begin(); it != insts.end(); ++it ){ - if( visited.find( it->first )==visited.end() ){ + if( !it->second.empty() && visited.find( it->first )==visited.end() ){ stringstream ss; ss << "While performing quantifier elimination, processed a quantified formula : " << it->first; ss << " that was not related to the query. Try option --simplification=none."; diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp index 8abc3f65a..80066d690 100644 --- a/src/theory/quantifiers/alpha_equivalence.cpp +++ b/src/theory/quantifiers/alpha_equivalence.cpp @@ -29,7 +29,7 @@ struct sortTypeOrder { } }; -bool AlphaEquivalenceNode::registerNode( AlphaEquivalenceNode* aen, QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index ) { +Node AlphaEquivalenceNode::registerNode( AlphaEquivalenceNode* aen, QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index ) { while( !tt.empty() ){ if( tt.size()==arg_index.size()+1 ){ Node t = tt.back(); @@ -49,26 +49,25 @@ bool AlphaEquivalenceNode::registerNode( AlphaEquivalenceNode* aen, QuantifiersE } } } + Node lem; Trace("aeq-debug") << std::endl; if( aen->d_quant.isNull() ){ aen->d_quant = q; - return true; }else{ if( q.getNumChildren()==2 ){ //lemma ( q <=> d_quant ) Trace("quant-ae") << "Alpha equivalent : " << std::endl; Trace("quant-ae") << " " << q << std::endl; Trace("quant-ae") << " " << aen->d_quant << std::endl; - qe->getOutputChannel().lemma( q.iffNode( aen->d_quant ) ); - return false; + lem = q.iffNode( aen->d_quant ); }else{ //do not reduce annotated quantified formulas based on alpha equivalence - return true; } } + return lem; } -bool AlphaEquivalenceTypeNode::registerNode( AlphaEquivalenceTypeNode* aetn, +Node AlphaEquivalenceTypeNode::registerNode( AlphaEquivalenceTypeNode* aetn, QuantifiersEngine* qe, Node q, Node t, std::vector< TypeNode >& typs, std::map< TypeNode, int >& typ_count, int index ){ while( index<(int)typs.size() ){ TypeNode curr = typs[index]; @@ -84,7 +83,7 @@ bool AlphaEquivalenceTypeNode::registerNode( AlphaEquivalenceTypeNode* aetn, return AlphaEquivalenceNode::registerNode( &(aetn->d_data), qe, q, tt, arg_index ); } -bool AlphaEquivalence::reduceQuantifier( Node q ) { +Node AlphaEquivalence::reduceQuantifier( Node q ) { Assert( q.getKind()==FORALL ); Trace("aeq") << "Alpha equivalence : register " << q << std::endl; //construct canonical quantified formula @@ -104,7 +103,7 @@ bool AlphaEquivalence::reduceQuantifier( Node q ) { sto.d_tdb = d_qe->getTermDatabase(); std::sort( typs.begin(), typs.end(), sto ); Trace("aeq-debug") << " "; - bool ret = !AlphaEquivalenceTypeNode::registerNode( &d_ae_typ_trie, d_qe, q, t, typs, typ_count ); + Node ret = AlphaEquivalenceTypeNode::registerNode( &d_ae_typ_trie, d_qe, q, t, typs, typ_count ); Trace("aeq") << " ...result : " << ret << std::endl; return ret; } diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h index 40f533da7..8e7556eb6 100644 --- a/src/theory/quantifiers/alpha_equivalence.h +++ b/src/theory/quantifiers/alpha_equivalence.h @@ -28,14 +28,14 @@ class AlphaEquivalenceNode { public: std::map< Node, std::map< int, AlphaEquivalenceNode > > d_children; Node d_quant; - static bool registerNode( AlphaEquivalenceNode* aen, QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index ); + static Node registerNode( AlphaEquivalenceNode* aen, QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index ); }; class AlphaEquivalenceTypeNode { public: std::map< TypeNode, std::map< int, AlphaEquivalenceTypeNode > > d_children; AlphaEquivalenceNode d_data; - static bool registerNode( AlphaEquivalenceTypeNode* aetn, + static Node registerNode( AlphaEquivalenceTypeNode* aetn, QuantifiersEngine* qe, Node q, Node t, std::vector< TypeNode >& typs, std::map< TypeNode, int >& typ_count, int index = 0 ); }; @@ -47,8 +47,8 @@ private: public: AlphaEquivalence( QuantifiersEngine* qe ) : d_qe( qe ){} ~AlphaEquivalence(){} - - bool reduceQuantifier( Node q ); + /** reduce quantifier, return value (if non-null) is lemma justifying why q ia reducible. */ + Node reduceQuantifier( Node q ); }; } diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp index dd6db951d..5192da7de 100644 --- a/src/theory/quantifiers/ambqi_builder.cpp +++ b/src/theory/quantifiers/ambqi_builder.cpp @@ -159,7 +159,7 @@ bool AbsDef::addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, return true; }else{ if( depth==q[0].getNumChildren() ){ - if( qe->addInstantiation( q, terms ) ){ + if( qe->addInstantiation( q, terms, true ) ){ Trace("ambqi-inst-debug") << "-> Added instantiation." << std::endl; inst++; return true; diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index b00ddf036..d9059a3e6 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -432,7 +432,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { Assert( aq==q ); std::vector< Node > model_terms; if( getModelValues( conj, conj->d_candidates, model_terms ) ){ - d_quantEngine->addInstantiation( q, model_terms, false ); + d_quantEngine->addInstantiation( q, model_terms ); } } }else{ diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 6b06b9e5c..33c853328 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -682,7 +682,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, }else{ //just add the instance d_triedLemmas++; - if( d_qe->addInstantiation( f, inst ) ){ + if( d_qe->addInstantiation( f, inst, true ) ){ Trace("fmc-debug-inst") << "** Added instantiation." << std::endl; d_addedLemmas++; if( d_qe->inConflict() || options::fmfOneInstPerRound() ){ @@ -810,7 +810,7 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No if (ev!=d_true) { Trace("fmc-exh-debug") << ", add!"; //add as instantiation - if( d_qe->addInstantiation( f, inst ) ){ + if( d_qe->addInstantiation( f, inst, true ) ){ Trace("fmc-exh-debug") << " ...success."; addedLemmas++; if( d_qe->inConflict() || options::fmfOneInstPerRound() ){ diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 55a4e8f8c..8818175db 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -142,7 +142,7 @@ bool InstMatch::set( QuantifiersEngine* qe, int i, TNode n ) { } bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq, - bool modInst, ImtIndexOrder* imtio, bool onlyExist, int index ) { + ImtIndexOrder* imtio, bool onlyExist, int index ) { if( index==(int)f[0].getNumChildren() || ( imtio && index==(int)imtio->d_order.size() ) ){ return false; }else{ @@ -150,7 +150,7 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< No Node n = m[i_index]; std::map< Node, InstMatchTrie >::iterator it = d_data.find( n ); if( it!=d_data.end() ){ - bool ret = it->second.addInstMatch( qe, f, m, modEq, modInst, imtio, onlyExist, index+1 ); + bool ret = it->second.addInstMatch( qe, f, m, modEq, imtio, onlyExist, index+1 ); if( !onlyExist || !ret ){ return ret; } @@ -165,7 +165,7 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< No if( en!=n ){ std::map< Node, InstMatchTrie >::iterator itc = d_data.find( en ); if( itc!=d_data.end() ){ - if( itc->second.addInstMatch( qe, f, m, modEq, modInst, imtio, true, index+1 ) ){ + if( itc->second.addInstMatch( qe, f, m, modEq, imtio, true, index+1 ) ){ return false; } } @@ -175,7 +175,7 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< No } } if( !onlyExist ){ - d_data[n].addInstMatch( qe, f, m, modEq, modInst, imtio, false, index+1 ); + d_data[n].addInstMatch( qe, f, m, modEq, imtio, false, index+1 ); } return true; } @@ -240,7 +240,7 @@ CDInstMatchTrie::~CDInstMatchTrie() { bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, - context::Context* c, bool modEq, bool modInst, int index, bool onlyExist ){ + context::Context* c, bool modEq, int index, bool onlyExist ){ bool reset = false; if( !d_valid.get() ){ if( onlyExist ){ @@ -256,7 +256,7 @@ bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node n = m[ index ]; std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n ); if( it!=d_data.end() ){ - bool ret = it->second->addInstMatch( qe, f, m, c, modEq, modInst, index+1, onlyExist ); + bool ret = it->second->addInstMatch( qe, f, m, c, modEq, index+1, onlyExist ); if( !onlyExist || !ret ){ return reset || ret; } @@ -271,7 +271,7 @@ bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< if( en!=n ){ std::map< Node, CDInstMatchTrie* >::iterator itc = d_data.find( en ); if( itc!=d_data.end() ){ - if( itc->second->addInstMatch( qe, f, m, c, modEq, modInst, index+1, true ) ){ + if( itc->second->addInstMatch( qe, f, m, c, modEq, index+1, true ) ){ return false; } } @@ -286,7 +286,7 @@ bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< CDInstMatchTrie* imt = new CDInstMatchTrie( c ); Assert(d_data.find(n) == d_data.end()); d_data[n] = imt; - imt->addInstMatch( qe, f, m, c, modEq, modInst, index+1, false ); + imt->addInstMatch( qe, f, m, c, modEq, index+1, false ); } return true; } diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index a87d2704e..ad287c1a3 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -111,23 +111,23 @@ public: modInst is if we return true if m is an instance of a match that exists */ bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, - bool modInst = false, ImtIndexOrder* imtio = NULL, int index = 0 ) { - return !addInstMatch( qe, f, m, modEq, modInst, imtio, true, index ); + ImtIndexOrder* imtio = NULL, int index = 0 ) { + return !addInstMatch( qe, f, m, modEq, imtio, true, index ); } bool existsInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false, - bool modInst = false, ImtIndexOrder* imtio = NULL, int index = 0 ) { - return !addInstMatch( qe, f, m, modEq, modInst, imtio, true, index ); + ImtIndexOrder* imtio = NULL, int index = 0 ) { + return !addInstMatch( qe, f, m, modEq, imtio, true, index ); } /** add match m for quantifier f, take into account equalities if modEq = true, if imtio is non-null, this is the order to add to trie return true if successful */ bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, - bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 ){ - return addInstMatch( qe, f, m.d_vals, modEq, modInst, imtio, onlyExist, index ); + ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 ){ + return addInstMatch( qe, f, m.d_vals, modEq, imtio, onlyExist, index ); } bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false, - bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 ); + ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 ); bool removeInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, ImtIndexOrder* imtio = NULL, int index = 0 ); void print( std::ostream& out, Node q ) const{ std::vector< TNode > terms; @@ -159,23 +159,23 @@ public: modInst is if we return true if m is an instance of a match that exists */ bool existsInstMatch( QuantifiersEngine* qe, Node q, InstMatch& m, context::Context* c, bool modEq = false, - bool modInst = false, int index = 0 ) { - return !addInstMatch( qe, q, m, c, modEq, modInst, index, true ); + int index = 0 ) { + return !addInstMatch( qe, q, m, c, modEq, index, true ); } bool existsInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, context::Context* c, bool modEq = false, - bool modInst = false, int index = 0 ) { - return !addInstMatch( qe, q, m, c, modEq, modInst, index, true ); + int index = 0 ) { + return !addInstMatch( qe, q, m, c, modEq, index, true ); } /** add match m for quantifier f, take into account equalities if modEq = true, if imtio is non-null, this is the order to add to trie return true if successful */ bool addInstMatch( QuantifiersEngine* qe, Node q, InstMatch& m, context::Context* c, bool modEq = false, - bool modInst = false, int index = 0, bool onlyExist = false ) { - return addInstMatch( qe, q, m.d_vals, c, modEq, modInst, index, onlyExist ); + int index = 0, bool onlyExist = false ) { + return addInstMatch( qe, q, m.d_vals, c, modEq, index, onlyExist ); } bool addInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, context::Context* c, bool modEq = false, - bool modInst = false, int index = 0, bool onlyExist = false ); + int index = 0, bool onlyExist = false ); bool removeInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, int index = 0 ); void print( std::ostream& out, Node q ) const{ std::vector< TNode > terms; @@ -202,10 +202,10 @@ public: public: /** add match m, return true if successful */ bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){ - return d_imt.addInstMatch( qe, f, m, modEq, modInst, d_imtio ); + return d_imt.addInstMatch( qe, f, m, modEq, d_imtio ); } bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){ - return d_imt.existsInstMatch( qe, f, m, modEq, modInst, d_imtio ); + return d_imt.existsInstMatch( qe, f, m, modEq, d_imtio ); } };/* class InstMatchTrieOrdered */ diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index 791e36ce4..bf05de3bb 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -270,7 +270,7 @@ bool InstMatchGenerator::continueNextMatch( Node f, InstMatch& m, QuantifiersEng return d_next->getNextMatch( f, m, qe ); }else{ if( d_active_add ){ - return qe->addInstantiation( f, m, false ); + return qe->addInstantiation( f, m ); }else{ return true; } @@ -343,7 +343,7 @@ int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, Quantif while( getNextMatch( f, m, qe ) ){ if( !d_active_add ){ m.add( baseMatch ); - if( qe->addInstantiation( f, m, false ) ){ + if( qe->addInstantiation( f, m ) ){ addedLemmas++; if( qe->inConflict() ){ break; @@ -366,7 +366,7 @@ int InstMatchGenerator::addTerm( Node f, Node t, QuantifiersEngine* qe ){ if( !d_match_pattern.isNull() ){ InstMatch m( f ); if( getMatch( f, t, m, qe ) ){ - if( qe->addInstantiation( f, m, false ) ){ + if( qe->addInstantiation( f, m ) ){ return 1; } } @@ -674,7 +674,7 @@ void InstMatchGeneratorMulti::processNewInstantiations2( QuantifiersEngine* qe, } }else{ //m is an instantiation - if( qe->addInstantiation( d_f, m, false ) ){ + if( qe->addInstantiation( d_f, m ) ){ addedLemmas++; Debug("smart-multi-trigger") << "-> Produced instantiation " << m << std::endl; } @@ -770,7 +770,7 @@ void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngin Debug("simple-trigger") << "...set " << it->second << " " << t[it->first] << std::endl; m.setValue( it->second, t[it->first] ); } - if( qe->addInstantiation( d_f, m, false ) ){ + if( qe->addInstantiation( d_f, m ) ){ addedLemmas++; Debug("simple-trigger") << "-> Produced instantiation " << m << std::endl; } @@ -815,7 +815,7 @@ int InstMatchGeneratorSimple::addTerm( Node q, Node t, QuantifiersEngine* qe ){ return 0; } } - return qe->addInstantiation( q, m, false ) ? 1 : 0; + return qe->addInstantiation( q, m ) ? 1 : 0; } }/* CVC4::theory::inst namespace */ diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index fe4867b4e..149330c61 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -648,12 +648,12 @@ bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) { if( d_quantEngine->getTermDatabase()->isQAttrQuantElimPartial( d_curr_quant ) ){ d_cbqi_set_quant_inactive = true; d_incomplete_check = true; - d_quantEngine->recordInstantiationInternal( d_curr_quant, subs, false, false, true ); + d_quantEngine->recordInstantiationInternal( d_curr_quant, subs, false, false ); return true; }else{ //check if we need virtual term substitution (if used delta or infinity) bool used_vts = d_quantEngine->getTermDatabase()->containsVtsTerm( subs, false ); - if( d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, false, used_vts ) ){ + if( d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, used_vts ) ){ //d_added_inst.insert( d_curr_quant ); return true; }else{ diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 8c67eb95e..630880690 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -599,18 +599,6 @@ bool FullSaturation::process( Node f, bool fullEffort ){ unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1; unsigned rend = fullEffort ? 1 : rstart; for( unsigned r=rstart; r<=rend; r++ ){ - /* - //complete guess - if( d_guessed.find( f )==d_guessed.end() ){ - Trace("inst-alg") << "-> Guess instantiate " << f << "..." << std::endl; - d_guessed[f] = true; - InstMatch m( f ); - if( d_quantEngine->addInstantiation( f, m ) ){ - ++(d_quantEngine->d_statistics.d_instantiations_guess); - return true; - } - } - */ if( rd || r>0 ){ if( r==0 ){ Trace("inst-alg") << "-> Relevant domain instantiate " << f << "..." << std::endl; @@ -700,7 +688,7 @@ bool FullSaturation::process( Node f, bool fullEffort ){ Trace("inst-alg-rd") << " " << d_quantEngine->getTermDatabase()->getTypeGroundTerm( ftypes[i], childIndex[i] ) << std::endl; } } - if( d_quantEngine->addInstantiation( f, terms, false ) ){ + if( d_quantEngine->addInstantiation( f, terms ) ){ Trace("inst-alg-rd") << "Success!" << std::endl; ++(d_quantEngine->d_statistics.d_instantiations_guess); return true; diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index b0ca43cfe..3ae36b1d4 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -280,7 +280,7 @@ int QModelBuilderIG::initializeQuantifier( Node f, Node fp ){ //try to add it Trace("inst-fmf-init") << "Init: try to add match " << d_quant_basis_match[f] << std::endl; //add model basis instantiation - if( d_qe->addInstantiation( fp, d_quant_basis_match[f], false ) ){ + if( d_qe->addInstantiation( fp, d_quant_basis_match[f] ) ){ d_quant_basis_match_added[f] = true; return 1; }else{ @@ -430,7 +430,7 @@ bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i } Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl; //add as instantiation - if( d_qe->addInstantiation( f, m ) ){ + if( d_qe->addInstantiation( f, m, true ) ){ d_addedLemmas++; if( d_qe->inConflict() ){ break; diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index f94e947e5..0bbca88eb 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -294,7 +294,7 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl; triedLemmas++; //add as instantiation - if( d_quantEngine->addInstantiation( f, m ) ){ + if( d_quantEngine->addInstantiation( f, m, true ) ){ addedLemmas++; if( d_quantEngine->inConflict() ){ break; diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index c796333b3..ca87a607d 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -2004,7 +2004,7 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { Assert( !getTermDatabase()->isEntailed( inst, true ) ); Assert( getTermDatabase()->isEntailed( inst, false ) || e>effort_conflict ); } - if( d_quantEngine->addInstantiation( q, terms, false ) ){ + 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"); diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index 07b1462c6..5365dbcfa 100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -154,7 +154,7 @@ int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) { if( inst.size()>f[0].getNumChildren() ){ inst.resize( f[0].getNumChildren() ); } - if( d_quantEngine->addInstantiation( f, inst, false ) ){ + if( d_quantEngine->addInstantiation( f, inst ) ){ addedLemmas++; tempAddedLemmas++; /* diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 1008d7d49..6d3b17254 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -58,7 +58,7 @@ using namespace CVC4::theory::inst; QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te): d_te( te ), //d_quants(u), - //d_quants_red(u), + d_quants_red(u), d_lemmas_produced_c(u), d_skolemized(u), d_ierCounter_c(c), @@ -385,6 +385,14 @@ void QuantifiersEngine::check( Theory::Effort e ){ if( d_hasAddedLemma ){ return; } + if( !d_recorded_inst.empty() ){ + Trace("quant-engine-debug") << "Removing " << d_recorded_inst.size() << " instantiations..." << std::endl; + //remove explicitly recorded instantiations + for( unsigned i=0; ireduceQuantifier( q ) ){ - Trace("quant-engine-red") << "...alpha equivalence success." << std::endl; - ++(d_statistics.d_red_alpha_equiv); - d_quants_red[q] = true; - return true; + Node lem; + std::map< Node, Node >::iterator itr = d_quants_red_lem.find( q ); + if( itr==d_quants_red_lem.end() ){ + if( d_alpha_equiv ){ + Trace("quant-engine-red") << "Alpha equivalence " << q << "?" << std::endl; + //add equivalence with another quantified formula + lem = d_alpha_equiv->reduceQuantifier( q ); + if( !lem.isNull() ){ + Trace("quant-engine-red") << "...alpha equivalence success." << std::endl; + ++(d_statistics.d_red_alpha_equiv); + } } + d_quants_red_lem[q] = lem; + }else{ + lem = itr->second; } - d_quants_red[q] = false; - return false; + if( !lem.isNull() ){ + getOutputChannel().lemma( lem ); + } + d_quants_red[q] = !lem.isNull(); + return !lem.isNull(); }else{ return (*it).second; } @@ -759,13 +779,13 @@ void QuantifiersEngine::computeTermVector( Node f, InstMatch& m, std::vector< No } -bool QuantifiersEngine::recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq, bool modInst, bool addedLem ) { +bool QuantifiersEngine::recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq, bool addedLem ) { if( !addedLem ){ //record the instantiation for deletion later - //TODO + d_recorded_inst.push_back( std::pair< Node, std::vector< Node > >( q, terms ) ); } if( options::incrementalSolving() ){ - Trace("inst-add-debug") << "Adding into context-dependent inst trie, modEq = " << modEq << ", modInst = " << modInst << std::endl; + Trace("inst-add-debug") << "Adding into context-dependent inst trie, modEq = " << modEq << std::endl; inst::CDInstMatchTrie* imt; std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( q ); if( it!=d_c_inst_match_trie.end() ){ @@ -774,10 +794,10 @@ bool QuantifiersEngine::recordInstantiationInternal( Node q, std::vector< Node > imt = new CDInstMatchTrie( getUserContext() ); d_c_inst_match_trie[q] = imt; } - return imt->addInstMatch( this, q, terms, getUserContext(), modEq, modInst ); + return imt->addInstMatch( this, q, terms, getUserContext(), modEq ); }else{ Trace("inst-add-debug") << "Adding into inst trie" << std::endl; - return d_inst_match_trie[q].addInstMatch( this, q, terms, modEq, modInst ); + return d_inst_match_trie[q].addInstMatch( this, q, terms, modEq ); } } @@ -906,24 +926,20 @@ Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& terms, bo } /* -bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){ +bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq ){ if( options::incrementalSolving() ){ if( d_c_inst_match_trie.find( f )!=d_c_inst_match_trie.end() ){ - if( d_c_inst_match_trie[f]->existsInstMatch( this, f, m, getUserContext(), modEq, modInst ) ){ + if( d_c_inst_match_trie[f]->existsInstMatch( this, f, m, getUserContext(), modEq ) ){ return true; } } }else{ if( d_inst_match_trie.find( f )!=d_inst_match_trie.end() ){ - if( d_inst_match_trie[f].existsInstMatch( this, f, m, modEq, modInst ) ){ + if( d_inst_match_trie[f].existsInstMatch( this, f, m, modEq ) ){ return true; } } } - //also check model builder (it may contain instantiations internally) - if( d_builder && d_builder->existsInstantiation( f, m, modEq, modInst ) ){ - return true; - } return false; } */ @@ -969,13 +985,13 @@ void QuantifiersEngine::addRequirePhase( Node lit, bool req ){ d_phase_req_waiting[lit] = req; } -bool QuantifiersEngine::addInstantiation( Node q, InstMatch& m, bool mkRep, bool modEq, bool modInst, bool doVts ){ +bool QuantifiersEngine::addInstantiation( Node q, InstMatch& m, bool mkRep, bool modEq, bool doVts ){ std::vector< Node > terms; m.getTerms( q, terms ); - return addInstantiation( q, terms, mkRep, modEq, modInst, doVts ); + return addInstantiation( q, terms, mkRep, modEq, doVts ); } -bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bool mkRep, bool modEq, bool modInst, bool doVts ) { +bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bool mkRep, bool modEq, bool doVts ) { // For resource-limiting (also does a time check). getOutputChannel().safePoint(options::quantifierStep()); Assert( !d_conflict ); @@ -1052,7 +1068,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo } //check for term vector duplication - bool alreadyExists = !recordInstantiationInternal( q, terms, modEq, modInst ); + bool alreadyExists = !recordInstantiationInternal( q, terms, modEq ); if( alreadyExists ){ Trace("inst-add-debug") << " --> Already exists." << std::endl; ++(d_statistics.d_inst_duplicate_eq); diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index a088dfec6..4ee66f9e7 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -164,7 +164,8 @@ private: /** list of all quantifiers seen */ std::map< Node, bool > d_quants; /** quantifiers reduced */ - std::map< Node, bool > d_quants_red; + BoolMap d_quants_red; + std::map< Node, Node > d_quants_red_lem; /** list of all lemmas produced */ //std::map< Node, bool > d_lemmas_produced; BoolMap d_lemmas_produced_c; @@ -175,6 +176,8 @@ private: /** list of all instantiations produced for each quantifier */ std::map< Node, inst::InstMatchTrie > d_inst_match_trie; std::map< Node, inst::CDInstMatchTrie* > d_c_inst_match_trie; + /** recorded instantiations */ + std::vector< std::pair< Node, std::vector< Node > > > d_recorded_inst; /** quantifiers that have been skolemized */ BoolMap d_skolemized; /** term database */ @@ -287,7 +290,7 @@ private: /** compute term vector */ void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms ); /** record instantiation, return true if it was non-duplicate */ - bool recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq = false, bool modInst = false, bool addedLem = true ); + bool recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq = false, bool addedLem = true ); /** remove instantiation */ bool removeInstantiationInternal( Node q, std::vector< Node >& terms ); /** set instantiation level attr */ @@ -310,9 +313,9 @@ public: /** add require phase */ void addRequirePhase( Node lit, bool req ); /** do instantiation specified by m */ - bool addInstantiation( Node q, InstMatch& m, bool mkRep = true, bool modEq = false, bool modInst = false, bool doVts = false ); + bool addInstantiation( Node q, InstMatch& m, bool mkRep = false, bool modEq = false, bool doVts = false ); /** add instantiation */ - bool addInstantiation( Node q, std::vector< Node >& terms, bool mkRep = true, bool modEq = false, bool modInst = false, bool doVts = false ); + bool addInstantiation( Node q, std::vector< Node >& terms, bool mkRep = false, bool modEq = false, bool doVts = false ); /** remove pending instantiation */ bool removeInstantiation( Node q, Node lem, std::vector< Node >& terms ); /** split on node n */ -- 2.30.2