From e54c0f73712b25f1d6d49a3817c923eea077da81 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 4 Feb 2013 00:08:32 -0600 Subject: [PATCH] Model no longer adds subterms of quantifiers to equality engine, this fixed bug 492 and resolves previous issue for bug 486.\n Multiple improvements for E-matching: do not choose multi-triggers if single triggers exist, only create multi-triggers that contain all variables, consider multiple terms per equivalence class but only add one instantiation per round per (trigger,term) pair.\nImprovements for strong solver: make use of sort inference information when choosing splits, check for cliques eagerly when disequalities are asserted. --- src/smt/smt_engine.cpp | 3 +- src/theory/model.cpp | 3 + .../quantifiers/inst_match_generator.cpp | 62 ++- src/theory/quantifiers/inst_match_generator.h | 17 +- .../quantifiers/inst_strategy_e_matching.cpp | 72 ++- .../quantifiers/inst_strategy_e_matching.h | 4 +- src/theory/quantifiers/options | 4 +- src/theory/quantifiers/term_database.cpp | 35 ++ src/theory/quantifiers/term_database.h | 2 + src/theory/quantifiers/trigger.cpp | 73 +-- src/theory/quantifiers/trigger.h | 4 +- src/theory/quantifiers_engine.cpp | 23 +- src/theory/quantifiers_engine.h | 4 + src/theory/theory_engine.h | 5 + src/theory/uf/options | 4 +- src/theory/uf/theory_uf_strong_solver.cpp | 420 ++++++++---------- src/theory/uf/theory_uf_strong_solver.h | 39 +- src/util/sort_inference.cpp | 26 +- src/util/sort_inference.h | 4 + test/regress/regress0/Makefile.am | 4 +- test/regress/regress0/quantifiers/Makefile.am | 6 +- 21 files changed, 430 insertions(+), 384 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 4104c0916..948e42857 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2641,8 +2641,7 @@ void SmtEnginePrivate::processAssertions() { if( options::sortInference() ){ //sort inference technique - SortInference si; - si.simplify( d_assertionsToPreprocess ); + d_smt.d_theoryEngine->getSortInference()->simplify( d_assertionsToPreprocess ); } dumpAssertions("pre-simplify", d_assertionsToPreprocess); diff --git a/src/theory/model.cpp b/src/theory/model.cpp index 713587be2..bbc51c9e0 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -395,6 +395,9 @@ bool TheoryEngineModelBuilder::isAssignable(TNode n) void TheoryEngineModelBuilder::checkTerms(TNode n, TheoryModel* tm, NodeSet& cache) { + if (n.getKind()==FORALL || n.getKind()==EXISTS) { + return; + } if (cache.find(n) != cache.end()) { return; } diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index 3b5e594fb..7dc0058cf 100755 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -41,6 +41,13 @@ InstMatchGenerator::InstMatchGenerator( std::vector< Node >& pats, QuantifiersEn } } +void InstMatchGenerator::setActiveAdd(){ + d_active_add = true; + if( !d_children.empty() ){ + d_children[d_children.size()-1]->setActiveAdd(); + } +} + void InstMatchGenerator::initializePatterns( std::vector< Node >& pats, QuantifiersEngine* qe ){ int childMatchPolicy = d_matchPolicy==MATCH_GEN_EFFICIENT_E_MATCH ? 0 : d_matchPolicy; for( int i=0; i<(int)pats.size(); i++ ){ @@ -52,6 +59,7 @@ void InstMatchGenerator::initializePatterns( std::vector< Node >& pats, Quantifi } void InstMatchGenerator::initializePattern( Node pat, QuantifiersEngine* qe ){ + d_active_add = false; Debug("inst-match-gen") << "Pattern term is " << pat << std::endl; Assert( pat.hasAttribute(InstConstantAttribute()) ); d_pattern = pat; @@ -136,9 +144,9 @@ void InstMatchGenerator::initializePattern( Node pat, QuantifiersEngine* qe ){ } /** get match (not modulo equality) */ -bool InstMatchGenerator::getMatch( Node t, InstMatch& m, QuantifiersEngine* qe ){ +bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngine* qe ){ Debug("matching") << "Matching " << t << " against pattern " << d_match_pattern << " (" - << m.size() << ")" << ", " << d_children.size() << std::endl; + << m << ")" << ", " << d_children.size() << std::endl; Assert( !d_match_pattern.isNull() ); if( qe->d_optMatchIgnoreModelBasis && t.getAttribute(ModelBasisAttribute()) ){ return true; @@ -191,7 +199,7 @@ bool InstMatchGenerator::getMatch( Node t, InstMatch& m, QuantifiersEngine* qe ) int index = 0; while( index>=0 && index<(int)d_children.size() ){ partial.push_back( InstMatch( &partial[index] ) ); - if( d_children[index]->getNextMatch2( partial[index+1], qe ) ){ + if( d_children[index]->getNextMatch2( f, partial[index+1], qe ) ){ index++; }else{ d_children[index]->d_cg->reset( reps[index] ); @@ -203,15 +211,22 @@ bool InstMatchGenerator::getMatch( Node t, InstMatch& m, QuantifiersEngine* qe ) } } if( index>=0 ){ - m = partial.back(); - return true; + if( d_children.empty() && d_active_add ){ + Trace("active-add") << "Active Adding instantiation " << partial.back() << std::endl; + bool succ = qe->addInstantiation( f, partial.back() ); + Trace("active-add") << "Success = " << succ << std::endl; + return succ; + }else{ + m = partial.back(); + return true; + } }else{ return false; } } } -bool InstMatchGenerator::getNextMatch2( InstMatch& m, QuantifiersEngine* qe, bool saveMatched ){ +bool InstMatchGenerator::getNextMatch2( Node f, InstMatch& m, QuantifiersEngine* qe, bool saveMatched ){ bool success = false; Node t; do{ @@ -219,7 +234,7 @@ bool InstMatchGenerator::getNextMatch2( InstMatch& m, QuantifiersEngine* qe, boo t = d_cg->getNextCandidate(); //if t not null, try to fit it into match m if( !t.isNull() && t.getType()==d_match_pattern.getType() ){ - success = getMatch( t, m, qe ); + success = getMatch( f, t, m, qe ); } }while( !success && !t.isNull() ); if (saveMatched) m.d_matched = t; @@ -315,7 +330,7 @@ void InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){ } } -bool InstMatchGenerator::getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ +bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ){ m.d_matched = Node::null(); if( d_match_pattern.isNull() ){ int index = (int)d_partial.size(); @@ -325,7 +340,7 @@ bool InstMatchGenerator::getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ }else{ d_partial.push_back( InstMatch() ); } - if( d_children[index]->getNextMatch( d_partial[index], qe ) ){ + if( d_children[index]->getNextMatch( f, d_partial[index], qe ) ){ index++; }else{ d_children[index]->reset( Node::null(), qe ); @@ -344,7 +359,7 @@ bool InstMatchGenerator::getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ return false; } }else{ - bool res = getNextMatch2( m, qe, true ); + bool res = getNextMatch2( f, m, qe, true ); Assert(!res || !m.d_matched.isNull()); return res; } @@ -356,16 +371,21 @@ int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, Quantif //now, try to add instantiation for each match produced int addedLemmas = 0; InstMatch m; - while( getNextMatch( m, qe ) ){ - //m.makeInternal( d_quantEngine->getEqualityQuery() ); - m.add( baseMatch ); - if( qe->addInstantiation( f, m ) ){ - addedLemmas++; - if( qe->d_optInstLimitActive && qe->d_optInstLimit<=0 ){ - return addedLemmas; + while( getNextMatch( f, m, qe ) ){ + //if( d_active_add ){ + // std::cout << "should not add at top level." << std::endl; + //} + if( !d_active_add ){ + //m.makeInternal( d_quantEngine->getEqualityQuery() ); + m.add( baseMatch ); + if( qe->addInstantiation( f, m ) ){ + addedLemmas++; + if( qe->d_optInstLimitActive && qe->d_optInstLimit<=0 ){ + return addedLemmas; + } } + m.clear(); } - m.clear(); } //return number of lemmas added return addedLemmas; @@ -375,7 +395,7 @@ int InstMatchGenerator::addTerm( Node f, Node t, QuantifiersEngine* qe ){ Assert( options::eagerInstQuant() ); if( !d_match_pattern.isNull() ){ InstMatch m; - if( getMatch( t, m, qe ) ){ + if( getMatch( f, t, m, qe ) ){ if( qe->addInstantiation( f, m ) ){ return 1; } @@ -473,7 +493,7 @@ int InstMatchGeneratorMulti::addInstantiations( Node f, InstMatch& baseMatch, Qu Debug("smart-multi-trigger") << "Calculate matches " << i << std::endl; std::vector< InstMatch > newMatches; InstMatch m; - while( d_children[i]->getNextMatch( m, qe ) ){ + while( d_children[i]->getNextMatch( f, m, qe ) ){ m.makeRepresentative( qe ); newMatches.push_back( InstMatch( &m ) ); m.clear(); @@ -595,7 +615,7 @@ int InstMatchGeneratorMulti::addTerm( Node f, Node t, QuantifiersEngine* qe ){ if( ((InstMatchGenerator*)d_children[i])->d_match_pattern.getOperator()==t.getOperator() ){ InstMatch m; //if it produces a match, then process it with the rest - if( ((InstMatchGenerator*)d_children[i])->getMatch( t, m, qe ) ){ + if( ((InstMatchGenerator*)d_children[i])->getMatch( f, t, m, qe ) ){ processNewMatch( qe, m, i, addedLemmas ); } } diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h index af65e809b..a544f605a 100755 --- a/src/theory/quantifiers/inst_match_generator.h +++ b/src/theory/quantifiers/inst_match_generator.h @@ -38,11 +38,13 @@ public: /** reset, eqc is the equivalence class to search in (any if eqc=null) */ virtual void reset( Node eqc, QuantifiersEngine* qe ) = 0; /** get the next match. must call reset( eqc ) before this function. */ - virtual bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) = 0; + virtual bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) = 0; /** add instantiations directly */ virtual int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ) = 0; /** add ground term t, called when t is added to term db */ virtual int addTerm( Node f, Node t, QuantifiersEngine* qe ) = 0; + /** set active add */ + virtual void setActiveAdd() {} };/* class IMGenerator */ class CandidateGenerator; @@ -78,7 +80,7 @@ private: /** get the next match. must call d_cg->reset( ... ) before using. only valid for use where !d_match_pattern.isNull(). */ - bool getNextMatch2( InstMatch& m, QuantifiersEngine* qe, bool saveMatched = false ); + bool getNextMatch2( Node f, InstMatch& m, QuantifiersEngine* qe, bool saveMatched = false ); /** for arithmetic */ bool getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe ); public: @@ -86,7 +88,7 @@ public: d_match_pattern and t should have the same shape. only valid for use where !d_match_pattern.isNull(). */ - bool getMatch( Node t, InstMatch& m, QuantifiersEngine* qe ); + bool getMatch( Node f, Node t, InstMatch& m, QuantifiersEngine* qe ); /** constructors */ InstMatchGenerator( Node pat, QuantifiersEngine* qe, int matchOption = 0 ); @@ -105,11 +107,14 @@ public: /** reset, eqc is the equivalence class to search in (any if eqc=null) */ void reset( Node eqc, QuantifiersEngine* qe ); /** get the next match. must call reset( eqc ) before this function. */ - bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ); + bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ); /** add instantiations */ int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ); /** add ground term t */ int addTerm( Node f, Node t, QuantifiersEngine* qe ); + + bool d_active_add; + void setActiveAdd(); };/* class InstMatchGenerator */ /** smart multi-trigger implementation */ @@ -152,7 +157,7 @@ public: /** reset, eqc is the equivalence class to search in (any if eqc=null) */ void reset( Node eqc, QuantifiersEngine* qe ); /** get the next match. must call reset( eqc ) before this function. (not implemented) */ - bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; } + bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) { return false; } /** add instantiations */ int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ); /** add ground term t */ @@ -178,7 +183,7 @@ public: /** reset, eqc is the equivalence class to search in (any if eqc=null) */ void reset( Node eqc, QuantifiersEngine* qe ) {} /** get the next match. must call reset( eqc ) before this function. (not implemented) */ - bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; } + bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) { return false; } /** add instantiations */ int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ); /** add ground term t, possibly add instantiations */ diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 48af334ff..91cd2829c 100755 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -27,7 +27,6 @@ using namespace CVC4::theory; using namespace CVC4::theory::inst; using namespace CVC4::theory::quantifiers; -#define USE_SINGLE_TRIGGER_BEFORE_MULTI_TRIGGER //#define MULTI_TRIGGER_FULL_EFFORT_HALF #define MULTI_MULTI_TRIGGERS @@ -65,18 +64,13 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){ //Notice() << "Try user-provided patterns..." << std::endl; for( int i=0; i<(int)d_user_gen[f].size(); i++ ){ bool processTrigger = true; - if( effort!=Theory::EFFORT_LAST_CALL && d_user_gen[f][i]->isMultiTrigger() ){ -//#ifdef MULTI_TRIGGER_FULL_EFFORT_HALF -// processTrigger = d_counter[f]%2==0; -//#endif - } if( processTrigger ){ //if( d_user_gen[f][i]->isMultiTrigger() ) - //Notice() << " Process (user) " << (*d_user_gen[f][i]) << " for " << f << "..." << std::endl; + Trace("process-trigger") << " Process (user) " << (*d_user_gen[f][i]) << "..." << std::endl; InstMatch baseMatch; int numInst = d_user_gen[f][i]->addInstantiations( baseMatch ); //if( d_user_gen[f][i]->isMultiTrigger() ) - //Notice() << " Done, numInst = " << numInst << "." << std::endl; + Trace("process-trigger") << " Done, numInst = " << numInst << "." << std::endl; d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_user_patterns += numInst; if( d_user_gen[f][i]->isMultiTrigger() ){ d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst; @@ -125,6 +119,7 @@ void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort itt->first->reset( Node::null() ); } } + d_processed_trigger.clear(); } int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ){ @@ -134,6 +129,7 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ) if( efirst; if( tr ){ bool processTrigger = itt->second; - if( effort!=Theory::EFFORT_LAST_CALL && tr->isMultiTrigger() ){ -#ifdef MULTI_TRIGGER_FULL_EFFORT_HALF - processTrigger = d_counter[f]%2==0; -#endif - } - if( processTrigger ){ + if( processTrigger && d_processed_trigger[f].find( tr )==d_processed_trigger[f].end() ){ + d_processed_trigger[f][tr] = true; //if( tr->isMultiTrigger() ) - Debug("quant-uf-strategy-auto-gen-triggers") << " Process " << (*tr) << "..." << std::endl; + Trace("process-trigger") << " Process " << (*tr) << "..." << std::endl; InstMatch baseMatch; int numInst = tr->addInstantiations( baseMatch ); //if( tr->isMultiTrigger() ) - Debug("quant-uf-strategy-auto-gen-triggers") << " Done, numInst = " << numInst << "." << std::endl; + Trace("process-trigger") << " Done, numInst = " << numInst << "." << std::endl; if( d_tr_strategy==Trigger::TS_MIN_TRIGGER ){ d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_auto_gen_min += numInst; }else{ @@ -181,24 +173,24 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ) } Debug("quant-uf-strategy") << "done." << std::endl; //Notice() << "done" << std::endl; + return status; } - return STATUS_UNKNOWN; } -void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ - Debug("auto-gen-trigger") << "Generate trigger for " << f << std::endl; +void InstStrategyAutoGenTriggers::generateTriggers( Node f, Theory::Effort effort, int e, int & status ){ + Trace("auto-gen-trigger-debug") << "Generate trigger for " << f << std::endl; if( d_patTerms[0].find( f )==d_patTerms[0].end() ){ //determine all possible pattern terms based on trigger term selection strategy d_tr_strategy d_patTerms[0][f].clear(); d_patTerms[1][f].clear(); std::vector< Node > patTermsF; Trigger::collectPatTerms( d_quantEngine, f, d_quantEngine->getTermDatabase()->getInstConstantBody( f ), patTermsF, d_tr_strategy, true ); - Debug("auto-gen-trigger") << "Collected pat terms for " << d_quantEngine->getTermDatabase()->getInstConstantBody( f ) << std::endl; - Debug("auto-gen-trigger") << " "; + Trace("auto-gen-trigger") << "Collected pat terms for " << d_quantEngine->getTermDatabase()->getInstConstantBody( f ) << std::endl; + Trace("auto-gen-trigger") << " "; for( int i=0; i<(int)patTermsF.size(); i++ ){ - Debug("auto-gen-trigger") << patTermsF[i] << " "; + Trace("auto-gen-trigger") << patTermsF[i] << " "; } - Debug("auto-gen-trigger") << std::endl; + Trace("auto-gen-trigger") << std::endl; //extend to literal matching (if applicable) d_quantEngine->getPhaseReqTerms( f, patTermsF ); //sort into single/multi triggers @@ -214,23 +206,22 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ } } d_made_multi_trigger[f] = false; - Debug("auto-gen-trigger") << "Single triggers for " << f << " : " << std::endl; - Debug("auto-gen-trigger") << " "; + Trace("auto-gen-trigger") << "Single triggers for " << f << " : " << std::endl; + Trace("auto-gen-trigger") << " "; for( int i=0; i<(int)d_patTerms[0][f].size(); i++ ){ - Debug("auto-gen-trigger") << d_patTerms[0][f][i] << " "; + Trace("auto-gen-trigger") << d_patTerms[0][f][i] << " "; } - Debug("auto-gen-trigger") << std::endl; - Debug("auto-gen-trigger") << "Multi-trigger term pool for " << f << " : " << std::endl; - Debug("auto-gen-trigger") << " "; + Trace("auto-gen-trigger") << std::endl; + Trace("auto-gen-trigger") << "Multi-trigger term pool for " << f << " : " << std::endl; + Trace("auto-gen-trigger") << " "; for( int i=0; i<(int)d_patTerms[1][f].size(); i++ ){ - Debug("auto-gen-trigger") << d_patTerms[1][f][i] << " "; + Trace("auto-gen-trigger") << d_patTerms[1][f][i] << " "; } - Debug("auto-gen-trigger") << std::endl; + Trace("auto-gen-trigger") << std::endl; } //populate candidate pattern term vector for the current trigger std::vector< Node > patTerms; -#ifdef USE_SINGLE_TRIGGER_BEFORE_MULTI_TRIGGER //try to add single triggers first for( int i=0; i<(int)d_patTerms[0][f].size(); i++ ){ if( !d_single_trigger_gen[d_patTerms[0][f][i]] ){ @@ -241,13 +232,9 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ if( patTerms.empty() ){ patTerms.insert( patTerms.begin(), d_patTerms[1][f].begin(), d_patTerms[1][f].end() ); } -#else - patTerms.insert( patTerms.begin(), d_patTerms[0][f].begin(), d_patTerms[0][f].end() ); - patTerms.insert( patTerms.begin(), d_patTerms[1][f].begin(), d_patTerms[1][f].end() ); -#endif if( !patTerms.empty() ){ - Debug("auto-gen-trigger") << "Generate trigger for " << f << std::endl; + Trace("auto-gen-trigger") << "Generate trigger for " << f << std::endl; //sort terms based on relevance if( d_rlv_strategy==RELEVANCE_DEFAULT ){ sortQuantifiersForSymbol sqfs; @@ -273,6 +260,15 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ options::smartTriggers() ); d_single_trigger_gen[ patTerms[0] ] = true; }else{ + //only generate multi trigger if effort level > 5, or if no single triggers exist + if( !d_patTerms[0][f].empty() ){ + if( e<=5 ){ + status = STATUS_UNFINISHED; + return; + }else{ + Trace("multi-trigger-debug") << "Resort to choosing multi-triggers..." << std::endl; + } + } //if we are re-generating triggers, shuffle based on some method if( d_made_multi_trigger[f] ){ #ifndef MULTI_MULTI_TRIGGERS diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h index 23f0d8a54..fa4094634 100755 --- a/src/theory/quantifiers/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/inst_strategy_e_matching.h @@ -80,12 +80,14 @@ private: std::map< Node, bool > d_is_single_trigger; std::map< Node, bool > d_single_trigger_gen; std::map< Node, bool > d_made_multi_trigger; + //processed trigger this round + std::map< Node, std::map< inst::Trigger*, bool > > d_processed_trigger; private: /** process functions */ void processResetInstantiationRound( Theory::Effort effort ); int process( Node f, Theory::Effort effort, int e ); /** generate triggers */ - void generateTriggers( Node f ); + void generateTriggers( Node f, Theory::Effort effort, int e, int & status ); public: /** tstrt is the type of triggers to use (maximum depth, minimum depth, or all) rstrt is the relevance setting for trigger (use only relevant triggers vs. use all) diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index bc45e6051..eace177b7 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -45,8 +45,8 @@ option macrosQuant --macros-quant bool :default false option smartTriggers /--disable-smart-triggers bool :default true disable smart triggers # Whether to use relevent triggers -option relevantTriggers /--relevant-triggers bool :default true - prefer triggers that are more relevant based on SInE style method +option relevantTriggers --relevant-triggers bool :default true + prefer triggers that are more relevant based on SInE style analysis # Whether to consider terms in the bodies of quantifiers for matching option registerQuantBodyTerms --register-quant-body-terms bool :default false diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index d60aa2ef4..78109ea37 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -206,6 +206,7 @@ Node TermDb::getModelBasisTerm( TypeNode tn, int i ){ ModelBasisAttribute mba; mbt.setAttribute(mba,true); d_model_basis_term[tn] = mbt; + Trace("model-basis-term") << "Choose " << mbt << " as model basis term for " << tn << std::endl; } return d_model_basis_term[tn]; } @@ -367,6 +368,10 @@ Node TermDb::getSkolemizedBody( Node f ){ Node skv = NodeManager::currentNM()->mkSkolem( "skv_$$", f[0][i].getType(), "is a termdb-created skolemized body" ); d_skolem_constants[ f ].push_back( skv ); vars.push_back( f[0][i] ); + //carry information for sort inference + if( options::sortInference() ){ + d_quantEngine->getTheoryEngine()->getSortInference()->setSkolemVar( f, f[0][i], skv ); + } } d_skolem_body[ f ] = f[ 1 ].substitute( vars.begin(), vars.end(), d_skolem_constants[ f ].begin(), d_skolem_constants[ f ].end() ); @@ -515,6 +520,34 @@ int TermDb::isInstanceOf( Node n1, Node n2 ){ return 0; } +bool TermDb::isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& subs ){ + if( n1==n2 ){ + return true; + }else if( n2.getKind()==INST_CONSTANT ){ + //if( !node_contains( n1, n2 ) ){ + // return false; + //} + if( subs.find( n2 )==subs.end() ){ + subs[n2] = n1; + }else if( subs[n2]!=n1 ){ + return false; + } + return true; + }else if( n1.getKind()==n2.getKind() && n1.getMetaKind()==kind::metakind::PARAMETERIZED ){ + if( n1.getOperator()!=n2.getOperator() ){ + return false; + } + for( int i=0; i<(int)n1.getNumChildren(); i++ ){ + if( !isUnifiableInstanceOf( n1[i], n2[i], subs ) ){ + return false; + } + } + return true; + }else{ + return false; + } +} + void TermDb::filterInstances( std::vector< Node >& nodes ){ std::vector< bool > active; active.resize( nodes.size(), true ); @@ -523,8 +556,10 @@ void TermDb::filterInstances( std::vector< Node >& nodes ){ if( active[i] && active[j] ){ int result = isInstanceOf( nodes[i], nodes[j] ); if( result==1 ){ + Trace("filter-instances") << nodes[j] << " is an instance of " << nodes[i] << std::endl; active[j] = false; }else if( result==-1 ){ + Trace("filter-instances") << nodes[i] << " is an instance of " << nodes[j] << std::endl; active[i] = false; } } diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index a1f1de1dc..9ac431107 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -212,6 +212,8 @@ private: std::map< TNode, std::vector< TNode > > d_var_contains; /** triggers for each operator */ std::map< Node, std::vector< inst::Trigger* > > d_op_triggers; + /** helper for is intance of */ + bool isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& subs ); public: /** compute var contains */ void computeVarContains( Node n ); diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index bc577fda6..4b181a807 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -40,6 +40,7 @@ d_quantEngine( qe ), d_f( f ){ d_mg = new InstMatchGeneratorSimple( f, d_nodes[0] ); }else{ d_mg = new InstMatchGenerator( d_nodes[0], qe, matchOption ); + d_mg->setActiveAdd(); } }else{ d_mg = new InstMatchGeneratorMulti( f, d_nodes, qe, matchOption ); @@ -59,7 +60,7 @@ d_quantEngine( qe ), d_f( f ){ ++(qe->d_statistics.d_simple_triggers); } }else{ - Debug("multi-trigger") << "Multi-trigger " << (*this) << std::endl; + Trace("multi-trigger") << "Multi-trigger " << (*this) << " for " << f << std::endl; //Notice() << "Multi-trigger for " << f << " : " << std::endl; //Notice() << " " << (*this) << std::endl; ++(qe->d_statistics.d_multi_triggers); @@ -80,14 +81,14 @@ void Trigger::reset( Node eqc ){ d_mg->reset( eqc, d_quantEngine ); } -bool Trigger::getNextMatch( InstMatch& m ){ - bool retVal = d_mg->getNextMatch( m, d_quantEngine ); +bool Trigger::getNextMatch( Node f, InstMatch& m ){ + bool retVal = d_mg->getNextMatch( f, m, d_quantEngine ); return retVal; } -bool Trigger::getMatch( Node t, InstMatch& m ){ +bool Trigger::getMatch( Node f, Node t, InstMatch& m ){ //FIXME: this assumes d_mg is an inst match generator - return ((InstMatchGenerator*)d_mg)->getMatch( t, m, d_quantEngine ); + return ((InstMatchGenerator*)d_mg)->getMatch( f, t, m, d_quantEngine ); } int Trigger::addTerm( Node t ){ @@ -115,6 +116,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& temp.insert( temp.begin(), nodes.begin(), nodes.end() ); std::map< Node, bool > vars; std::map< Node, std::vector< Node > > patterns; + size_t varCount = 0; for( int i=0; i<(int)temp.size(); i++ ){ bool foundVar = false; qe->getTermDatabase()->computeVarContains( temp[i] ); @@ -122,6 +124,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& Node v = qe->getTermDatabase()->d_var_contains[ temp[i] ][j]; if( v.getAttribute(InstConstantAttribute())==f ){ if( vars.find( v )==vars.end() ){ + varCount++; vars[ v ] = true; foundVar = true; } @@ -134,32 +137,40 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& patterns[ v ].push_back( temp[i] ); } } - } - //now, minimalize the trigger - for( int i=0; i<(int)trNodes.size(); i++ ){ - bool keepPattern = false; - Node n = trNodes[i]; - for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ n ].size(); j++ ){ - Node v = qe->getTermDatabase()->d_var_contains[ n ][j]; - if( patterns[v].size()==1 ){ - keepPattern = true; - break; - } + if( varCount==f[0].getNumChildren() ){ + break; } - if( !keepPattern ){ - //remove from pattern vector + } + if( varCountgetTermDatabase()->d_var_contains[ n ].size(); j++ ){ Node v = qe->getTermDatabase()->d_var_contains[ n ][j]; - for( int k=0; k<(int)patterns[v].size(); k++ ){ - if( patterns[v][k]==n ){ - patterns[v].erase( patterns[v].begin() + k, patterns[v].begin() + k + 1 ); - break; + if( patterns[v].size()==1 ){ + keepPattern = true; + break; + } + } + if( !keepPattern ){ + //remove from pattern vector + for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ n ].size(); j++ ){ + Node v = qe->getTermDatabase()->d_var_contains[ n ][j]; + for( int k=0; k<(int)patterns[v].size(); k++ ){ + if( patterns[v][k]==n ){ + patterns[v].erase( patterns[v].begin() + k, patterns[v].begin() + k + 1 ); + break; + } } } + //remove from trigger nodes + trNodes.erase( trNodes.begin() + i, trNodes.begin() + i + 1 ); + i--; } - //remove from trigger nodes - trNodes.erase( trNodes.begin() + i, trNodes.begin() + i + 1 ); - i--; } } }else{ @@ -322,16 +333,16 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto temp.insert( temp.begin(), patTerms2.begin(), patTerms2.end() ); qe->getTermDatabase()->filterInstances( temp ); if( temp.size()!=patTerms2.size() ){ - Debug("trigger-filter-instance") << "Filtered an instance: " << std::endl; - Debug("trigger-filter-instance") << "Old: "; + Trace("trigger-filter-instance") << "Filtered an instance: " << std::endl; + Trace("trigger-filter-instance") << "Old: "; for( int i=0; i<(int)patTerms2.size(); i++ ){ - Debug("trigger-filter-instance") << patTerms2[i] << " "; + Trace("trigger-filter-instance") << patTerms2[i] << " "; } - Debug("trigger-filter-instance") << std::endl << "New: "; + Trace("trigger-filter-instance") << std::endl << "New: "; for( int i=0; i<(int)temp.size(); i++ ){ - Debug("trigger-filter-instance") << temp[i] << " "; + Trace("trigger-filter-instance") << temp[i] << " "; } - Debug("trigger-filter-instance") << std::endl; + Trace("trigger-filter-instance") << std::endl; } if( tstrt==TS_ALL ){ patTerms.insert( patTerms.begin(), temp.begin(), temp.end() ); diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 6fcd316f4..93731283b 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -56,12 +56,12 @@ public: /** reset, eqc is the equivalence class to search in (search in any if eqc=null) */ void reset( Node eqc ); /** get next match. must call reset( eqc ) once before this function. */ - bool getNextMatch( InstMatch& m ); + bool getNextMatch( Node f, InstMatch& m ); /** get the match against ground term or formula t. the trigger and t should have the same shape. Currently the trigger should not be a multi-trigger. */ - bool getMatch( Node t, InstMatch& m); + bool getMatch( Node f, Node t, InstMatch& m); /** add ground term t, called when t is added to the TermDb */ int addTerm( Node t ); /** return whether this is a multi-trigger */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 08bdd496b..f938199f8 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -71,6 +71,7 @@ d_lemmas_produced_c(u){ d_optMatchIgnoreModelBasis = false; d_optInstLimitActive = false; d_optInstLimit = 0; + d_total_inst_count_debug = 0; } QuantifiersEngine::~QuantifiersEngine(){ @@ -142,10 +143,23 @@ void QuantifiersEngine::check( Theory::Effort e ){ } //build the model if not done so already // this happens if no quantifiers are currently asserted and no model-building module is enabled - if( options::produceModels() && e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma && !d_model->isModelSet() ){ - d_te->getModelBuilder()->buildModel( d_model, true ); + if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){ + if( options::produceModels() && !d_model->isModelSet() ){ + d_te->getModelBuilder()->buildModel( d_model, true ); + } + if( Trace.isOn("inst-per-quant") ){ + for( std::map< Node, int >::iterator it = d_total_inst_debug.begin(); it != d_total_inst_debug.end(); ++it ){ + Trace("inst-per-quant") << " * " << it->second << " for " << it->first << std::endl; + } + } + }else{ + if( Trace.isOn("inst-per-quant-round") ){ + for( std::map< Node, int >::iterator it = d_temp_inst_debug.begin(); it != d_temp_inst_debug.end(); ++it ){ + Trace("inst-per-quant-round") << " * " << it->second << " for " << it->first << std::endl; + d_temp_inst_debug[it->first] = 0; + } + } } - Trace("quant-engine") << "Finished quantifiers engine check." << std::endl; } } @@ -242,6 +256,9 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std Node lem = nb; //check for duplication if( addLemma( lem ) ){ + d_total_inst_debug[f]++; + d_temp_inst_debug[f]++; + d_total_inst_count_debug++; Trace("inst") << "*** Instantiate " << f << " with " << std::endl; uint64_t maxInstLevel = 0; for( int i=0; i<(int)terms.size(); i++ ){ diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 29381a309..fa8a51d1f 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -119,6 +119,10 @@ private: rrinst::TriggerTrie* d_rr_tr_trie; /** extended model object */ quantifiers::FirstOrderModel* d_model; + /** statistics for debugging */ + std::map< Node, int > d_total_inst_debug; + std::map< Node, int > d_temp_inst_debug; + int d_total_inst_count_debug; private: KEEP_STATISTIC(TimerStat, d_time, "theory::QuantifiersEngine::time"); public: diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 27371eac3..388c0edf0 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -41,6 +41,7 @@ #include "util/hash.h" #include "util/cache.h" #include "util/cvc4_assert.h" +#include "util/sort_inference.h" #include "theory/ite_simplifier.h" #include "theory/unconstrained_simplifier.h" #include "theory/uf/equality_engine.h" @@ -422,6 +423,9 @@ class TheoryEngine { RemoveITE& d_iteRemover; + /** sort inference module */ + SortInference d_sortInfer; + /** Time spent in theory combination */ TimerStat d_combineTheoriesTime; @@ -732,6 +736,7 @@ public: SharedTermsDatabase* getSharedTermsDatabase() { return &d_sharedTerms; } + SortInference* getSortInference() { return &d_sortInfer; } private: std::map< std::string, std::vector< theory::Theory* > > d_attr_handle; public: diff --git a/src/theory/uf/options b/src/theory/uf/options index 2569ccbff..d6a2bb025 100644 --- a/src/theory/uf/options +++ b/src/theory/uf/options @@ -25,6 +25,8 @@ option ufssAbortCardinality --uf-ss-abort-card=N int :default -1 option ufssSmartSplits --uf-ss-smart-split bool :default false use smart splitting heuristic for uf strong solver option ufssExplainedCliques --uf-ss-explained-cliques bool :default false - add explained clique lemmas for uf strong solver + use explained clique lemmas for uf strong solver +option ufssSimpleCliques --uf-ss-simple-cliques bool :default true + always use simple clique lemmas for uf strong solver endmodule diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 46ac5aa60..0a96cf548 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -533,6 +533,7 @@ void StrongSolverTheoryUf::SortRepModel::assertDisequal( Node a, Node b, Node re //internal disequality d_regions[ai]->setDisequal( a, b, 1, true ); d_regions[ai]->setDisequal( b, a, 1, true ); + checkRegion( ai, false ); //do not need to check if it needs to combine (no new ext. disequalities) }else{ //external disequality d_regions[ai]->setDisequal( a, b, 0, true ); @@ -610,14 +611,33 @@ void StrongSolverTheoryUf::SortRepModel::check( Theory::Effort level, OutputChan if( level==Theory::EFFORT_FULL ){ if( !addedLemma ){ Trace("uf-ss-debug") << "No splits added. " << d_cardinality << std::endl; - if( !options::ufssColoringSat() ){ + Trace("uf-ss-si") << "Must combine region" << std::endl; + if( true || !options::ufssColoringSat() ){ bool recheck = false; //naive strategy, force region combination involving the first valid region - for( int i=0; i<(int)d_regions_index; i++ ){ - if( d_regions[i]->d_valid ){ - forceCombineRegion( i, false ); - recheck = true; - break; + if( options::sortInference()){ + std::map< int, int > sortsFound; + for( int i=0; i<(int)d_regions_index; i++ ){ + if( d_regions[i]->d_valid ){ + Node op = d_regions[i]->d_nodes.begin()->first; + int sort_id = d_th->getQuantifiersEngine()->getTheoryEngine()->getSortInference()->getSortId(op) ; + if( sortsFound.find( sort_id )!=sortsFound.end() ){ + combineRegions( sortsFound[sort_id], i ); + recheck = true; + break; + }else{ + sortsFound[sort_id] = i; + } + } + } + } + if( !recheck ) { + for( int i=0; i<(int)d_regions_index; i++ ){ + if( d_regions[i]->d_valid ){ + forceCombineRegion( i, false ); + recheck = true; + break; + } } } if( recheck ){ @@ -803,15 +823,10 @@ void StrongSolverTheoryUf::SortRepModel::assertCardinality( OutputChannel* out, } } -void StrongSolverTheoryUf::SortRepModel::checkRegion( int ri, bool rec ){ +void StrongSolverTheoryUf::SortRepModel::checkRegion( int ri, bool checkCombine ){ if( isValid(ri) && d_hasCard ){ Assert( d_cardinality>0 ); - //first check if region is in conflict - std::vector< Node > clique; - if( d_regions[ri]->check( Theory::EFFORT_STANDARD, d_cardinality, clique ) ){ - //explain clique - addCliqueLemma( clique, &d_th->getOutputChannel() ); - }else if( d_regions[ri]->getMustCombine( d_cardinality ) ){ + if( checkCombine && d_regions[ri]->getMustCombine( d_cardinality ) ){ ////alternatively, check if we can reduce the number of external disequalities by moving single nodes //for( std::map< Node, bool >::iterator it = d_regions[i]->d_reps.begin(); it != d_regions[i]->d_reps.end(); ++it ){ // if( it->second ){ @@ -822,10 +837,16 @@ void StrongSolverTheoryUf::SortRepModel::checkRegion( int ri, bool rec ){ // } //} int riNew = forceCombineRegion( ri, true ); - if( riNew>=0 && rec ){ - checkRegion( riNew, rec ); + if( riNew>=0 ){ + checkRegion( riNew, checkCombine ); } } + //now check if region is in conflict + std::vector< Node > clique; + if( d_regions[ri]->check( Theory::EFFORT_STANDARD, d_cardinality, clique ) ){ + //explain clique + addCliqueLemma( clique, &d_th->getOutputChannel() ); + } } } @@ -996,6 +1017,13 @@ bool StrongSolverTheoryUf::SortRepModel::addSplit( Region* r, OutputChannel* out Assert( s!=Node::null() && s.getKind()==EQUAL ); s = Rewriter::rewrite( s ); Trace("uf-ss-lemma") << "*** Split on " << s << std::endl; + if( options::sortInference()) { + for( int i=0; i<2; i++ ){ + int si = d_th->getQuantifiersEngine()->getTheoryEngine()->getSortInference()->getSortId( s[i] ); + Trace("uf-ss-split-si") << si << " "; + } + Trace("uf-ss-split-si") << std::endl; + } //Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areEqual( s[0], s[1] ) << " "; //Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areDisequal( s[0], s[1] ) << std::endl; //Trace("uf-ss-lemma") << s[0].getType() << " " << s[1].getType() << std::endl; @@ -1018,117 +1046,149 @@ void StrongSolverTheoryUf::SortRepModel::addCliqueLemma( std::vector< Node >& cl while( clique.size()>size_t(d_cardinality+1) ){ clique.pop_back(); } - if( !options::ufssExplainedCliques() ){ + if( options::ufssSimpleCliques() && !options::ufssExplainedCliques() ){ //add as lemma std::vector< Node > eqs; for( int i=0; i<(int)clique.size(); i++ ){ for( int j=0; jd_equalityEngine.getRepresentative(clique[i]); + Node r2 = d_th->d_equalityEngine.getRepresentative(clique[j]); eqs.push_back( clique[i].eqNode( clique[j] ) ); } } eqs.push_back( d_cardinality_literal[ d_cardinality ].notNode() ); Node lem = NodeManager::currentNM()->mkNode( OR, eqs ); + Trace("uf-ss-lemma") << "*** Add clique conflict " << lem << std::endl; + ++( d_th->getStrongSolver()->d_statistics.d_clique_lemmas ); out->lemma( lem ); - return; - } - //if( options::ufssModelInference() || - if( Trace.isOn("uf-ss-cliques") ){ - std::vector< Node > clique_vec; - clique_vec.insert( clique_vec.begin(), clique.begin(), clique.end() ); - d_cliques[ d_cardinality ].push_back( clique_vec ); - } - - //found a clique - Debug("uf-ss-cliques") << "Found a clique (cardinality=" << d_cardinality << ") :" << std::endl; - Debug("uf-ss-cliques") << " "; - for( int i=0; i<(int)clique.size(); i++ ){ - Debug("uf-ss-cliques") << clique[i] << " "; - } - Debug("uf-ss-cliques") << std::endl; - Debug("uf-ss-cliques") << "Finding clique disequalities..." << std::endl; - std::vector< Node > conflict; - //collect disequalities, and nodes that must be equal within representatives - std::map< Node, std::map< Node, bool > > explained; - std::map< Node, std::map< Node, bool > > nodesWithinRep; - for( int i=0; i<(int)d_disequalities_index; i++ ){ - //if both sides of disequality exist in clique - Node r1 = d_th->d_equalityEngine.getRepresentative( d_disequalities[i][0][0] ); - Node r2 = d_th->d_equalityEngine.getRepresentative( d_disequalities[i][0][1] ); - if( r1!=r2 && ( explained.find( r1 )==explained.end() || explained[r1].find( r2 )==explained[r1].end() ) && - std::find( clique.begin(), clique.end(), r1 )!=clique.end() && - std::find( clique.begin(), clique.end(), r2 )!=clique.end() ){ - explained[r1][r2] = true; - explained[r2][r1] = true; - conflict.push_back( d_disequalities[i] ); - Debug("uf-ss-cliques") << " -> disequality : " << d_disequalities[i] << std::endl; - nodesWithinRep[r1][ d_disequalities[i][0][0] ] = true; - nodesWithinRep[r2][ d_disequalities[i][0][1] ] = true; - if( conflict.size()==(clique.size()*( clique.size()-1 )/2) ){ - break; + }else{ + //debugging information + if( Trace.isOn("uf-ss-cliques") ){ + std::vector< Node > clique_vec; + clique_vec.insert( clique_vec.begin(), clique.begin(), clique.end() ); + d_cliques[ d_cardinality ].push_back( clique_vec ); + } + //found a clique + Debug("uf-ss-cliques") << "Found a clique (cardinality=" << d_cardinality << ") :" << std::endl; + Debug("uf-ss-cliques") << " "; + for( int i=0; i<(int)clique.size(); i++ ){ + Debug("uf-ss-cliques") << clique[i] << " "; + } + Debug("uf-ss-cliques") << std::endl; + Debug("uf-ss-cliques") << "Finding clique disequalities..." << std::endl; + + //we will scan through each of the disequaltities + bool isSatConflict = true; + std::vector< Node > conflict; + //collect disequalities, and nodes that must be equal within representatives + std::map< Node, std::map< Node, bool > > explained; + std::map< Node, std::map< Node, bool > > nodesWithinRep; + //map from the reprorted clique members to those reported in the lemma + std::map< Node, Node > cliqueRepMap; + for( int i=0; i<(int)d_disequalities_index; i++ ){ + //if both sides of disequality exist in clique + Node r1 = d_th->d_equalityEngine.getRepresentative( d_disequalities[i][0][0] ); + Node r2 = d_th->d_equalityEngine.getRepresentative( d_disequalities[i][0][1] ); + if( r1!=r2 && ( explained.find( r1 )==explained.end() || explained[r1].find( r2 )==explained[r1].end() ) && + std::find( clique.begin(), clique.end(), r1 )!=clique.end() && + std::find( clique.begin(), clique.end(), r2 )!=clique.end() ){ + explained[r1][r2] = true; + explained[r2][r1] = true; + if( options::ufssExplainedCliques() ){ + conflict.push_back( d_disequalities[i] ); + Debug("uf-ss-cliques") << " -> disequality : " << d_disequalities[i] << std::endl; + nodesWithinRep[r1][ d_disequalities[i][0][0] ] = true; + nodesWithinRep[r2][ d_disequalities[i][0][1] ] = true; + }else{ + //get the terms we report in the lemma + Node ru1 = r1; + if( cliqueRepMap.find( r1 )==cliqueRepMap.end() ){ + ru1 = d_disequalities[i][0][0]; + cliqueRepMap[r1] = ru1; + }else{ + ru1 = cliqueRepMap[r1]; + } + Node ru2 = r2; + if( cliqueRepMap.find( r2 )==cliqueRepMap.end() ){ + ru2 = d_disequalities[i][0][1]; + cliqueRepMap[r2] = ru2; + }else{ + ru2 = cliqueRepMap[r2]; + } + if( ru1!=d_disequalities[i][0][0] || ru2!=d_disequalities[i][0][1] ){ + //disequalities have endpoints that are not connected within an equivalence class + // we will be producing a lemma, introducing a new literal ru1 != ru2 + conflict.push_back( ru1.eqNode( ru2 ).notNode() ); + isSatConflict = false; + }else{ + conflict.push_back( d_disequalities[i] ); + } + } + if( conflict.size()==(clique.size()*( clique.size()-1 )/2) ){ + break; + } } } - } - //Debug("uf-ss-cliques") << conflict.size() << " " << clique.size() << std::endl; - Assert( (int)conflict.size()==((int)clique.size()*( (int)clique.size()-1 )/2) ); - //Assert( (int)conflict.size()==(int)clique.size()*( (int)clique.size()-1 )/2 ); - Debug("uf-ss-cliques") << "Finding clique equalities internal to eq classes..." << std::endl; - //now, we must explain equalities within each equivalence class - for( std::map< Node, std::map< Node, bool > >::iterator it = nodesWithinRep.begin(); it != nodesWithinRep.end(); ++it ){ - if( it->second.size()>1 ){ - Node prev; - //add explanation of t1 = t2 = ... = tn - Debug("uf-ss-cliques") << "Explain "; - for( std::map< Node, bool >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ - if( prev!=Node::null() ){ - Debug("uf-ss-cliques") << " = "; - //explain it2->first and prev - std::vector< TNode > expl; - d_th->d_equalityEngine.explainEquality( it2->first, prev, true, expl ); - for( int i=0; i<(int)expl.size(); i++ ){ - if( std::find( conflict.begin(), conflict.end(), expl[i] )==conflict.end() ){ - conflict.push_back( expl[i] ); + if( options::ufssExplainedCliques() ){ + //Debug("uf-ss-cliques") << conflict.size() << " " << clique.size() << std::endl; + Assert( (int)conflict.size()==((int)clique.size()*( (int)clique.size()-1 )/2) ); + //Assert( (int)conflict.size()==(int)clique.size()*( (int)clique.size()-1 )/2 ); + Debug("uf-ss-cliques") << "Finding clique equalities internal to eq classes..." << std::endl; + //now, we must explain equalities within each equivalence class + for( std::map< Node, std::map< Node, bool > >::iterator it = nodesWithinRep.begin(); it != nodesWithinRep.end(); ++it ){ + if( it->second.size()>1 ){ + Node prev; + //add explanation of t1 = t2 = ... = tn + Debug("uf-ss-cliques") << "Explain "; + for( std::map< Node, bool >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ + if( prev!=Node::null() ){ + Debug("uf-ss-cliques") << " = "; + //explain it2->first and prev + std::vector< TNode > expl; + d_th->d_equalityEngine.explainEquality( it2->first, prev, true, expl ); + for( int i=0; i<(int)expl.size(); i++ ){ + if( std::find( conflict.begin(), conflict.end(), expl[i] )==conflict.end() ){ + conflict.push_back( expl[i] ); + } + } } + prev = it2->first; + Debug("uf-ss-cliques") << prev; } + Debug("uf-ss-cliques") << std::endl; } - prev = it2->first; - Debug("uf-ss-cliques") << prev; + } + Debug("uf-ss-cliques") << "Explanation of clique (size=" << conflict.size() << ") = " << std::endl; + for( int i=0; i<(int)conflict.size(); i++ ){ + Debug("uf-ss-cliques") << conflict[i] << " "; } Debug("uf-ss-cliques") << std::endl; } - } - Debug("uf-ss-cliques") << "Explanation of clique (size=" << conflict.size() << ") = " << std::endl; - for( int i=0; i<(int)conflict.size(); i++ ){ - Debug("uf-ss-cliques") << conflict[i] << " "; - //bool value; - //bool hasValue = d_th->getValuation().hasSatValue( conflict[i], value ); - //Assert( hasValue ); - //Assert( value ); - } - Debug("uf-ss-cliques") << std::endl; - //now, make the conflict -#if 1 - conflict.push_back( d_cardinality_literal[ d_cardinality ] ); - Node conflictNode = NodeManager::currentNM()->mkNode( AND, conflict ); - Trace("uf-ss-lemma") << "*** Add clique conflict " << conflictNode << std::endl; - //Notice() << "*** Add clique conflict " << conflictNode << std::endl; - out->conflict( conflictNode ); - d_conflict = true; -#else - Node conflictNode = conflict.size()==1 ? conflict[0] : NodeManager::currentNM()->mkNode( AND, conflict ); - //add cardinality constraint - Node cardNode = d_cardinality_literal[ d_cardinality ]; - //bool value; - //bool hasValue = d_th->getValuation().hasSatValue( cardNode, value ); - //Assert( hasValue ); - //Assert( value ); - conflictNode = NodeManager::currentNM()->mkNode( IMPLIES, conflictNode, cardNode.notNode() ); - Trace("uf-ss-lemma") << "*** Add clique conflict " << conflictNode << std::endl; - //Notice() << "*** Add clique conflict " << conflictNode << std::endl; - out->lemma( conflictNode ); -#endif - ++( d_th->getStrongSolver()->d_statistics.d_clique_lemmas ); + //now, make the conflict + if( isSatConflict ){ + conflict.push_back( d_cardinality_literal[ d_cardinality ] ); + Node conflictNode = NodeManager::currentNM()->mkNode( AND, conflict ); + Trace("uf-ss-lemma") << "*** Add clique conflict " << conflictNode << std::endl; + //Notice() << "*** Add clique conflict " << conflictNode << std::endl; + out->conflict( conflictNode ); + d_conflict = true; + ++( d_th->getStrongSolver()->d_statistics.d_clique_conflicts ); + }else{ + Node conflictNode = conflict.size()==1 ? conflict[0] : NodeManager::currentNM()->mkNode( AND, conflict ); + //add cardinality constraint + Node cardNode = d_cardinality_literal[ d_cardinality ]; + //bool value; + //bool hasValue = d_th->getValuation().hasSatValue( cardNode, value ); + //Assert( hasValue ); + //Assert( value ); + conflictNode = NodeManager::currentNM()->mkNode( IMPLIES, conflictNode, cardNode.notNode() ); + Trace("uf-ss-lemma") << "*** Add clique lemma " << conflictNode << std::endl; + out->lemma( conflictNode ); + ++( d_th->getStrongSolver()->d_statistics.d_clique_lemmas ); + } - //DO_THIS: ensure that the same clique is not reported??? Check standard effort after assertDisequal can produce same clique. + //DO_THIS: ensure that the same clique is not reported??? Check standard effort after assertDisequal can produce same clique. + } } void StrongSolverTheoryUf::SortRepModel::addTotalityAxiom( Node n, int cardinality, OutputChannel* out ){ @@ -1222,7 +1282,7 @@ int StrongSolverTheoryUf::SortRepModel::getNumRegions(){ } void StrongSolverTheoryUf::SortRepModel::getRepresentatives( std::vector< Node >& reps ){ - if( !options::ufssColoringSat() ){ + //if( !options::ufssColoringSat() ){ bool foundRegion = false; for( int i=0; i<(int)d_regions_index; i++ ){ //should not have multiple regions at this point @@ -1235,123 +1295,9 @@ void StrongSolverTheoryUf::SortRepModel::getRepresentatives( std::vector< Node > foundRegion = true; } } - }else{ - Unimplemented("Build representatives for fmf region sat is not implemented"); - } -} - - -/** initialize */ -void StrongSolverTheoryUf::InfRepModel::initialize( OutputChannel* out ){ - -} - -/** new node */ -void StrongSolverTheoryUf::InfRepModel::newEqClass( Node n ){ - d_rep[n] = n; - //d_const_rep[n] = n.getMetaKind()==metakind::CONSTANT; -} - -/** merge */ -void StrongSolverTheoryUf::InfRepModel::merge( Node a, Node b ){ - //d_rep[b] = false; - //d_const_rep[a] = d_const_rep[a] || d_const_rep[b]; - Node repb = d_rep[b]; - Assert( !repb.isNull() ); - if( repb.getMetaKind()==metakind::CONSTANT || isBadRepresentative( d_rep[a] ) ){ - d_rep[a] = repb; - } - d_rep[b] = Node::null(); -} - -/** check */ -void StrongSolverTheoryUf::InfRepModel::check( Theory::Effort level, OutputChannel* out ){ - -} - -/** minimize */ -bool StrongSolverTheoryUf::InfRepModel::minimize( OutputChannel* out ){ -#if 0 - bool retVal = true; -#else - bool retVal = !addSplit( out ); -#endif - if( retVal ){ - std::vector< Node > reps; - getRepresentatives( reps ); - Trace("uf-ss-fmf") << "Num representatives of type " << d_type << " : " << reps.size() << std::endl; - /* - for( int i=0; i<(int)reps.size(); i++ ){ - std::cout << reps[i] << " "; - } - std::cout << std::endl; - for( int i=0; i<(int)reps.size(); i++ ){ - std::cout << reps[i].getMetaKind() << " "; - } - std::cout << std::endl; - for( NodeNodeMap::iterator it = d_rep.begin(); it != d_rep.end(); ++it ){ - Node rep = (*it).second; - if( !rep.isNull() && !isBadRepresentative( rep ) ){ - for( NodeNodeMap::iterator it2 = d_rep.begin(); it2 != d_rep.end(); ++it2 ){ - Node rep2 = (*it2).second; - if( !rep2.isNull() && !isBadRepresentative( rep2 ) ){ - if( d_th->getQuantifiersEngine()->getEqualityQuery()->areDisequal( rep, rep2 ) ){ - std::cout << "1 "; - }else{ - std::cout << "0 "; - } - } - } - //std::cout << " : " << rep; - std::cout << std::endl; - } - } - */ - } - return retVal; -} - -/** get representatives */ -void StrongSolverTheoryUf::InfRepModel::getRepresentatives( std::vector< Node >& reps ){ - for( NodeNodeMap::iterator it = d_rep.begin(); it != d_rep.end(); ++it ){ - if( !(*it).second.isNull() ){ - reps.push_back( (*it).first ); - } - } -} - - -/** add split function */ -bool StrongSolverTheoryUf::InfRepModel::addSplit( OutputChannel* out ){ - std::vector< Node > visited; - for( NodeNodeMap::iterator it = d_rep.begin(); it != d_rep.end(); ++it ){ - Node rep = (*it).second; - if( !rep.isNull() && !isBadRepresentative( rep ) ){ - bool constRep = rep.getMetaKind()==metakind::CONSTANT; - for( size_t i=0; igetQuantifiersEngine()->getEqualityQuery()->areDisequal( rep, visited[i] ) ){ - //split on these nodes - Node eq = rep.eqNode( visited[i] ); - Trace("uf-ss-lemma") << "*** Split on " << eq << std::endl; - eq = Rewriter::rewrite( eq ); - Debug("uf-ss-lemma-debug") << "Rewritten " << eq << std::endl; - out->split( eq ); - //explore the equals branch first - out->requirePhase( eq, true ); - ++( d_th->getStrongSolver()->d_statistics.d_split_lemmas ); - return true; - } - } - } - visited.push_back( rep ); - } - } - return false; -} - -bool StrongSolverTheoryUf::InfRepModel::isBadRepresentative( Node n ){ - return n.getKind()==kind::PLUS; + //}else{ + // Unimplemented("Build representatives for fmf region sat is not implemented"); + //} } StrongSolverTheoryUf::StrongSolverTheoryUf(context::Context* c, context::UserContext* u, OutputChannel& out, TheoryUF* th) : @@ -1438,6 +1384,13 @@ void StrongSolverTheoryUf::check( Theory::Effort level ){ if( level==Theory::EFFORT_FULL ){ debugPrint( "uf-ss-debug" ); } + if( !d_conflict && level==Theory::EFFORT_FULL && options::ufssColoringSat() ){ + int lemmas = d_term_amb->disambiguateTerms( d_out ); + d_statistics.d_disamb_term_lemmas += lemmas; + if( lemmas>=0 ){ + return; + } + } for( std::map< TypeNode, RepModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ it->second->check( level, d_out ); if( it->second->isConflict() ){ @@ -1446,10 +1399,10 @@ void StrongSolverTheoryUf::check( Theory::Effort level ){ } } //disambiguate terms if necessary - if( !d_conflict && level==Theory::EFFORT_FULL && options::ufssColoringSat() ){ - Assert( d_term_amb!=NULL ); - d_statistics.d_disamb_term_lemmas += d_term_amb->disambiguateTerms( d_out ); - } + //if( !d_conflict && level==Theory::EFFORT_FULL && options::ufssColoringSat() ){ + // Assert( d_term_amb!=NULL ); + // d_statistics.d_disamb_term_lemmas += d_term_amb->disambiguateTerms( d_out ); + //} Trace("uf-ss-solver") << "Done StrongSolverTheoryUf: check " << level << std::endl; } } @@ -1481,9 +1434,6 @@ void StrongSolverTheoryUf::preRegisterTerm( TNode n ){ if( tn.isSort() ){ Trace("uf-ss-register") << "Preregister sort " << tn << "." << std::endl; rm = new SortRepModel( n, d_th->getSatContext(), d_th ); - }else if( tn.isInteger() ){ - //rm = new InfRepModel( tn, d_th->getSatContext(), d_th ); - //rm = new SortRepModel( tn, d_th->getSatContext(), d_th ); }else{ /* if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){ @@ -1603,12 +1553,14 @@ void StrongSolverTheoryUf::debugModel( TheoryModel* m ){ } StrongSolverTheoryUf::Statistics::Statistics(): + d_clique_conflicts("StrongSolverTheoryUf::Clique_Conflicts", 0), d_clique_lemmas("StrongSolverTheoryUf::Clique_Lemmas", 0), d_split_lemmas("StrongSolverTheoryUf::Split_Lemmas", 0), d_disamb_term_lemmas("StrongSolverTheoryUf::Disambiguate_Term_Lemmas", 0), d_totality_lemmas("StrongSolverTheoryUf::Totality_Lemmas", 0), d_max_model_size("StrongSolverTheoryUf::Max_Model_Size", 1) { + StatisticsRegistry::registerStat(&d_clique_conflicts); StatisticsRegistry::registerStat(&d_clique_lemmas); StatisticsRegistry::registerStat(&d_split_lemmas); StatisticsRegistry::registerStat(&d_disamb_term_lemmas); @@ -1617,6 +1569,7 @@ StrongSolverTheoryUf::Statistics::Statistics(): } StrongSolverTheoryUf::Statistics::~Statistics(){ + StatisticsRegistry::unregisterStat(&d_clique_conflicts); StatisticsRegistry::unregisterStat(&d_clique_lemmas); StatisticsRegistry::unregisterStat(&d_split_lemmas); StatisticsRegistry::unregisterStat(&d_disamb_term_lemmas); @@ -1667,11 +1620,12 @@ int TermDisambiguator::disambiguateTerms( OutputChannel* out ){ } Assert( children.size()>1 ); Node lem = NodeManager::currentNM()->mkNode( OR, children ); - Debug( "uf-ss-lemma" ) << "*** Disambiguate lemma : " << lem << std::endl; + Trace( "uf-ss-lemma" ) << "*** Disambiguate lemma : " << lem << std::endl; //Notice() << "*** Disambiguate lemma : " << lem << std::endl; out->lemma( lem ); d_term_amb[ eq ] = false; lemmaAdded++; + return lemmaAdded; } } } diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index febae2eae..ceb59d5c3 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -213,7 +213,7 @@ public: void setSplitScore( Node n, int s ); private: /** check if we need to combine region ri */ - void checkRegion( int ri, bool rec = true ); + void checkRegion( int ri, bool checkCombine = true ); /** force combine region */ int forceCombineRegion( int ri, bool useDensity = true ); /** merge regions */ @@ -292,42 +292,6 @@ public: /** get number of regions (for debugging) */ int getNumRegions(); }; /** class SortRepModel */ -private: - /** infinite rep model */ - class InfRepModel : public RepModel - { - protected: - /** theory uf pointer */ - TheoryUF* d_th; - /** list of representatives */ - NodeNodeMap d_rep; - /** whether representatives are constant */ - NodeBoolMap d_const_rep; - /** add split */ - bool addSplit( OutputChannel* out ); - /** is bad representative */ - bool isBadRepresentative( Node n ); - public: - InfRepModel( TypeNode tn, context::Context* c, TheoryUF* th ) : RepModel( tn ), - d_th( th ), d_rep( c ), d_const_rep( c ){} - virtual ~InfRepModel(){} - /** initialize */ - void initialize( OutputChannel* out ); - /** new node */ - void newEqClass( Node n ); - /** merge */ - void merge( Node a, Node b ); - /** assert terms are disequal */ - void assertDisequal( Node a, Node b, Node reason ){} - /** check */ - void check( Theory::Effort level, OutputChannel* out ); - /** minimize */ - bool minimize( OutputChannel* out ); - /** get representatives */ - void getRepresentatives( std::vector< Node >& reps ); - /** print debug */ - void debugPrint( const char* c ){} - }; private: /** The output channel for the strong solver. */ OutputChannel* d_out; @@ -393,6 +357,7 @@ public: class Statistics { public: + IntStat d_clique_conflicts; IntStat d_clique_lemmas; IntStat d_split_lemmas; IntStat d_disamb_term_lemmas; diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp index 7e0af3e9f..cab5dac42 100755 --- a/src/util/sort_inference.cpp +++ b/src/util/sort_inference.cpp @@ -58,6 +58,14 @@ void SortInference::simplify( std::vector< Node >& assertions, bool doRewrite ){ printSort( "sort-inference", it->second ); Trace("sort-inference") << std::endl; } + for( std::map< Node, std::map< Node, int > >::iterator it = d_var_types.begin(); it != d_var_types.end(); ++it ){ + Trace("sort-inference") << "Quantified formula " << it->first << " : " << std::endl; + for( std::map< Node, int >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ + printSort( "sort-inference", it2->second ); + Trace("sort-inference") << std::endl; + } + Trace("sort-inference") << std::endl; + } } if( doRewrite ){ //simplify all assertions by introducing new symbols wherever necessary (NOTE: this is unsound for quantifiers) @@ -149,11 +157,11 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound ){ if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){ for( size_t i=0; i& var_bound ){ } } +int SortInference::getSortId( Node n ) { + Node op = n.getKind()==kind::APPLY_UF ? n.getOperator() : n; + return getRepresentative( d_op_return_types[op] ); +} + +int SortInference::getSortId( Node f, Node v ) { + return getRepresentative( d_var_types[f][v] ); +} +void SortInference::setSkolemVar( Node f, Node v, Node sk ){ + d_op_return_types[sk] = getSortId( f, v ); } + +} \ No newline at end of file diff --git a/src/util/sort_inference.h b/src/util/sort_inference.h index 363dbd84d..1378a266c 100755 --- a/src/util/sort_inference.h +++ b/src/util/sort_inference.h @@ -65,6 +65,10 @@ public: ~SortInference(){} void simplify( std::vector< Node >& assertions, bool doRewrite = false ); + int getSortId( Node n ); + int getSortId( Node f, Node v ); + //set that sk is the skolem variable of v for quantifier f + void setSkolemVar( Node f, Node v, Node sk ); }; } diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 938e7e5c1..b81bcf799 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -143,8 +143,8 @@ BUG_TESTS = \ bug421.smt2 \ bug421b.smt2 \ bug425.cvc \ - bug480.smt2 -# bug486.cvc + bug480.smt2 \ + bug486.cvc TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 112da2a6e..3e04c8437 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -36,8 +36,10 @@ TESTS = \ smtlib46f14a.smt2 \ smtlibf957ea.smt2 \ gauss_init_0030.fof.smt2 \ - piVC_5581bd.smt2 \ - set3.smt2 + piVC_5581bd.smt2 + +# regression can be solved with --finite-model-find --fmf-inst-engine +# set3.smt2 # removed because it now reports unknown # symmetric_unsat_7.smt2 \ -- 2.30.2