From 83f91b92090ef0231156560f337affc6e5c2a33f Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 3 Sep 2014 12:35:00 +0200 Subject: [PATCH] Work on conjecture generator : do not generalize subterms with concrete values, filter conjectures with ground substitutions whose equality is unknown, simplify generalization depth calculation. Print --dump-instantiations on sat/unknown. --- src/main/command_executor.cpp | 5 +- src/main/command_executor_portfolio.cpp | 5 +- .../quantifiers/conjecture_generator.cpp | 156 ++++++------------ src/theory/quantifiers/conjecture_generator.h | 40 ++--- src/theory/quantifiers/options | 3 + 5 files changed, 76 insertions(+), 133 deletions(-) diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index fee7e23a2..4bbfe2762 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -22,6 +22,7 @@ #include "main/options.h" #include "smt/options.h" +#include "printer/options.h" #ifndef __WIN32__ # include @@ -132,7 +133,9 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) res.asSatisfiabilityResult() == Result::UNSAT ) { g = new GetProofCommand(); } else if( d_options[options::dumpInstantiations] && - res.asSatisfiabilityResult() == Result::UNSAT ) { + ( ( d_options[options::instFormatMode]!=INST_FORMAT_MODE_SZS && + ( res.asSatisfiabilityResult() == Result::SAT || (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) || + res.asSatisfiabilityResult() == Result::UNSAT ) ) { g = new GetInstantiationsCommand(); } else if( d_options[options::dumpUnsatCores] && res.asSatisfiabilityResult() == Result::UNSAT ) { diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index 8af0c452a..fde9c1c85 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -29,6 +29,7 @@ #include "main/portfolio.h" #include "options/options.h" #include "smt/options.h" +#include "printer/options.h" #include "cvc4autoconfig.h" @@ -371,7 +372,9 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) Command* gp = new GetProofCommand(); status = doCommandSingleton(gp); } else if( d_options[options::dumpInstantiations] && - d_result.asSatisfiabilityResult() == Result::UNSAT ) { + ( ( d_options[options::instFormatMode]!=INST_FORMAT_MODE_SZS && + ( res.asSatisfiabilityResult() == Result::SAT || (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) || + res.asSatisfiabilityResult() == Result::UNSAT ) ) { Command* gi = new GetInstantiationsCommand(); status = doCommandSingleton(gi); } else if( d_options[options::dumpUnsatCores] && diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index a7c67a5e4..17489b6ba 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -81,7 +81,7 @@ d_ee_conjectures( c ){ d_fullEffortCount = 0; d_uequalityEngine.addFunctionKind( kind::APPLY_UF ); d_uequalityEngine.addFunctionKind( kind::APPLY_CONSTRUCTOR ); - + } void ConjectureGenerator::eqNotifyNewClass( TNode t ){ @@ -214,7 +214,7 @@ bool ConjectureGenerator::isUniversalLessThan( TNode rt1, TNode rt2 ) { 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; return true; @@ -232,8 +232,8 @@ bool ConjectureGenerator::isUniversalLessThan( TNode rt1, TNode rt2 ) { } -bool ConjectureGenerator::isReportedCanon( TNode n ) { - return std::find( d_ue_canon.begin(), d_ue_canon.end(), n )==d_ue_canon.end(); +bool ConjectureGenerator::isReportedCanon( TNode n ) { + return std::find( d_ue_canon.begin(), d_ue_canon.end(), n )==d_ue_canon.end(); } void ConjectureGenerator::markReportedCanon( TNode n ) { @@ -545,7 +545,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { if( it->first.isNull() ){ Trace("sg-gen-tg-debug") << "In this order : "; for( unsigned i=0; isecond.size(); i++ ){ - Trace("sg-gen-tg-debug") << it->second[i] << " "; + Trace("sg-gen-tg-debug") << it->second[i] << " "; } Trace("sg-gen-tg-debug") << std::endl; } @@ -663,10 +663,10 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { d_rel_pattern_var_sum.clear(); d_rel_pattern_typ_index.clear(); d_rel_pattern_subs_index.clear(); - d_gen_lat_maximal.clear(); - d_gen_lat_child.clear(); - d_gen_lat_parent.clear(); - d_gen_depth.clear(); + //d_gen_lat_maximal.clear(); + //d_gen_lat_child.clear(); + //d_gen_lat_parent.clear(); + //d_gen_depth.clear(); //the following generates a set of relevant terms d_use_ccand_eqc = true; @@ -682,6 +682,8 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { } 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++ ){ @@ -693,7 +695,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { d_var_limit.clear(); d_tg_id = 0; d_tg_gdepth = 0; - d_tg_gdepth_limit = -1; + d_tg_gdepth_limit = depth; //consider all types d_tg_alloc[0].reset( this, TypeNode::null() ); while( d_tg_alloc[0].getNextTerm( this, depth ) ){ @@ -717,7 +719,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { } TypeNode tnn = nn.getType(); Trace("sg-gen-tg-debug") << "...term is " << nn << std::endl; - Assert( getUniversalRepresentative( nn )==nn ); + conj_lhs[depth].push_back( nn ); //add information about pattern Trace("sg-gen-tg-debug") << "Collect pattern information..." << std::endl; @@ -742,38 +744,6 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { Assert( d_pattern_is_normal[nn] ); Trace("sg-gen-tg-debug") << "...done collect pattern information" << std::endl; - //compute generalization relation - Trace("sg-gen-tg-debug") << "Build generalization information..." << std::endl; - std::map< TNode, bool > patProc; - int maxGenDepth = -1; - unsigned i = d_rel_patterns[tnn].size()-1; - for( int j=(int)(i-1); j>=0; j-- ){ - TNode np = d_rel_patterns[tnn][j]; - if( patProc.find( np )==patProc.end() ){ - Trace("sg-gen-tg-debug2") << "Check if generalized by " << np << "..." << std::endl; - if( isGeneralization( np, nn ) ){ - Trace("sg-rel-terms-debug") << " is generalized by : " << np << std::endl; - d_gen_lat_child[np].push_back( nn ); - d_gen_lat_parent[nn].push_back( np ); - if( d_gen_depth[np]>maxGenDepth ){ - maxGenDepth = d_gen_depth[np]; - } - //don't consider the transitive closure of generalizes - Trace("sg-gen-tg-debug2") << "Add generalizations" << std::endl; - addGeneralizationsOf( np, patProc ); - Trace("sg-gen-tg-debug2") << "Done add generalizations" << std::endl; - }else{ - Trace("sg-gen-tg-debug2") << " is not generalized by : " << np << std::endl; - } - } - } - if( d_gen_lat_parent[nn].empty() ){ - d_gen_lat_maximal[tnn].push_back( nn ); - } - d_gen_depth[nn] = maxGenDepth+1; - Trace("sg-rel-term-debug") << " -> generalization depth is " << d_gen_depth[nn] << " <> " << depth << std::endl; - Trace("sg-gen-tg-debug") << "...done build generalization information" << std::endl; - //record information about types Trace("sg-gen-tg-debug") << "Collect type information..." << std::endl; PatternTypIndex * pti = &d_rel_pattern_typ_index; @@ -834,8 +804,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { } } Trace("sg-proc") << "...done generate terms at depth " << depth << std::endl; - - + //now generate right hand sides @@ -852,11 +821,11 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { 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(); + //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 @@ -865,19 +834,17 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { Assert( d_tg_alloc.empty() ); Trace("sg-proc") << "Generate relevant RHS terms of type " << rt_types[i] << " at depth " << depth << "..." << std::endl; d_tg_id = 0; + d_tg_gdepth = 0; + d_tg_gdepth_limit = -1; d_tg_alloc[0].reset( this, rt_types[i] ); while( d_tg_alloc[0].getNextTerm( this, depth ) && totalCount<100 ){ if( d_tg_alloc[0].getDepth( this )==depth ){ Node rhs = d_tg_alloc[0].getTerm( this ); Trace("sg-rel-prop") << "Relevant RHS : " << rhs << std::endl; + conj_rhs[depth].push_back( rhs ); //register pattern Assert( rhs.getType()==rt_types[i] ); registerPattern( rhs, rt_types[i] ); - //for each maximal node of type rt_types[i] in generalization lattice - for( unsigned j=0; j=0; i-- ){ - processCandidateConjecture( d_cconj_at_depth[conj_depth][i], conj_depth ); + for( int rhs_d=depth; rhs_d>=0; rhs_d-- ){ + int lhs_d = (depth-rhs_d)+1; + for( unsigned i=0; i=0 && d_tg_gdepth>(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; return false; } - + //----optimizations if( d_tg_alloc[i-1].d_status==1 ){ }else if( d_tg_alloc[i-1].d_status==2 ){ @@ -1202,40 +1168,13 @@ bool ConjectureGenerator::isGeneralization( TNode patg, TNode pat, std::map< TNo } } -void ConjectureGenerator::addGeneralizationsOf( TNode pat, std::map< TNode, bool >& patProc ) { - patProc[pat] = true; - for( unsigned k=0; k=optFullCheckConjectures() ){ return; } - TNode lhs = d_cconj[0][cid]; - TNode rhs = d_cconj[1][cid]; - if( !considerCandidateConjecture( lhs, rhs ) ){ - //push to children of generalization lattice - for( unsigned i=0; i found witness that falsifies the conjecture." << std::endl; return false; @@ -1349,7 +1290,7 @@ bool ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) { 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; + return false; }else{ Trace("sg-cconj-debug") << "Checked if " << slhsr << " and " << srhsr << " were equal." << std::endl; } @@ -1364,7 +1305,7 @@ bool ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) { 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; @@ -1375,12 +1316,12 @@ bool ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) { exit(0); } */ - + //check if still canonical representation (should be, but for efficiency this is not guarenteed) if( getUniversalRepresentative( lhs )!=lhs || getUniversalRepresentative( rhs )!=rhs ){ Trace("sg-cconj") << " -> after processing, not canonical." << std::endl; } - + return true; } } @@ -1414,6 +1355,11 @@ bool ConjectureGenerator::notifySubstitution( TNode glhs, std::map< TNode, TNode Trace("sg-cconj-witness") << " " << it->first << " -> " << it->second << std::endl; } return false; + }else{ + d_subs_unkCount++; + if( optFilterUnknown() ){ + return false; + } } } } @@ -1592,9 +1538,16 @@ void TermGenerator::resetMatching( ConjectureGenerator * s, TNode eqc, unsigned d_match_children.clear(); d_match_children_end.clear(); d_match_mode = mode; + //if this term generalizes, it must generalize a non-ground term + if( mode<2 && s->isGroundEqc( eqc ) && d_status==5 ){ + d_match_status = -1; + } } bool TermGenerator::getNextMatch( ConjectureGenerator * s, TNode eqc, std::map< TypeNode, std::map< unsigned, TNode > >& subs, std::map< TNode, bool >& rev_subs ) { + if( d_match_status<0 ){ + return false; + } if( Trace.isOn("sg-gen-tg-match") ){ Trace("sg-gen-tg-match") << "Matching "; debugPrint( s, "sg-gen-tg-match", "sg-gen-tg-match" ); @@ -1940,12 +1893,13 @@ void TheoremIndex::debugPrint( const char * c, unsigned ind ) { 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::optFullCheckFrequency() { return 1; } -unsigned ConjectureGenerator::optFullCheckConjectures() { return 1; } +unsigned ConjectureGenerator::optFullCheckConjectures() { return options::conjectureGenPerRound(); } } diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index afdd9e018..94a13829c 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -81,11 +81,9 @@ public: int d_status_child_num; //children (pointers to TermGenerators) std::vector< unsigned > d_children; - //possible eqc for this term - //std::vector< TNode > d_eqc; //match status - unsigned d_match_status; + int d_match_status; int d_match_status_child_num; //match mode //1 : different variables must have different matches @@ -213,14 +211,14 @@ private: void setUniversalRelevant( TNode n ); /** ordering for universal terms */ bool isUniversalLessThan( TNode rt1, TNode rt2 ); - + /** the nodes we have reported as canonical representative */ std::vector< TNode > d_ue_canon; /** is reported canon */ bool isReportedCanon( TNode n ); /** mark that term has been reported as canonical rep */ void markReportedCanon( TNode n ); - + private: //information regarding the conjectures /** list of all conjectures */ std::vector< Node > d_conjectures; @@ -297,7 +295,6 @@ public: //environment for term enumeration std::map< unsigned, TermGenerator > d_tg_alloc; unsigned d_tg_gdepth; int d_tg_gdepth_limit; - //std::vector< std::vector< unsigned > > d_var_eq_tg; //access functions unsigned getNumTgVars( TypeNode tn ); bool allowVar( TypeNode tn ); @@ -308,37 +305,17 @@ public: //environment for term enumeration bool considerCurrentTerm(); bool considerTermCanon( unsigned tg_id ); void changeContext( bool add ); -public: //for generalization lattice - //id of maximal nodes - std::map< TypeNode, std::vector< TNode > > d_gen_lat_maximal; - //generalization lattice - std::map< TNode, std::vector< TNode > > d_gen_lat_child; - std::map< TNode, std::vector< TNode > > d_gen_lat_parent; - //generalization depth - std::map< TNode, int > d_gen_depth; +public: //for generalization //generalizations bool isGeneralization( TNode patg, TNode pat ) { std::map< TNode, TNode > subs; return isGeneralization( patg, pat, subs ); } bool isGeneralization( TNode patg, TNode pat, std::map< TNode, TNode >& subs ); - void addGeneralizationsOf( TNode pat, std::map< TNode, bool >& patProc ); - - //from generalization depth to relevant patterns - std::map< TypeNode, std::map< unsigned, std::vector< TNode > > > d_rel_patterns_at_depth; - - + public: //for property enumeration - //conjectures to process at a particular depth - std::map< unsigned, std::vector< unsigned > > d_cconj_at_depth; - //RHS, LHS - std::vector< TNode > d_cconj[2]; - // RHS paired - std::map< TNode, std::vector< TNode > > d_cconj_rhs_paired; - //add candidate conjecture - void addCandidateConjecture( TNode lhs, TNode rhs, unsigned depth ); - //process candidate conjecture at depth - void processCandidateConjecture( unsigned cid, unsigned depth ); + //process this candidate conjecture + void processCandidateConjecture( TNode lhs, TNode rhs, unsigned lhs_depth, unsigned rhs_depth ); //whether it should be considered bool considerCandidateConjecture( TNode lhs, TNode rhs ); //notified of a substitution @@ -349,6 +326,8 @@ public: //for property enumeration std::vector< TNode > d_subs_confirmWitnessRange; //individual witnesses (for domain) std::map< TNode, std::vector< TNode > > d_subs_confirmWitnessDomain; + //number of ground substitutions whose equality is unknown + unsigned d_subs_unkCount; public: //for ground equivalence classes eq::EqualityEngine * getEqualityEngine(); bool areDisequal( TNode n1, TNode n2 ); @@ -386,6 +365,7 @@ public: private: bool optReqDistinctVarPatterns(); bool optFilterFalsification(); + bool optFilterUnknown(); bool optFilterConfirmation(); bool optFilterConfirmationDomain(); bool optFilterConfirmationOnlyGround(); diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 2b4ce9aef..aa68aefcc 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -158,5 +158,8 @@ option intWfInduction --int-wf-ind bool :read-write :default false apply strengthening for integers based on well-founded induction 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 endmodule -- 2.30.2