From bc3f6fdaf84da10f5fd5ad3a5f5700ec242dd082 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 16 Sep 2014 16:56:10 +0200 Subject: [PATCH] Refactoring of conjecture generator. Determine subgoals are non-canonical based on ground equalities. Add filtering options to options file. --- src/smt/smt_engine.cpp | 11 + .../quantifiers/conjecture_generator.cpp | 630 ++++++++++-------- src/theory/quantifiers/conjecture_generator.h | 28 +- src/theory/quantifiers/options | 11 +- src/theory/quantifiers/term_database.cpp | 30 + src/theory/quantifiers/term_database.h | 2 + 6 files changed, 414 insertions(+), 298 deletions(-) mode change 100644 => 100755 src/theory/quantifiers/conjecture_generator.cpp mode change 100644 => 100755 src/theory/quantifiers/conjecture_generator.h diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index cd3a7943e..caa757426 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1310,6 +1310,17 @@ void SmtEngine::setDefaults() { options::purifyTriggers.set( true ); } } + if( options::conjectureNoFilter() ){ + if( !options::conjectureFilterActiveTerms.wasSetByUser() ){ + options::conjectureFilterActiveTerms.set( false ); + } + if( !options::conjectureFilterCanonical.wasSetByUser() ){ + options::conjectureFilterCanonical.set( false ); + } + if( !options::conjectureFilterModel.wasSetByUser() ){ + options::conjectureFilterModel.set( false ); + } + } //until bugs 371,431 are fixed if( ! options::minisatUseElim.wasSetByUser()){ diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp old mode 100644 new mode 100755 index 0b8e0e462..018460466 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -103,6 +103,7 @@ void ConjectureGenerator::eqNotifyPreMerge(TNode t1, TNode t2) { } Trace("thm-ee-debug") << "UEE : equality holds : " << t1 << " == " << t2 << std::endl; Trace("thm-ee-debug") << " ureps : " << rt1 << " == " << rt2 << std::endl; + Trace("thm-ee-debug") << " relevant : " << d_pattern_is_relevant[rt1] << " " << d_pattern_is_relevant[rt2] << std::endl; Trace("thm-ee-debug") << " normal : " << d_pattern_is_normal[rt1] << " " << d_pattern_is_normal[rt2] << std::endl; Trace("thm-ee-debug") << " size : " << d_pattern_fun_sum[rt1] << " " << d_pattern_fun_sum[rt2] << std::endl; @@ -145,60 +146,6 @@ ConjectureGenerator::EqcInfo* ConjectureGenerator::getOrMakeEqcInfo( TNode n, bo } } -void ConjectureGenerator::doPendingAddUniversalTerms() { - //merge all pending equalities - while( !d_upendingAdds.empty() ){ - Trace("sg-pending") << "Add " << d_upendingAdds.size() << " pending terms..." << std::endl; - std::vector< Node > pending; - pending.insert( pending.end(), d_upendingAdds.begin(), d_upendingAdds.end() ); - d_upendingAdds.clear(); - for( unsigned i=0; i eq_terms; - d_thm_index.getEquivalentTerms( t, eq_terms ); - if( !eq_terms.empty() ){ - Trace("thm-ee-add") << "UEE : Based on theorem database, it is equivalent to " << eq_terms.size() << " terms : " << std::endl; - //add equivalent terms as equalities to universal engine - for( unsigned i=0; ihasTerm( t ) ){ - TNode grt = ee->getRepresentative( t ); - if( t!=grt ){ - Node exp; - d_uequalityEngine.assertEquality( t.eqNode( grt ), true, exp ); - } - } - */ - } - } -} - void ConjectureGenerator::setUniversalRelevant( TNode n ) { //add pattern information registerPattern( n, n.getType() ); @@ -210,22 +157,29 @@ void ConjectureGenerator::setUniversalRelevant( TNode n ) { bool ConjectureGenerator::isUniversalLessThan( TNode rt1, TNode rt2 ) { //prefer the one that is (normal, smaller) lexographically + Assert( d_pattern_is_relevant.find( rt1 )!=d_pattern_is_relevant.end() ); + Assert( d_pattern_is_relevant.find( rt2 )!=d_pattern_is_relevant.end() ); Assert( d_pattern_is_normal.find( rt1 )!=d_pattern_is_normal.end() ); Assert( d_pattern_is_normal.find( rt2 )!=d_pattern_is_normal.end() ); Assert( d_pattern_fun_sum.find( rt1 )!=d_pattern_fun_sum.end() ); Assert( d_pattern_fun_sum.find( rt2 )!=d_pattern_fun_sum.end() ); - if( d_pattern_is_normal[rt1] && !d_pattern_is_normal[rt2] ){ - Trace("thm-ee-debug") << "UEE : LT due to normal." << std::endl; + if( d_pattern_is_relevant[rt1] && !d_pattern_is_relevant[rt2] ){ + Trace("thm-ee-debug") << "UEE : LT due to relevant." << std::endl; return true; - }else if( d_pattern_is_normal[rt1]==d_pattern_is_normal[rt2] ){ - if( d_pattern_fun_sum[rt1] pending; + pending.insert( pending.end(), d_upendingAdds.begin(), d_upendingAdds.end() ); + d_upendingAdds.clear(); + for( unsigned i=0; i eq_terms; + //if occurs modulo equality at ground level, it is equivalent to representative of ground equality engine + TNode gt = getTermDatabase()->evaluateTerm( t ); + if( !gt.isNull() && gt!=t ){ + eq_terms.push_back( gt ); + } + //get all equivalent terms based on theorem database + d_thm_index.getEquivalentTerms( t, eq_terms ); + if( !eq_terms.empty() ){ + Trace("thm-ee-add") << "UEE : Based on ground EE/theorem DB, it is equivalent to " << eq_terms.size() << " terms : " << std::endl; + //add equivalent terms as equalities to universal engine + for( unsigned i=0; i >::iterator it = d_typ_funcs.begin(); it != d_typ_funcs.end(); ++it ){ d_typ_tg_funcs[it->first].insert( d_typ_tg_funcs[it->first].end(), it->second.begin(), it->second.end() ); } std::map< TypeNode, unsigned > rt_var_max; std::vector< TypeNode > rt_types; - std::map< int, std::vector< Node > > conj_lhs; - std::map< int, std::vector< Node > > conj_rhs; - //map from generalization depth to maximum depth - //std::map< unsigned, unsigned > gdepth_to_tdepth; - for( unsigned depth=1; depth<3; depth++ ){ + std::map< TypeNode, std::map< int, std::vector< Node > > > conj_lhs; + for( unsigned depth=1; depth<=3; depth++ ){ Assert( d_tg_alloc.empty() ); - Trace("sg-proc") << "Generate terms at depth " << depth << "..." << std::endl; + Trace("sg-proc") << "Generate relevant LHS at depth " << depth << "..." << std::endl; Trace("sg-rel-term") << "Relevant terms of depth " << depth << " : " << std::endl; //set up environment + for( unsigned i=0; i<2; i++ ){ + d_ccand_eqc[i].clear(); + d_ccand_eqc[i].push_back( d_relevant_eqc[i] ); + } d_var_id.clear(); d_var_limit.clear(); d_tg_id = 0; d_tg_gdepth = 0; d_tg_gdepth_limit = depth; + d_gen_relevant_terms = true; //consider all types d_tg_alloc[0].reset( this, TypeNode::null() ); while( d_tg_alloc[0].getNextTerm( this, depth ) ){ - Assert( d_tg_alloc[0].getGeneralizationDepth( this )==d_tg_gdepth ); + //Assert( d_tg_alloc[0].getGeneralizationDepth( this )==d_tg_gdepth ); //if( d_tg_alloc[0].getDepth( this )==depth ){ - if( (int)d_tg_gdepth==d_tg_gdepth_limit ){ + if( d_tg_alloc[0].getGeneralizationDepth( this )==depth ){ //construct term Node nn = d_tg_alloc[0].getTerm( this ); if( getUniversalRepresentative( nn )==nn ){ - d_rel_term_count++; + rel_term_count++; Trace("sg-rel-term") << "*** Relevant term : "; d_tg_alloc[0].debugPrint( this, "sg-rel-term", "sg-rel-term-debug2" ); Trace("sg-rel-term") << std::endl; @@ -720,7 +721,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { } TypeNode tnn = nn.getType(); Trace("sg-gen-tg-debug") << "...term is " << nn << std::endl; - conj_lhs[depth].push_back( nn ); + conj_lhs[tnn][depth].push_back( nn ); //add information about pattern Trace("sg-gen-tg-debug") << "Collect pattern information..." << std::endl; @@ -805,104 +806,143 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { } } Trace("sg-proc") << "...done generate terms at depth " << depth << std::endl; - + Trace("sg-stats") << "--------> Total LHS of depth : " << rel_term_count << std::endl; + //Trace("conjecture-count") << "Total LHS of depth " << depth << " : " << conj_lhs[depth].size() << std::endl; //now generate right hand sides - - } - Trace("sg-stats") << "--------> Total relevant patterns : " << d_rel_term_count << std::endl; - - Trace("sg-proc") << "Generate properties..." << std::endl; - //set up environment - d_use_ccand_eqc = false; - d_var_id.clear(); - d_var_limit.clear(); - for( std::map< TypeNode, unsigned >::iterator it = rt_var_max.begin(); it != rt_var_max.end(); ++it ){ - d_var_id[ it->first ] = it->second; - d_var_limit[ it->first ] = it->second; - } - //set up environment for candidate conjectures - //d_cconj_at_depth.clear(); - //for( unsigned i=0; i<2; i++ ){ - // d_cconj[i].clear(); - //} - //d_cconj_rhs_paired.clear(); - unsigned totalCount = 0; - for( unsigned depth=0; depth<5; depth++ ){ //consider types from relevant terms - std::random_shuffle( rt_types.begin(), rt_types.end() ); - for( unsigned i=0; i::iterator it = rt_var_max.begin(); it != rt_var_max.end(); ++it ){ + d_var_id[ it->first ] = it->second; + d_var_limit[ it->first ] = it->second; + } + std::random_shuffle( rt_types.begin(), rt_types.end() ); + std::map< TypeNode, std::vector< Node > > conj_rhs; + for( unsigned i=0; i=0; rhs_d-- ){ - int lhs_d = (depth-rhs_d)+1; - for( unsigned i=0; i=optFullCheckConjectures() ){ + break; + } + Trace("sg-proc") << "Consider conjectures at depth (" << lhs_depth << ", " << rdepth << ")..." << std::endl; + for( std::map< TypeNode, std::vector< Node > >::iterator it = conj_rhs.begin(); it != conj_rhs.end(); ++it ){ + for( unsigned j=0; jsecond.size(); j++ ){ + for( unsigned k=0; kfirst][lhs_depth].size(); k++ ){ + processCandidateConjecture( conj_lhs[it->first][lhs_depth][k], it->second[j], lhs_depth, rdepth ); + } + } + } } } } - Trace("sg-proc") << "...done process candidate conjectures at RHS term depth " << depth << std::endl; + if( optStatsOnly() ){ + Trace("conjecture-count") << "Generated " << d_waiting_conjectures_lhs.size() << " conjectures for depth " << depth << "." << std::endl; + d_waiting_conjectures_lhs.clear(); + d_waiting_conjectures_rhs.clear(); + }else if( d_waiting_conjectures_lhs.size()>=optFullCheckConjectures() ){ + break; + } } - Trace("sg-proc") << "...done generate properties" << std::endl; - - if( !d_waiting_conjectures.empty() ){ - Trace("sg-proc") << "Generated " << d_waiting_conjectures.size() << " conjectures." << std::endl; - d_conjectures.insert( d_conjectures.end(), d_waiting_conjectures.begin(), d_waiting_conjectures.end() ); - for( unsigned i=0; imkNode( OR, d_waiting_conjectures[i].negate(), d_waiting_conjectures[i] ); - d_quantEngine->addLemma( lem, false ); - d_quantEngine->addRequirePhase( d_waiting_conjectures[i], false ); + + if( !d_waiting_conjectures_lhs.empty() ){ + Trace("sg-proc") << "Generated " << d_waiting_conjectures_lhs.size() << " conjectures." << std::endl; + //TODO: prune conjectures in a smart way + for( unsigned i=0; ioptFullCheckConjectures() ){ + break; + }else{ + //we have determined a relevant subgoal + Node lhs = d_waiting_conjectures_lhs[i]; + Node rhs = d_waiting_conjectures_rhs[i]; + std::vector< Node > bvs; + for( std::map< TypeNode, unsigned >::iterator it = d_pattern_var_id[lhs].begin(); it != d_pattern_var_id[lhs].end(); ++it ){ + for( unsigned i=0; i<=it->second; i++ ){ + bvs.push_back( getFreeVar( it->first, i ) ); + } + } + Node rsg; + if( !bvs.empty() ){ + Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvs ); + rsg = NodeManager::currentNM()->mkNode( FORALL, bvl, lhs.eqNode( rhs ) ); + }else{ + rsg = lhs.eqNode( rhs ); + } + rsg = Rewriter::rewrite( rsg ); + Trace("sg-lemma") << "Constructed : " << rsg << std::endl; + d_conjectures.push_back( rsg ); + d_eq_conjectures[lhs].push_back( rhs ); + d_eq_conjectures[rhs].push_back( lhs ); + + Node lem = NodeManager::currentNM()->mkNode( OR, rsg.negate(), rsg ); + d_quantEngine->addLemma( lem, false ); + d_quantEngine->addRequirePhase( rsg, false ); + } } + d_waiting_conjectures_lhs.clear(); + d_waiting_conjectures_rhs.clear(); d_waiting_conjectures.clear(); } - Trace("thm-ee") << "Universal equality engine is : " << std::endl; - eq::EqClassesIterator ueqcs_i = eq::EqClassesIterator( &d_uequalityEngine ); - while( !ueqcs_i.isFinished() ){ - TNode r = (*ueqcs_i); - bool firstTime = true; - TNode rr = getUniversalRepresentative( r ); - Trace("thm-ee") << " " << r; - if( rr!=r ){ Trace("thm-ee") << " [" << rr << "]"; } - Trace("thm-ee") << " : { "; - eq::EqClassIterator ueqc_i = eq::EqClassIterator( r, &d_uequalityEngine ); - while( !ueqc_i.isFinished() ){ - TNode n = (*ueqc_i); - if( r!=n ){ - if( firstTime ){ - Trace("thm-ee") << std::endl; - firstTime = false; + if( Trace.isOn("thm-ee") ){ + Trace("thm-ee") << "Universal equality engine is : " << std::endl; + eq::EqClassesIterator ueqcs_i = eq::EqClassesIterator( &d_uequalityEngine ); + while( !ueqcs_i.isFinished() ){ + TNode r = (*ueqcs_i); + bool firstTime = true; + TNode rr = getUniversalRepresentative( r ); + Trace("thm-ee") << " " << r; + if( rr!=r ){ Trace("thm-ee") << " [" << rr << "]"; } + Trace("thm-ee") << " : { "; + eq::EqClassIterator ueqc_i = eq::EqClassIterator( r, &d_uequalityEngine ); + while( !ueqc_i.isFinished() ){ + TNode n = (*ueqc_i); + if( r!=n ){ + if( firstTime ){ + Trace("thm-ee") << std::endl; + firstTime = false; + } + Trace("thm-ee") << " " << n << std::endl; } - Trace("thm-ee") << " " << n << std::endl; + ++ueqc_i; } - ++ueqc_i; + if( !firstTime ){ Trace("thm-ee") << " "; } + Trace("thm-ee") << "}" << std::endl; + ++ueqcs_i; } - if( !firstTime ){ Trace("thm-ee") << " "; } - Trace("thm-ee") << "}" << std::endl; - ++ueqcs_i; + Trace("thm-ee") << std::endl; } - Trace("thm-ee") << std::endl; } } } @@ -960,9 +1000,7 @@ bool ConjectureGenerator::considerCurrentTerm() { Trace("sg-gen-tg-debug") << "? curr term size = " << d_tg_alloc.size() << ", last status = " << d_tg_alloc[i-1].d_status; Trace("sg-gen-tg-debug") << std::endl; - Assert( d_tg_alloc[0].getGeneralizationDepth( this )==d_tg_gdepth ); - - if( d_tg_gdepth_limit>=0 && d_tg_gdepth>(unsigned)d_tg_gdepth_limit ){ + if( d_tg_gdepth_limit>=0 && d_tg_alloc[0].getGeneralizationDepth( this )>(unsigned)d_tg_gdepth_limit ){ Trace("sg-gen-consider-term") << "-> generalization depth of "; d_tg_alloc[0].debugPrint( this, "sg-gen-consider-term", "sg-gen-tg-debug" ); Trace("sg-gen-consider-term") << " is too high " << d_tg_gdepth << " " << d_tg_alloc[0].getGeneralizationDepth( this ) << ", do not consider." << std::endl; @@ -970,6 +1008,7 @@ bool ConjectureGenerator::considerCurrentTerm() { } //----optimizations + /* if( d_tg_alloc[i-1].d_status==1 ){ }else if( d_tg_alloc[i-1].d_status==2 ){ }else if( d_tg_alloc[i-1].d_status==5 ){ @@ -977,12 +1016,13 @@ bool ConjectureGenerator::considerCurrentTerm() { Trace("sg-gen-tg-debug") << "Bad tg: " << &d_tg_alloc[i-1] << std::endl; Assert( false ); } + */ //if equated two variables, first check if context-independent TODO //----end optimizations //check based on which candidate equivalence classes match - if( d_use_ccand_eqc ){ + if( d_gen_relevant_terms ){ Trace("sg-gen-tg-debug") << "Filter based on relevant ground EQC"; Trace("sg-gen-tg-debug") << ", #eqc to try = " << d_ccand_eqc[0][i-1].size() << "/" << d_ccand_eqc[1][i-1].size() << std::endl; @@ -1019,13 +1059,13 @@ bool ConjectureGenerator::considerCurrentTerm() { } Trace("sg-gen-tg-debug") << std::endl; } - if( d_ccand_eqc[0][i].empty() ){ + if( options::conjectureFilterActiveTerms() && d_ccand_eqc[0][i].empty() ){ Trace("sg-gen-consider-term") << "Do not consider term of form "; d_tg_alloc[0].debugPrint( this, "sg-gen-consider-term", "sg-gen-consider-term-debug" ); Trace("sg-gen-consider-term") << " since no relevant EQC matches it." << std::endl; return false; } - if( d_ccand_eqc[1][i].empty() && optFilterConfirmation() ){ + if( options::conjectureFilterModel() && d_ccand_eqc[1][i].empty() && optFilterConfirmation() ){ Trace("sg-gen-consider-term") << "Do not consider term of form "; d_tg_alloc[0].debugPrint( this, "sg-gen-consider-term", "sg-gen-consider-term-debug" ); Trace("sg-gen-consider-term") << " since no ground EQC matches it." << std::endl; @@ -1039,33 +1079,35 @@ bool ConjectureGenerator::considerCurrentTerm() { return true; } -bool ConjectureGenerator::considerTermCanon( unsigned tg_id ){ +bool ConjectureGenerator::considerCurrentTermCanon( unsigned tg_id ){ Assert( tg_id& mnvn, std::map< TypeNode, unsigned >& mxvn ){ if( pat.hasOperator() ){ funcs[pat.getOperator()]++; + if( !isRelevantFunc( pat.getOperator() ) ){ + d_pattern_is_relevant[opat] = false; + } unsigned sum = 1; for( unsigned i=0; i=optFullCheckConjectures() ){ - return; +int ConjectureGenerator::calculateGeneralizationDepth( TNode n, std::vector< TNode >& fv ) { + if( n.getKind()==BOUND_VARIABLE ){ + if( std::find( fv.begin(), fv.end(), n )==fv.end() ){ + fv.push_back( n ); + return 0; + }else{ + return 1; + } + }else{ + int depth = 1; + for( unsigned i=0; i trivial." << std::endl; @@ -1238,17 +1295,28 @@ bool ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) { return false; } } + //currently active conjecture? std::map< Node, std::vector< Node > >::iterator iteq = d_eq_conjectures.find( lhs ); if( iteq!=d_eq_conjectures.end() ){ if( std::find( iteq->second.begin(), iteq->second.end(), rhs )!=iteq->second.end() ){ + Trace("sg-cconj-debug") << " -> this conjecture is already active." << std::endl; + return false; + } + } + //current a waiting conjecture? + std::map< Node, std::vector< Node > >::iterator itw = d_waiting_conjectures.find( lhs ); + if( itw!=d_waiting_conjectures.end() ){ + if( std::find( itw->second.begin(), itw->second.end(), rhs )!=itw->second.end() ){ Trace("sg-cconj-debug") << " -> already are considering this conjecture." << std::endl; return false; } } + + Trace("sg-cconj") << "Consider possible candidate conjecture : " << lhs << " == " << rhs << "?" << std::endl; //find witness for counterexample, if possible - if( optFilterConfirmation() || optFilterFalsification() ){ + if( options::conjectureFilterModel() && ( optFilterConfirmation() || optFilterFalsification() ) ){ Assert( d_rel_pattern_var_sum.find( lhs )!=d_rel_pattern_var_sum.end() ); Trace("sg-cconj-debug") << "Notify substitutions over " << d_rel_pattern_var_sum[lhs] << " variables." << std::endl; std::map< TNode, TNode > subs; @@ -1266,12 +1334,12 @@ bool ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) { return false; } } - if( optFilterConfirmationDomain() ){ + if( optFilterConfirmationDomainThreshold()>0 ){ std::vector< TNode > vars; std::vector< TNode > subs; for( std::map< TNode, std::vector< TNode > >::iterator it = d_subs_confirmWitnessDomain.begin(); it != d_subs_confirmWitnessDomain.end(); ++it ){ Assert( d_pattern_fun_id[lhs].find( it->first )!=d_pattern_fun_id[lhs].end() ); - unsigned req = d_pattern_fun_id[lhs][it->first]; + unsigned req = optFilterConfirmationDomainThreshold() + (d_pattern_fun_id[lhs][it->first]-1); std::map< TNode, unsigned >::iterator itrf = d_pattern_fun_id[rhs].find( it->first ); if( itrf!=d_pattern_fun_id[rhs].end() ){ req = itrf->second>req ? itrf->second : req; @@ -1285,43 +1353,18 @@ bool ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) { subs.push_back( it->second[0] ); } } - if( optFilterConfirmationNonCanonical() && !vars.empty() ){ - Node slhs = lhs.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); - Node srhs = rhs.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); - TNode slhsr = getUniversalRepresentative( slhs, true ); - TNode srhsr = getUniversalRepresentative( srhs, true ); - if( areUniversalEqual( slhsr, srhsr ) ){ - Trace("sg-cconj") << " -> all ground witnesses can be proven by other theorems." << std::endl; - return false; - }else{ - Trace("sg-cconj-debug") << "Checked if " << slhsr << " and " << srhsr << " were equal." << std::endl; - } - } } - } - - Trace("sg-cconj") << " -> SUCCESS." << std::endl; - if( optFilterConfirmation() || optFilterFalsification() ){ + Trace("sg-cconj") << " -> SUCCESS." << std::endl; Trace("sg-cconj") << " confirmed = " << d_subs_confirmCount << ", #witnesses range = " << d_subs_confirmWitnessRange.size() << "." << std::endl; for( std::map< TNode, std::vector< TNode > >::iterator it = d_subs_confirmWitnessDomain.begin(); it != d_subs_confirmWitnessDomain.end(); ++it ){ Trace("sg-cconj") << " #witnesses for " << it->first << " : " << it->second.size() << std::endl; } } - /* - if( getUniversalRepresentative( lhs )!=lhs ){ - std::cout << "bad universal representative LHS : " << lhs << " " << getUniversalRepresentative( lhs ) << std::endl; - exit(0); - } - if( getUniversalRepresentative( rhs )!=rhs ){ - std::cout << "bad universal representative RHS : " << rhs << " " << getUniversalRepresentative( rhs ) << std::endl; - exit(0); - } - */ - //check if still canonical representation (should be, but for efficiency this is not guarenteed) - if( getUniversalRepresentative( lhs )!=lhs || getUniversalRepresentative( rhs )!=rhs ){ + if( options::conjectureFilterCanonical() && ( getUniversalRepresentative( lhs )!=lhs || getUniversalRepresentative( rhs )!=rhs ) ){ Trace("sg-cconj") << " -> after processing, not canonical." << std::endl; + return false; } return true; @@ -1360,20 +1403,13 @@ bool ConjectureGenerator::notifySubstitution( TNode glhs, std::map< TNode, TNode }else{ d_subs_unkCount++; if( optFilterUnknown() ){ + Trace("sg-cconj-debug") << "...ground substitution giving terms that are neither equal nor disequal." << std::endl; return false; } } } } } - /* - if( getEqualityEngine()->areDisequal( glhs, grhs, false ) ){ - Trace("sg-cconj-debug") << "..." << glhs << " and " << grhs << " are disequal." << std::endl; - return false; - }else{ - Trace("sg-cconj-debug") << "..." << glhs << " and " << grhs << " are not disequal." << std::endl; - } - */ }else{ Trace("sg-cconj-witness") << " Witnessed " << glhs << " == " << grhs << ", substutition is : " << std::endl; for( std::map< TNode, TNode >::iterator it = subs.begin(); it != subs.end(); ++it ){ @@ -1432,7 +1468,9 @@ bool TermGenerator::getNextTerm( ConjectureGenerator * s, unsigned depth ) { //check allocating new variable d_status++; d_status_num = -1; - s->d_tg_gdepth++; + if( s->d_gen_relevant_terms ){ + s->d_tg_gdepth++; + } return getNextTerm( s, depth ); } }else{ @@ -1453,7 +1491,9 @@ bool TermGenerator::getNextTerm( ConjectureGenerator * s, unsigned depth ) { Trace("sg-gen-tg-debug2") << this << "...consider other var #" << d_status_num << std::endl; return s->considerCurrentTerm() ? true : getNextTerm( s, depth ); }else{ - s->d_tg_gdepth--; + if( s->d_gen_relevant_terms ){ + s->d_tg_gdepth--; + } d_status++; return getNextTerm( s, depth ); } @@ -1487,7 +1527,7 @@ bool TermGenerator::getNextTerm( ConjectureGenerator * s, unsigned depth ) { return getNextTerm( s, depth ); }else if( d_status_child_num==(int)s->d_func_args[f].size() ){ d_status_child_num--; - return s->considerTermCanon( d_id ) ? true : getNextTerm( s, depth ); + return s->considerCurrentTermCanon( d_id ) ? true : getNextTerm( s, depth ); //return true; }else{ Assert( d_status_child_num<(int)s->d_func_args[f].size() ); @@ -1695,21 +1735,35 @@ unsigned TermGenerator::getDepth( ConjectureGenerator * s ) { } } -unsigned TermGenerator::getGeneralizationDepth( ConjectureGenerator * s ) { +unsigned TermGenerator::calculateGeneralizationDepth( ConjectureGenerator * s, std::map< TypeNode, std::vector< int > >& fvs ) { if( d_status==5 ){ unsigned sum = 1; for( unsigned i=0; id_tg_alloc[d_children[i]].getGeneralizationDepth( s ); + sum += s->d_tg_alloc[d_children[i]].calculateGeneralizationDepth( s, fvs ); } return sum; - }else if( d_status==2 ){ - return 1; }else{ - Assert( d_status==1 ); + Assert( d_status==2 || d_status==1 ); + std::map< TypeNode, std::vector< int > >::iterator it = fvs.find( d_typ ); + if( it!=fvs.end() ){ + if( std::find( it->second.begin(), it->second.end(), d_status_num )!=it->second.end() ){ + return 1; + } + } + fvs[d_typ].push_back( d_status_num ); return 0; } } +unsigned TermGenerator::getGeneralizationDepth( ConjectureGenerator * s ) { + //if( s->d_gen_relevant_terms ){ + // return s->d_tg_gdepth; + //}else{ + std::map< TypeNode, std::vector< int > > fvs; + return calculateGeneralizationDepth( s, fvs ); + //} +} + Node TermGenerator::getTerm( ConjectureGenerator * s ) { if( d_status==1 || d_status==2 ){ Assert( !d_typ.isNull() ); @@ -1811,8 +1865,9 @@ void TheoremIndex::addTheoremNode( TNode curr, std::vector< TNode >& lhs_v, std: d_children[curr.getOperator()].addTheorem( lhs_v, lhs_arg, rhs ); }else{ Assert( curr.getKind()==kind::BOUND_VARIABLE ); - Assert( d_var.isNull() || d_var==curr ); - d_var = curr; + TypeNode tn = curr.getType(); + Assert( d_var[tn].isNull() || d_var[tn]==curr ); + d_var[tn] = curr; d_children[curr].addTheorem( lhs_v, lhs_arg, rhs ); } } @@ -1855,26 +1910,27 @@ void TheoremIndex::getEquivalentTermsNode( Node curr, std::vector< TNode >& n_v, } Trace("thm-db-debug") << "...done check based on operator" << std::endl; } - if( !d_var.isNull() ){ - Trace("thm-db-debug") << "Check for substitution with " << d_var << "..." << std::endl; - if( curr.getType()==d_var.getType() ){ - //add to substitution if possible - bool success = false; - std::map< TNode, TNode >::iterator it = smap.find( d_var ); - if( it==smap.end() ){ - smap[d_var] = curr; - vars.push_back( d_var ); - subs.push_back( curr ); - success = true; - }else if( it->second==curr ){ - success = true; - }else{ - //also check modulo equality (in universal equality engine) - } - Trace("thm-db-debug") << "...check for substitution with " << d_var << ", success = " << success << "." << std::endl; - if( success ){ - d_children[d_var].getEquivalentTerms( n_v, n_arg, smap, vars, subs, terms ); - } + TypeNode tn = curr.getType(); + std::map< TypeNode, TNode >::iterator itt = d_var.find( tn ); + if( itt!=d_var.end() ){ + Trace("thm-db-debug") << "Check for substitution with " << itt->second << "..." << std::endl; + Assert( curr.getType()==itt->second.getType() ); + //add to substitution if possible + bool success = false; + std::map< TNode, TNode >::iterator it = smap.find( itt->second ); + if( it==smap.end() ){ + smap[itt->second] = curr; + vars.push_back( itt->second ); + subs.push_back( curr ); + success = true; + }else if( it->second==curr ){ + success = true; + }else{ + //also check modulo equality (in universal equality engine) + } + Trace("thm-db-debug") << "...check for substitution with " << itt->second << ", success = " << success << "." << std::endl; + if( success ){ + d_children[itt->second].getEquivalentTerms( n_v, n_arg, smap, vars, subs, terms ); } } } @@ -1903,12 +1959,14 @@ bool ConjectureGenerator::optReqDistinctVarPatterns() { return false; } bool ConjectureGenerator::optFilterFalsification() { return true; } bool ConjectureGenerator::optFilterUnknown() { return true; } //may change bool ConjectureGenerator::optFilterConfirmation() { return true; } -bool ConjectureGenerator::optFilterConfirmationDomain() { return true; } -bool ConjectureGenerator::optFilterConfirmationOnlyGround() { return true; }//false; } -bool ConjectureGenerator::optFilterConfirmationNonCanonical() { return false; }//true; } +unsigned ConjectureGenerator::optFilterConfirmationDomainThreshold() { return 1; } +bool ConjectureGenerator::optFilterConfirmationOnlyGround() { return true; } +bool ConjectureGenerator::optFilterConfirmationNonCanonical() { return false; } unsigned ConjectureGenerator::optFullCheckFrequency() { return 1; } unsigned ConjectureGenerator::optFullCheckConjectures() { return options::conjectureGenPerRound(); } +bool ConjectureGenerator::optStatsOnly() { return false; } + } diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h old mode 100644 new mode 100755 index 93cda7311..9e632557f --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -68,6 +68,8 @@ public: class TermGenerator { +private: + unsigned calculateGeneralizationDepth( ConjectureGenerator * s, std::map< TypeNode, std::vector< int > >& fvs ); public: TermGenerator(){} TypeNode d_typ; @@ -119,7 +121,7 @@ private: std::map< TNode, TNode >& smap, std::vector< TNode >& vars, std::vector< TNode >& subs, std::vector< Node >& terms ); public: - TNode d_var; + std::map< TypeNode, TNode > d_var; std::map< TNode, TheoremIndex > d_children; std::vector< Node > d_terms; @@ -137,7 +139,7 @@ public: getEquivalentTermsNode( n, nv, na, smap, vars, subs, terms ); } void clear(){ - d_var = Node::null(); + d_var.clear(); d_children.clear(); d_terms.clear(); } @@ -199,8 +201,6 @@ private: void eqNotifyPostMerge(TNode t1, TNode t2); /** called when two equivalence classes are made disequal */ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); - /** add pending universal terms, merge equivalence classes */ - void doPendingAddUniversalTerms(); /** are universal equal */ bool areUniversalEqual( TNode n1, TNode n2 ); /** are universal disequal */ @@ -223,7 +223,10 @@ private: //information regarding the conjectures /** list of all conjectures */ std::vector< Node > d_conjectures; /** list of all waiting conjectures */ - std::vector< Node > d_waiting_conjectures; + std::vector< Node > d_waiting_conjectures_lhs; + std::vector< Node > d_waiting_conjectures_rhs; + /** map of currently considered equality conjectures */ + std::map< Node, std::vector< Node > > d_waiting_conjectures; /** map of equality conjectures */ std::map< Node, std::vector< Node > > d_eq_conjectures; /** currently existing conjectures in equality engine */ @@ -267,7 +270,8 @@ private: //information regarding the terms // # duplicated variables std::map< TNode, unsigned > d_pattern_var_duplicate; // is normal pattern? (variables allocated in canonical way left to right) - std::map< TNode, bool > d_pattern_is_normal; + std::map< TNode, int > d_pattern_is_normal; + std::map< TNode, int > d_pattern_is_relevant; // patterns to a count of # operators (variables and functions) std::map< TNode, std::map< TNode, unsigned > > d_pattern_fun_id; // term size @@ -278,7 +282,6 @@ private: //information regarding the terms // add pattern void registerPattern( Node pat, TypeNode tpat ); private: //for debugging - unsigned d_rel_term_count; std::map< TNode, unsigned > d_em; public: //environment for term enumeration //the current number of enumerated variables per type @@ -288,7 +291,7 @@ public: //environment for term enumeration //the functions we can currently generate std::map< TypeNode, std::vector< TNode > > d_typ_tg_funcs; //the equivalence classes (if applicable) that match the currently generated term - bool d_use_ccand_eqc; + bool d_gen_relevant_terms; std::vector< std::vector< TNode > > d_ccand_eqc[2]; //the term generation objects unsigned d_tg_id; @@ -303,7 +306,7 @@ public: //environment for term enumeration unsigned getNumTgFuncs( TypeNode tn ); TNode getTgFunc( TypeNode tn, unsigned i ); bool considerCurrentTerm(); - bool considerTermCanon( unsigned tg_id ); + bool considerCurrentTermCanon( unsigned tg_id ); void changeContext( bool add ); public: //for generalization //generalizations @@ -312,6 +315,8 @@ public: //for generalization return isGeneralization( patg, pat, subs ); } bool isGeneralization( TNode patg, TNode pat, std::map< TNode, TNode >& subs ); + // get generalization depth + int calculateGeneralizationDepth( TNode n, std::vector< TNode >& fv ); public: //for property enumeration //process this candidate conjecture void processCandidateConjecture( TNode lhs, TNode rhs, unsigned lhs_depth, unsigned rhs_depth ); @@ -344,6 +349,7 @@ private: //information about ground equivalence classes Node getGroundEqc( TNode r ); bool isGroundEqc( TNode r ); bool isGroundTerm( TNode n ); + bool isRelevantFunc( Node f ); // count of full effort checks unsigned d_fullEffortCount; public: @@ -366,11 +372,13 @@ private: bool optFilterFalsification(); bool optFilterUnknown(); bool optFilterConfirmation(); - bool optFilterConfirmationDomain(); + unsigned optFilterConfirmationDomainThreshold(); bool optFilterConfirmationOnlyGround(); bool optFilterConfirmationNonCanonical(); //filter if all ground confirmations are non-canonical unsigned optFullCheckFrequency(); unsigned optFullCheckConjectures(); + + bool optStatsOnly(); }; diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index d30e5de4a..efe1b1098 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -160,6 +160,13 @@ option conjectureGen --conjecture-gen bool :read-write :default false generate candidate conjectures for inductive proofs option conjectureGenPerRound --conjecture-gen-per-round=N int :default 1 - number of conjectures to generate per instantiation round - + number of conjectures to generate per instantiation round +option conjectureNoFilter --conjecture-no-filter bool :default false + do not filter conjectures +option conjectureFilterActiveTerms --conjecture-filter-active-terms bool :read-write :default true + filter based on active terms +option conjectureFilterCanonical --conjecture-filter-canonical bool :read-write :default true + filter based on canonicity +option conjectureFilterModel --conjecture-filter-model bool :read-write :default true + filter based on model endmodule diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index cf68c198e..0d85eae83 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -227,6 +227,36 @@ TNode TermDb::evaluateTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRe } } +TNode TermDb::evaluateTerm( TNode n ) { + eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine(); + if( ee->hasTerm( n ) ){ + return ee->getRepresentative( n ); + }else if( n.getKind()!=BOUND_VARIABLE ){ + if( n.hasOperator() ){ + TNode f = getOperator( n ); + if( !f.isNull() ){ + std::vector< TNode > args; + for( unsigned i=0; ihasTerm( nn ) ){ + return ee->getRepresentative( nn ); + }else{ + //Assert( false ); + } + } + } + } + } + return TNode::null(); +} + bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol ) { Trace("term-db-eval") << "Check entailed : " << n << ", pol = " << pol << std::endl; Assert( n.getType().isBoolean() ); diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 504ecd667..91ad0135b 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -145,6 +145,8 @@ public: * subsRep is whether subs contains only representatives */ TNode evaluateTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep ); + /** same as above, but without substitution */ + TNode evaluateTerm( TNode n ); /** is entailed (incomplete check) */ bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol ); public: -- 2.30.2