From a4a943134f888a514f19adaffe2f6743a16a25a6 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 29 Sep 2014 21:39:34 +0200 Subject: [PATCH] Add option for aggressive model filtering in conjecture generator (enumerate ground terms). --- .../quantifiers/conjecture_generator.cpp | 190 +++++++++++++++--- src/theory/quantifiers/conjecture_generator.h | 22 +- src/theory/quantifiers/options | 2 + 3 files changed, 178 insertions(+), 36 deletions(-) diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index a2e3d4ce3..799cce9ed 100755 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -32,8 +32,8 @@ struct sortConjectureScore { std::vector< int > d_scores; bool operator() (unsigned i, unsigned j) { return d_scores[i]>d_scores[j]; } }; - - + + void OpArgIndex::addTerm( ConjectureGenerator * s, TNode n, unsigned index ){ if( index==n.getNumChildren() ){ Assert( n.hasOperator() ); @@ -264,7 +264,7 @@ TNode ConjectureGenerator::getUniversalRepresentative( TNode n, bool add ) { } } } - + if( d_uequalityEngine.hasTerm( n ) ){ Node r = d_uequalityEngine.getRepresentative( n ); EqcInfo * ei = getOrMakeEqcInfo( r ); @@ -381,6 +381,25 @@ bool ConjectureGenerator::needsCheck( Theory::Effort e ) { return e==Theory::EFFORT_FULL; } +bool ConjectureGenerator::hasEnumeratedUf( Node n ) { + if( options::conjectureGenGtEnum()>0 ){ + std::map< Node, bool >::iterator it = d_uf_enum.find( n.getOperator() ); + if( it==d_uf_enum.end() ){ + d_uf_enum[n.getOperator()] = true; + std::vector< Node > lem; + getEnumeratePredUfTerm( n, options::conjectureGenGtEnum(), lem ); + if( !lem.empty() ){ + for( unsigned j=0; jaddLemma( lem[j], false ); + d_hasAddedLemma = true; + } + return false; + } + } + } + return true; +} + void ConjectureGenerator::reset_round( Theory::Effort e ) { } @@ -389,11 +408,12 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){ d_fullEffortCount++; if( d_fullEffortCount%optFullCheckFrequency()==0 ){ + d_hasAddedLemma = false; d_tge.d_cg = this; double clSet = 0; if( Trace.isOn("sg-engine") ){ clSet = double(clock())/double(CLOCKS_PER_SEC); - Trace("sg-engine") << "---Instantiation Engine Round, effort = " << e << "---" << std::endl; + Trace("sg-engine") << "---Conjecture Engine Round, effort = " << e << "---" << std::endl; } eq::EqualityEngine * ee = getEqualityEngine(); @@ -529,8 +549,11 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { Trace("sg-proc") << "Collect signature information..." << std::endl; d_tge.collectSignatureInformation(); + if( d_hasAddedLemma ){ + Trace("sg-proc") << "...added enumeration lemmas." << std::endl; + } Trace("sg-proc") << "...done collect signature information" << std::endl; - + Trace("sg-proc") << "Build theorem index..." << std::endl; @@ -631,7 +654,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { d_thm_index.debugPrint( "thm-db" ); Trace("thm-db") << std::endl; Trace("sg-proc") << "...done build theorem index" << std::endl; - + //clear patterns d_patterns.clear(); @@ -759,12 +782,12 @@ 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 " << depth << " : " << rel_term_count << std::endl; //Trace("conjecture-count") << "Total LHS of depth " << depth << " : " << conj_lhs[depth].size() << std::endl; - + /* test... for( unsigned i=0; i::iterator it = d_typ_pred.find( tn ); + if( it==d_typ_pred.end() ){ + TypeNode op_tn = NodeManager::currentNM()->mkFunctionType( tn, NodeManager::currentNM()->booleanType() ); + Node op = NodeManager::currentNM()->mkSkolem( "PE", op_tn, "was created by conjecture ground term enumerator." ); + d_typ_pred[tn] = op; + return op; + }else{ + return it->second; + } +} + +void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< Node >& terms ) { + if( n.getNumChildren()>0 ){ + std::vector< int > vec; + for( unsigned i=0; i children; + children.push_back( n.getOperator() ); + for( unsigned i=0; i<(vec.size()-1); i++ ){ + Node nn = getEnumerateTerm( n[i].getType(), vec[i] ); + Assert( !nn.isNull() ); + Assert( nn.getType()==n[i].getType() ); + children.push_back( nn ); + } + children.push_back( lc ); + Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children ); + Trace("sg-gt-enum") << "Ground term enumerate : " << n << std::endl; + terms.push_back( n ); + } + vec.pop_back(); + index = 0; + } + }else{ + if( terms.size()>last_size ){ + last_size = terms.size(); + size_limit++; + for( unsigned i=0; i& terms ) { + std::vector< Node > uf_terms; + getEnumerateUfTerm( n, num, uf_terms ); + Node p = getPredicateForType( n.getType() ); + for( unsigned i=0; imkNode( APPLY_UF, p, uf_terms[i] ) ); + } +} + void ConjectureGenerator::processCandidateConjecture( TNode lhs, TNode rhs, unsigned lhs_depth, unsigned rhs_depth ) { - int score = considerCandidateConjecture( lhs, rhs ); + int score = considerCandidateConjecture( lhs, rhs ); if( score>0 ){ Trace("sg-conjecture") << "* Candidate conjecture : " << lhs << " == " << rhs << std::endl; Trace("sg-conjecture-debug") << " LHS, RHS generalization depth : " << lhs_depth << ", " << rhs_depth << std::endl; @@ -1132,7 +1252,7 @@ void ConjectureGenerator::processCandidateConjecture( TNode lhs, TNode rhs, unsi int ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) { Assert( lhs.getType()==rhs.getType() ); - + Trace("sg-cconj-debug") << "Consider candidate conjecture : " << lhs << " == " << rhs << "?" << std::endl; if( lhs==rhs ){ Trace("sg-cconj-debug") << " -> trivial." << std::endl; @@ -1179,7 +1299,7 @@ int ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) { // Trace("sg-cconj") << " -> after processing, not canonical." << std::endl; // return -1; //} - + int score; bool scoreSet = false; @@ -1218,7 +1338,7 @@ int ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) { Trace("sg-cconj") << " -> SUCCESS." << std::endl; Trace("sg-cconj") << " score : " << score << std::endl; - + return score; } } @@ -1684,15 +1804,24 @@ void TermGenEnv::collectSignatureInformation() { if( !getTermDatabase()->d_op_map[it->first].empty() ){ Node nn = getTermDatabase()->d_op_map[it->first][0]; if( d_cg->isHandledTerm( nn ) && nn.getKind()!=APPLY_SELECTOR_TOTAL && !nn.getType().isBoolean() ){ - d_funcs.push_back( it->first ); - for( unsigned i=0; ifirst].push_back( nn[i].getType() ); + bool do_enum = true; + //check if we have enumerated ground terms + if( nn.getKind()==APPLY_UF ){ + if( !d_cg->hasEnumeratedUf( nn ) ){ + do_enum = false; + } + } + if( do_enum ){ + d_funcs.push_back( it->first ); + for( unsigned i=0; ifirst].push_back( nn[i].getType() ); + } + d_func_kind[it->first] = nn.getKind(); + d_typ_tg_funcs[tnull].push_back( it->first ); + d_typ_tg_funcs[nn.getType()].push_back( it->first ); + Trace("sg-rel-sig") << "Will enumerate function applications of : " << it->first << ", #args = " << d_func_args[it->first].size() << ", kind = " << nn.getKind() << std::endl; + getTermDatabase()->computeUfEqcTerms( it->first ); } - d_func_kind[it->first] = nn.getKind(); - d_typ_tg_funcs[tnull].push_back( it->first ); - d_typ_tg_funcs[nn.getType()].push_back( it->first ); - Trace("sg-rel-sig") << "Will enumerate function applications of : " << it->first << ", #args = " << d_func_args[it->first].size() << ", kind = " << nn.getKind() << std::endl; - getTermDatabase()->computeUfEqcTerms( it->first ); } } } @@ -1712,18 +1841,18 @@ void TermGenEnv::collectSignatureInformation() { void TermGenEnv::reset( unsigned depth, bool genRelevant, TypeNode tn ) { Assert( d_tg_alloc.empty() ); d_tg_alloc.clear(); - + if( genRelevant ){ for( unsigned i=0; i<2; i++ ){ d_ccand_eqc[i].clear(); d_ccand_eqc[i].push_back( d_relevant_eqc[i] ); } } - + d_tg_id = 0; d_tg_gdepth = 0; d_tg_gdepth_limit = depth; - d_gen_relevant_terms = genRelevant; + d_gen_relevant_terms = genRelevant; d_tg_alloc[0].reset( this, tn ); } @@ -1741,8 +1870,8 @@ bool TermGenEnv::getNextTerm() { } //reset matching -void TermGenEnv::resetMatching( TNode eqc, unsigned mode ) { - d_tg_alloc[0].resetMatching( this, eqc, mode ); +void TermGenEnv::resetMatching( TNode eqc, unsigned mode ) { + d_tg_alloc[0].resetMatching( this, eqc, mode ); } //get next match @@ -1751,8 +1880,8 @@ bool TermGenEnv::getNextMatch( TNode eqc, std::map< TypeNode, std::map< unsigned } //get term -Node TermGenEnv::getTerm() { - return d_tg_alloc[0].getTerm( this ); +Node TermGenEnv::getTerm() { + return d_tg_alloc[0].getTerm( this ); } void TermGenEnv::debugPrint( const char * c, const char * cd ) { @@ -1931,7 +2060,6 @@ bool TermGenEnv::isGroundTerm( TNode n ){ } - void SubstitutionIndex::addSubstitution( TNode eqc, std::vector< TNode >& vars, std::vector< TNode >& terms, unsigned i ) { if( i==vars.size() ){ d_var = eqc; @@ -2084,5 +2212,3 @@ unsigned ConjectureGenerator::optFullCheckFrequency() { return 1; } bool ConjectureGenerator::optStatsOnly() { return false; } } - - diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index eb7f4b2aa..23e2b88ba 100755 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -129,7 +129,7 @@ public: Node getTerm(); //debug print void debugPrint( const char * c, const char * cd ); - + //conjecture generation ConjectureGenerator * d_cg; //the current number of enumerated variables per type @@ -149,14 +149,14 @@ public: std::map< unsigned, TermGenerator > d_tg_alloc; unsigned d_tg_gdepth; int d_tg_gdepth_limit; - + //all functions std::vector< TNode > d_funcs; //function to kind map std::map< TNode, Kind > d_func_kind; //type of each argument of the function std::map< TNode, std::vector< TypeNode > > d_func_args; - + //access functions unsigned getNumTgVars( TypeNode tn ); bool allowVar( TypeNode tn ); @@ -364,6 +364,16 @@ private: std::vector< TypeEnumerator > d_typ_enum; //get nth term for type Node getEnumerateTerm( TypeNode tn, unsigned index ); + //predicate for type + std::map< TypeNode, Node > d_typ_pred; + //get predicate for type + Node getPredicateForType( TypeNode tn ); + // + void getEnumerateUfTerm( Node n, unsigned num, std::vector< Node >& terms ); + // + void getEnumeratePredUfTerm( Node n, unsigned num, std::vector< Node >& terms ); + // uf operators enumerated + std::map< Node, bool > d_uf_enum; public: //for property enumeration //process this candidate conjecture void processCandidateConjecture( TNode lhs, TNode rhs, unsigned lhs_depth, unsigned rhs_depth ); @@ -396,8 +406,12 @@ private: //information about ground equivalence classes Node getGroundEqc( TNode r ); bool isGroundEqc( TNode r ); bool isGroundTerm( TNode n ); + //has enumerated UF + bool hasEnumeratedUf( Node n ); // count of full effort checks unsigned d_fullEffortCount; + // has added lemma + bool d_hasAddedLemma; //flush the waiting conjectures unsigned flushWaitingConjectures( unsigned& addedLemmas, int ldepth, int rdepth ); public: @@ -420,7 +434,7 @@ private: int optFilterScoreThreshold(); unsigned optFullCheckFrequency(); unsigned optFullCheckConjectures(); - + bool optStatsOnly(); }; diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index efe1b1098..16df9d9a9 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -169,4 +169,6 @@ option conjectureFilterCanonical --conjecture-filter-canonical bool :read-write filter based on canonicity option conjectureFilterModel --conjecture-filter-model bool :read-write :default true filter based on model +option conjectureGenGtEnum --conjecture-gen-gt-enum=N int :default 0 + number of ground terms to generate for model filtering endmodule -- 2.30.2