From b02943d28e641ff894c50bee810309b783731555 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 25 May 2022 14:43:04 -0500 Subject: [PATCH] Eliminate more static options accesses (#8802) A block of code changed indentation in the induction solver, this is cleaned to conform to guidelines. --- src/options/quantifiers_options.toml | 24 -- src/theory/difficulty_manager.cpp | 18 +- src/theory/difficulty_manager.h | 5 +- .../quantifiers/conjecture_generator.cpp | 205 ++++++++++-------- src/theory/relevance_manager.cpp | 2 +- .../sygus/issue4022-conjecture-gen.smt2 | 3 - 6 files changed, 128 insertions(+), 129 deletions(-) diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 2d6d74bb4..a624aae92 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -790,30 +790,6 @@ name = "Quantifiers" default = "1" help = "number of conjectures to generate per instantiation round" -[[option]] - name = "conjectureFilterActiveTerms" - category = "expert" - long = "conjecture-filter-active-terms" - type = "bool" - default = "true" - help = "filter based on active terms" - -[[option]] - name = "conjectureFilterCanonical" - category = "expert" - long = "conjecture-filter-canonical" - type = "bool" - default = "true" - help = "filter based on canonicity" - -[[option]] - name = "conjectureFilterModel" - category = "expert" - long = "conjecture-filter-model" - type = "bool" - default = "true" - help = "filter based on model" - [[option]] name = "conjectureGenGtEnum" category = "expert" diff --git a/src/theory/difficulty_manager.cpp b/src/theory/difficulty_manager.cpp index 797ebab79..0b74cb081 100644 --- a/src/theory/difficulty_manager.cpp +++ b/src/theory/difficulty_manager.cpp @@ -26,10 +26,14 @@ using namespace cvc5::internal::kind; namespace cvc5::internal { namespace theory { -DifficultyManager::DifficultyManager(RelevanceManager* rlv, - context::Context* c, +DifficultyManager::DifficultyManager(Env& env, + RelevanceManager* rlv, Valuation val) - : d_rlv(rlv), d_input(c), d_val(val), d_dfmap(c) + : EnvObj(env), + d_rlv(rlv), + d_input(userContext()), + d_val(val), + d_dfmap(userContext()) { } @@ -55,11 +59,13 @@ void DifficultyManager::notifyLemma(Node n, bool inFullEffortCheck) { // compute if we should consider the lemma bool considerLemma = false; - if (options::difficultyMode() == options::DifficultyMode::LEMMA_LITERAL_ALL) + if (options().smt.difficultyMode + == options::DifficultyMode::LEMMA_LITERAL_ALL) { considerLemma = true; } - else if (options::difficultyMode() == options::DifficultyMode::LEMMA_LITERAL) + else if (options().smt.difficultyMode + == options::DifficultyMode::LEMMA_LITERAL) { considerLemma = inFullEffortCheck; } @@ -103,7 +109,7 @@ void DifficultyManager::notifyLemma(Node n, bool inFullEffortCheck) void DifficultyManager::notifyCandidateModel(TheoryModel* m) { - if (options::difficultyMode() != options::DifficultyMode::MODEL_CHECK) + if (options().smt.difficultyMode != options::DifficultyMode::MODEL_CHECK) { return; } diff --git a/src/theory/difficulty_manager.h b/src/theory/difficulty_manager.h index b30fbd22e..f0c694c66 100644 --- a/src/theory/difficulty_manager.h +++ b/src/theory/difficulty_manager.h @@ -21,6 +21,7 @@ #include "context/cdhashmap.h" #include "context/cdhashset.h" #include "expr/node.h" +#include "smt/env_obj.h" #include "theory/valuation.h" namespace cvc5::internal { @@ -33,13 +34,13 @@ class RelevanceManager; * Difficulty manager, which tracks an estimate of the difficulty of each * preprocessed assertion during solving. */ -class DifficultyManager +class DifficultyManager : protected EnvObj { typedef context::CDHashSet NodeSet; typedef context::CDHashMap NodeUIntMap; public: - DifficultyManager(RelevanceManager* rlv, context::Context* c, Valuation val); + DifficultyManager(Env& env, RelevanceManager* rlv, Valuation val); /** Notify input assertions */ void notifyInputAssertions(const std::vector& assertions); /** diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index f403dc328..e8515d370 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -675,8 +675,7 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e) while( d_tge.getNextTerm() ){ //construct term Node nn = d_tge.getTerm(); - if (!options().quantifiers.conjectureFilterCanonical - || considerTermCanon(nn, true)) + if (considerTermCanon(nn, true)) { rel_term_count++; Trace("sg-rel-term") << "*** Relevant term : "; @@ -916,9 +915,8 @@ unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, in //we have determined a relevant subgoal Node lhs = d_waiting_conjectures_lhs[i]; Node rhs = d_waiting_conjectures_rhs[i]; - if (options().quantifiers.conjectureFilterCanonical - && (getUniversalRepresentative(lhs) != lhs - || getUniversalRepresentative(rhs) != rhs)) + if (getUniversalRepresentative(lhs) != lhs + || getUniversalRepresentative(rhs) != rhs) { //skip } @@ -1282,95 +1280,114 @@ int ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) { if( lhs==rhs ){ Trace("sg-cconj-debug") << " -> trivial." << std::endl; return -1; - }else{ - if( lhs.getKind()==APPLY_CONSTRUCTOR && rhs.getKind()==APPLY_CONSTRUCTOR ){ - Trace("sg-cconj-debug") << " -> irrelevant by syntactic analysis." << std::endl; + } + if (lhs.getKind() == APPLY_CONSTRUCTOR && rhs.getKind() == APPLY_CONSTRUCTOR) + { + Trace("sg-cconj-debug") + << " -> irrelevant by syntactic analysis." << std::endl; + return -1; + } + // variables of LHS must subsume variables of RHS + for (std::pair& p : d_pattern_var_id[rhs]) + { + std::map::iterator itl = + d_pattern_var_id[lhs].find(p.first); + if (itl == d_pattern_var_id[lhs].end()) + { + Trace("sg-cconj-debug") + << " -> has no variables of sort " << p.first << "." << std::endl; return -1; } - //variables of LHS must subsume variables of RHS - for( std::map< TypeNode, unsigned >::iterator it = d_pattern_var_id[rhs].begin(); it != d_pattern_var_id[rhs].end(); ++it ){ - std::map< TypeNode, unsigned >::iterator itl = d_pattern_var_id[lhs].find( it->first ); - if( itl!=d_pattern_var_id[lhs].end() ){ - if( itl->secondsecond ){ - Trace("sg-cconj-debug") << " -> variables of sort " << it->first << " are not subsumed." << std::endl; - return -1; - }else{ - Trace("sg-cconj-debug2") << " variables of sort " << it->first << " are : " << itl->second << " vs " << it->second << std::endl; - } - }else{ - Trace("sg-cconj-debug") << " -> has no variables of sort " << it->first << "." << std::endl; - return -1; - } + if (itl->second < p.second) + { + Trace("sg-cconj-debug") << " -> variables of sort " << p.first + << " are not subsumed." << std::endl; + return -1; } + Trace("sg-cconj-debug2") + << " variables of sort " << p.first << " are : " << itl->second + << " vs " << p.second << std::endl; + } - //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 -1; - } + // currently active conjecture? + std::map >::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 -1; } - //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 -1; - } + } + // current a waiting conjecture? + std::map >::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 -1; } - // check if canonical representation (should be, but for efficiency this is - // not guarenteed) if( options().quantifiers.conjectureFilterCanonical && ( - // getUniversalRepresentative( lhs )!=lhs || getUniversalRepresentative( rhs - // )!=rhs ) ){ - // Trace("sg-cconj") << " -> after processing, not canonical." << - // std::endl; return -1; - //} - - int score; - bool scoreSet = false; + } - Trace("sg-cconj") << "Consider possible candidate conjecture : " << lhs << " == " << rhs << "?" << std::endl; - //find witness for counterexample, if possible - if (options().quantifiers.conjectureFilterModel) + size_t score; + bool scoreSet = false; + + Trace("sg-cconj") << "Consider possible candidate conjecture : " << lhs + << " == " << rhs << "?" << std::endl; + // find witness for counterexample, if possible + 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 subs; + d_subs_confirmCount = 0; + d_subs_confirmWitnessRange.clear(); + d_subs_confirmWitnessDomain.clear(); + d_subs_unkCount = 0; + if (!d_rel_pattern_subs_index[lhs].notifySubstitutions( + this, subs, rhs, d_rel_pattern_var_sum[lhs])) + { + Trace("sg-cconj") << " -> found witness that falsifies the conjecture." + << std::endl; + return -1; + } + // score is the minimum number of distinct substitutions for a variable + for (std::pair >& w : + d_subs_confirmWitnessDomain) + { + size_t num = w.second.size(); + if (!scoreSet || num < score) { - 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; - d_subs_confirmCount = 0; - d_subs_confirmWitnessRange.clear(); - d_subs_confirmWitnessDomain.clear(); - d_subs_unkCount = 0; - if( !d_rel_pattern_subs_index[lhs].notifySubstitutions( this, subs, rhs, d_rel_pattern_var_sum[lhs] ) ){ - Trace("sg-cconj") << " -> found witness that falsifies the conjecture." << std::endl; - return -1; - } - //score is the minimum number of distinct substitutions for a variable - for( std::map< TNode, std::vector< TNode > >::iterator it = d_subs_confirmWitnessDomain.begin(); it != d_subs_confirmWitnessDomain.end(); ++it ){ - int num = (int)it->second.size(); - if( !scoreSet || num >::iterator it = d_subs_confirmWitnessDomain.begin(); it != d_subs_confirmWitnessDomain.end(); ++it ){ - Trace("sg-cconj") << " #witnesses for " << it->first << " : " << it->second.size() << std::endl; - } + score = num; + scoreSet = true; } - else + } + if (!scoreSet) + { + score = 0; + } + if (TraceIsOn("sg-cconj")) + { + Trace("sg-cconj") << " confirmed = " << d_subs_confirmCount + << ", #witnesses range = " + << d_subs_confirmWitnessRange.size() << "." << std::endl; + for (std::pair >& w : + d_subs_confirmWitnessDomain) { - score = 1; + Trace("sg-cconj") << " #witnesses for " << w.first << " : " + << w.second.size() << std::endl; } - Trace("sg-cconj") << " -> SUCCESS." << std::endl; Trace("sg-cconj") << " score : " << score << std::endl; - - return score; } + return static_cast(score); } bool ConjectureGenerator::notifySubstitution( TNode glhs, std::map< TNode, TNode >& subs, TNode rhs ) { @@ -2049,13 +2066,17 @@ bool TermGenEnv::considerCurrentTerm() { } Trace("sg-gen-tg-debug") << std::endl; } - if( options::conjectureFilterActiveTerms() && d_ccand_eqc[0][i].empty() ){ + // filter based active terms + if (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( options::conjectureFilterModel() && d_ccand_eqc[1][i].empty() ){ + // filter based on model + if (d_ccand_eqc[1][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 ground EQC matches it." << std::endl; @@ -2087,17 +2108,15 @@ void TermGenEnv::changeContext( bool add ) { bool TermGenEnv::considerCurrentTermCanon( unsigned tg_id ){ Assert(tg_id < d_tg_alloc.size()); - if( options::conjectureFilterCanonical() ){ - //check based on a canonicity of the term (if there is one) - Trace("sg-gen-tg-debug") << "Consider term canon "; - d_tg_alloc[0].debugPrint( this, "sg-gen-tg-debug", "sg-gen-tg-debug" ); - Trace("sg-gen-tg-debug") << ", tg is [" << tg_id << "]..." << std::endl; - - Node ln = d_tg_alloc[tg_id].getTerm( this ); - Trace("sg-gen-tg-debug") << "Term is " << ln << std::endl; - return d_cg->considerTermCanon( ln, d_gen_relevant_terms ); - } - return true; + // filter based on canonical + // check based on a canonicity of the term (if there is one) + Trace("sg-gen-tg-debug") << "Consider term canon "; + d_tg_alloc[0].debugPrint(this, "sg-gen-tg-debug", "sg-gen-tg-debug"); + Trace("sg-gen-tg-debug") << ", tg is [" << tg_id << "]..." << std::endl; + + Node ln = d_tg_alloc[tg_id].getTerm(this); + Trace("sg-gen-tg-debug") << "Term is " << ln << std::endl; + return d_cg->considerTermCanon(ln, d_gen_relevant_terms); } bool TermGenEnv::isRelevantFunc( Node f ) { diff --git a/src/theory/relevance_manager.cpp b/src/theory/relevance_manager.cpp index b9bf73da4..5a497c485 100644 --- a/src/theory/relevance_manager.cpp +++ b/src/theory/relevance_manager.cpp @@ -44,7 +44,7 @@ RelevanceManager::RelevanceManager(Env& env, Valuation val) { if (options().smt.produceDifficulty) { - d_dman = std::make_unique(this, userContext(), val); + d_dman = std::make_unique(env, this, val); d_trackRSetExp = true; // we cannot miniscope AND at the top level, since we need to // preserve the exact form of preprocessed assertions so the dependencies diff --git a/test/regress/cli/regress2/sygus/issue4022-conjecture-gen.smt2 b/test/regress/cli/regress2/sygus/issue4022-conjecture-gen.smt2 index 37eccc67f..b87cad954 100644 --- a/test/regress/cli/regress2/sygus/issue4022-conjecture-gen.smt2 +++ b/test/regress/cli/regress2/sygus/issue4022-conjecture-gen.smt2 @@ -1,10 +1,7 @@ ; COMMAND-LINE: ; EXPECT: sat (set-logic ALL) -(set-option :conjecture-filter-model true) (set-option :conjecture-gen true) -(set-option :conjecture-filter-canonical false) -(set-option :conjecture-filter-active-terms false) (set-option :quant-ind true) (set-option :sygus-inference true) (set-info :status sat) -- 2.30.2