From 9c02423e90cf9cb8509d4ca6565acba06e6f9b2d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 22 Aug 2018 17:40:22 -0500 Subject: [PATCH] More unused code elimination (#2358) --- src/options/uf_options.toml | 9 -- src/theory/quantifiers/inst_match.cpp | 4 - src/theory/quantifiers/inst_match.h | 2 - src/theory/quantifiers/quant_relevance.cpp | 42 ------ src/theory/quantifiers/quant_relevance.h | 11 +- src/theory/quantifiers/sygus/sygus_unif.cpp | 21 --- src/theory/quantifiers/sygus/sygus_unif.h | 2 +- src/theory/quantifiers_engine.cpp | 17 +-- src/theory/uf/theory_uf_strong_solver.cpp | 148 ++------------------ src/theory/uf/theory_uf_strong_solver.h | 28 ---- 10 files changed, 11 insertions(+), 273 deletions(-) diff --git a/src/options/uf_options.toml b/src/options/uf_options.toml index 73a2be9ff..e0c34127a 100644 --- a/src/options/uf_options.toml +++ b/src/options/uf_options.toml @@ -76,15 +76,6 @@ header = "options/uf_options.h" read_only = true help = "mode of operation for uf strong solver." -[[option]] - name = "ufssCliqueSplits" - category = "regular" - long = "uf-ss-clique-splits" - type = "bool" - default = "false" - read_only = true - help = "use cliques instead of splitting on demand to shrink model" - [[option]] name = "ufssFairness" category = "regular" diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 091c3b673..a16e03420 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -101,10 +101,6 @@ void InstMatch::clear() { } Node InstMatch::get(int i) const { return d_vals[i]; } -void InstMatch::getInst(std::vector& inst) const -{ - inst.insert(inst.end(), d_vals.begin(), d_vals.end()); -} void InstMatch::setValue( int i, TNode n ) { d_vals[i] = n; diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index 86138feb3..5695d1294 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -80,8 +80,6 @@ public: } /** get the i^th term in the instantiation */ Node get(int i) const; - /** append the terms of this instantiation to inst */ - void getInst(std::vector& inst) const; /** set/overwrites the i^th field in the instantiation with n */ void setValue( int i, TNode n ); /** set the i^th term in the instantiation to n diff --git a/src/theory/quantifiers/quant_relevance.cpp b/src/theory/quantifiers/quant_relevance.cpp index b9e4d0650..a05388d17 100644 --- a/src/theory/quantifiers/quant_relevance.cpp +++ b/src/theory/quantifiers/quant_relevance.cpp @@ -28,21 +28,6 @@ void QuantRelevance::registerQuantifier(Node f) std::vector syms; computeSymbols(f[1], syms); d_syms[f].insert(d_syms[f].begin(), syms.begin(), syms.end()); - // set initial relevance - int minRelevance = -1; - for (int i = 0; i < (int)syms.size(); i++) - { - d_syms_quants[syms[i]].push_back(f); - int r = getRelevance(syms[i]); - if (r != -1 && (minRelevance == -1 || r < minRelevance)) - { - minRelevance = r; - } - } - if (minRelevance != -1) - { - setRelevance(f, minRelevance + 1); - } } /** compute symbols */ @@ -65,33 +50,6 @@ void QuantRelevance::computeSymbols(Node n, std::vector& syms) } } -/** set relevance */ -void QuantRelevance::setRelevance(Node s, int r) -{ - if (d_computeRel) - { - int rOld = getRelevance(s); - if (rOld == -1 || r < rOld) - { - d_relevance[s] = r; - if (s.getKind() == FORALL) - { - for (int i = 0; i < (int)d_syms[s].size(); i++) - { - setRelevance(d_syms[s][i], r); - } - } - else - { - for (int i = 0; i < (int)d_syms_quants[s].size(); i++) - { - setRelevance(d_syms_quants[s][i], r + 1); - } - } - } - } -} - } /* CVC4::theory::quantifiers namespace */ } /* CVC4::theory namespace */ } /* CVC4 namespace */ diff --git a/src/theory/quantifiers/quant_relevance.h b/src/theory/quantifiers/quant_relevance.h index 75ae32318..21017e783 100644 --- a/src/theory/quantifiers/quant_relevance.h +++ b/src/theory/quantifiers/quant_relevance.h @@ -39,7 +39,7 @@ class QuantRelevance : public QuantifiersUtil * if this is false, then all calls to getRelevance * return -1. */ - QuantRelevance(bool cr) : d_computeRel(cr) {} + QuantRelevance() {} ~QuantRelevance() {} /** reset */ bool reset(Theory::Effort e) override { return true; } @@ -47,13 +47,6 @@ class QuantRelevance : public QuantifiersUtil void registerQuantifier(Node q) override; /** identify */ std::string identify() const override { return "QuantRelevance"; } - /** set relevance of symbol s to r */ - void setRelevance(Node s, int r); - /** get relevance of symbol s */ - int getRelevance(Node s) - { - return d_relevance.find(s) == d_relevance.end() ? -1 : d_relevance[s]; - } /** get number of quantifiers for symbol s */ unsigned getNumQuantifiersForSymbol(Node s) { @@ -61,8 +54,6 @@ class QuantRelevance : public QuantifiersUtil } private: - /** for computing relevance */ - bool d_computeRel; /** map from quantifiers to symbols they contain */ std::map > d_syms; /** map from symbols to quantifiers */ diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp index d0f156811..d1217d01d 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif.cpp @@ -42,27 +42,6 @@ void SygusUnif::initializeCandidate( d_strategy[f].initialize(qe, f, enums); } -bool SygusUnif::constructSolution(std::vector& sols, - std::vector& lemmas) -{ - // initialize a call to construct solution - initializeConstructSol(); - for (const Node& f : d_candidates) - { - // initialize a call to construct solution for function f - initializeConstructSolFor(f); - // call the virtual construct solution method - Node e = d_strategy[f].getRootEnumerator(); - Node sol = constructSol(f, e, role_equal, 1, lemmas); - if (sol.isNull()) - { - return false; - } - sols.push_back(sol); - } - return true; -} - Node SygusUnif::constructBestSolvedTerm(const std::vector& solved) { Assert(!solved.empty()); diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h index dd6922351..614a29d1c 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.h +++ b/src/theory/quantifiers/sygus/sygus_unif.h @@ -85,7 +85,7 @@ class SygusUnif * channel by the caller. */ virtual bool constructSolution(std::vector& sols, - std::vector& lemmas); + std::vector& lemmas) = 0; protected: /** reference to quantifier engine */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 8c43e98ff..a5cd95d29 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -135,7 +135,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl; if( options::relevantTriggers() ){ - d_quant_rel = new quantifiers::QuantRelevance(false); + d_quant_rel = new quantifiers::QuantRelevance; d_util.push_back(d_quant_rel); }else{ d_quant_rel = NULL; @@ -563,9 +563,6 @@ void QuantifiersEngine::check( Theory::Effort e ){ } if( e==Theory::EFFORT_LAST_CALL ){ - //if effort is last call, try to minimize model first - //uf::StrongSolverTheoryUF * ufss = ((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver(); - //if( ufss && !ufss->minimize() ){ return; } ++(d_statistics.d_instantiation_rounds_lc); }else if( e==Theory::EFFORT_FULL ){ ++(d_statistics.d_instantiation_rounds); @@ -908,18 +905,6 @@ void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool within { d_sygus_tdb->getEvalUnfold()->registerEvalTerm(n); } - - // added contains also the Node that just have been asserted in this - // branch - if (d_quant_rel) - { - for (std::set::iterator i = added.begin(), end = added.end(); - i != end; - i++) - { - d_quant_rel->setRelevance( i->getOperator(), 0 ); - } - } } } } diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 65f7238c9..4efa6c2ce 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -23,7 +23,6 @@ #include "theory/theory_model.h" //#define ONE_SPLIT_REGION -//#define DISABLE_QUICK_CLIQUE_CHECKS //#define COMBINE_REGIONS_SMALL_INTO_LARGE //#define LAZY_REL_EQC @@ -379,21 +378,6 @@ bool Region::check( Theory::Effort level, int cardinality, return false; } -bool Region::getCandidateClique( int cardinality, std::vector< Node >& clique ) -{ - if( d_testCliqueSize>=unsigned(cardinality+1) ){ - //test clique is a clique - for( NodeBoolMap::iterator it = d_testClique.begin(); - it != d_testClique.end(); ++it ){ - if( (*it).second ){ - clique.push_back( (*it).first ); - } - } - return true; - } - return false; -} - void Region::getNumExternalDisequalities( std::map< Node, int >& num_ext_disequalities ){ for( Region::iterator it = begin(); it != end(); ++it ){ @@ -713,25 +697,16 @@ void SortModel::check( Theory::Effort level, OutputChannel* out ){ //see if we have any recommended splits from large regions for( int i=0; i<(int)d_regions_index; i++ ){ if( d_regions[i]->valid() && d_regions[i]->getNumReps()>d_cardinality ){ - //just add the clique lemma - if( level==Theory::EFFORT_FULL && options::ufssCliqueSplits() ){ - std::vector< Node > clique; - if( d_regions[i]->getCandidateClique( d_cardinality, clique ) ){ - //add clique lemma - addCliqueLemma( clique, out ); - return; - } - }else{ - int sp = addSplit( d_regions[i], out ); - if( sp==1 ){ - addedLemma = true; + + int sp = addSplit( d_regions[i], out ); + if( sp==1 ){ + addedLemma = true; #ifdef ONE_SPLIT_REGION - break; + break; #endif - }else if( sp==-1 ){ - check( level, out ); - return; - } + }else if( sp==-1 ){ + check( level, out ); + return; } } } @@ -815,67 +790,6 @@ Node SortModel::getNextDecisionRequest(){ return Node::null(); } -bool SortModel::minimize( OutputChannel* out, TheoryModel* m ){ - if( options::ufssTotality() ){ - //do nothing - }else{ - if( m ){ -#if 0 - // ensure that the constructed model is minimal - // if the model has terms that the strong solver does not know about - if( (int)rs->d_type_reps[ d_type ].size()>d_cardinality ){ - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &m->getEqualityEngine() ); - while( !eqcs_i.isFinished() ){ - Node eqc = (*eqcs_i); - if( eqc.getType()==d_type ){ - //we must ensure that this equivalence class has been accounted for - if( d_regions_map.find( eqc )==d_regions_map.end() ){ - //split on unaccounted for term and cardinality lemma term (as default) - Node splitEq = eqc.eqNode( d_cardinality_term ); - splitEq = Rewriter::rewrite( splitEq ); - Trace("uf-ss-minimize") << "Last chance minimize : " << splitEq << std::endl; - out->split( splitEq ); - //tell the sat solver to explore the equals branch first - out->requirePhase( splitEq, true ); - ++( d_thss->d_statistics.d_split_lemmas ); - return false; - } - } - ++eqcs_i; - } - Assert( false ); - } -#endif - }else{ - Trace("uf-ss-debug") << "Minimize the UF model..." << std::endl; - //internal minimize, ensure that model forms a clique: - // if two equivalence classes are neither equal nor disequal, add a split - int validRegionIndex = -1; - for( int i=0; i<(int)d_regions_index; i++ ){ - if( d_regions[i]->valid() ){ - if( validRegionIndex!=-1 ){ - combineRegions( validRegionIndex, i ); - if( addSplit( d_regions[validRegionIndex], out )!=0 ){ - Trace("uf-ss-debug") << "Minimize model : combined regions, found split. " << std::endl; - return false; - } - }else{ - validRegionIndex = i; - } - } - } - Assert( validRegionIndex!=-1 ); - if( addSplit( d_regions[validRegionIndex], out )!=0 ){ - Trace("uf-ss-debug") << "Minimize model : found split. " << std::endl; - return false; - } - Trace("uf-ss-debug") << "Minimize success. " << std::endl; - } - } - return true; -} - - int SortModel::getNumDisequalitiesToRegion( Node n, int ri ){ int ni = d_regions_map[n]; int counter = 0; @@ -950,21 +864,6 @@ void SortModel::assertCardinality( OutputChannel* out, int c, bool val ){ } } }else{ - /* - if( options::ufssModelInference() ){ - //check if we are at decision level 0 - if( d_th->d_valuation.getAssertionLevel()==0 ){ - Trace("uf-ss-mi") << "We have proved that no models of size " << c << " for type " << d_type << " exist." << std::endl; - Trace("uf-ss-mi") << " # Clique lemmas : " << d_cliques[c].size() << std::endl; - if( d_cliques[c].size()==1 ){ - if( d_totality_terms[c+1].empty() ){ - Trace("uf-ss-mi") << "*** Establish model" << std::endl; - //d_totality_terms[c+1].insert( d_totality_terms[c].begin(), d_cliques[c][0].begin(), d_cliques[c][0].end() ); - } - } - } - } - */ //see if we need to request a new cardinality if( !d_hasCard ){ bool needsCard = true; @@ -1248,12 +1147,6 @@ void SortModel::addCliqueLemma( std::vector< Node >& clique, OutputChannel* out while( clique.size()>size_t(d_cardinality+1) ){ clique.pop_back(); } - //debugging information - if( Trace.isOn("uf-ss-cliques") ){ - std::vector< Node > clique_vec; - clique_vec.insert( clique_vec.begin(), clique.begin(), clique.end() ); - addClique( d_cardinality, clique_vec ); - } // add as lemma std::vector eqs; for (unsigned i = 0, size = clique.size(); i < size; i++) @@ -1323,25 +1216,14 @@ void SortModel::addTotalityAxiom( Node n, int cardinality, OutputChannel* out ){ } } -void SortModel::addClique( int c, std::vector< Node >& clique ) { - //if( d_clique_trie[c].add( clique ) ){ - // d_cliques[ c ].push_back( clique ); - //} -} - - /** apply totality */ bool SortModel::applyTotality( int cardinality ){ return options::ufssTotality() || cardinality<=options::ufssTotalityLimited(); - // || ( options::ufssModelInference() && !d_totality_terms[cardinality].empty() ); } /** get totality lemma terms */ Node SortModel::getTotalityLemmaTerm( int cardinality, int i ){ return d_totality_terms[0][i]; - //}else{ - // return d_totality_terms[cardinality][i]; - //} } void SortModel::simpleCheckCardinality() { @@ -1909,8 +1791,6 @@ SortModel* StrongSolverTheoryUF::getSortModel( Node n ){ } } -void StrongSolverTheoryUF::notifyRestart(){} - /** get cardinality for sort */ int StrongSolverTheoryUF::getCardinality( Node n ) { SortModel* c = getSortModel( n ); @@ -1929,18 +1809,6 @@ int StrongSolverTheoryUF::getCardinality( TypeNode tn ) { return -1; } -bool StrongSolverTheoryUF::minimize( TheoryModel* m ){ - for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ - if( !it->second->minimize( d_out, m ) ){ - return false; - } - } - for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ - Trace("uf-ss-minimize") << "Cardinality( " << it->first << " ) : " << it->second->getCardinality() << std::endl; - } - return true; -} - //print debug void StrongSolverTheoryUF::debugPrint( const char* c ){ //EqClassesIterator< TheoryUF::NotifyClass > eqc_iter( &((TheoryUF*)d_th)->d_equalityEngine ); diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index 5108e7ba1..2e219da04 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -200,8 +200,6 @@ public: void getNumExternalDisequalities(std::map< Node, int >& num_ext_disequalities ); /** check for cliques */ bool check( Theory::Effort level, int cardinality, std::vector< Node >& clique ); - /** get candidate clique */ - bool getCandidateClique( int cardinality, std::vector< Node >& clique ); //print debug void debugPrint( const char* c, bool incClique = false ); @@ -260,26 +258,6 @@ public: void addCliqueLemma( std::vector< Node >& clique, OutputChannel* out ); /** add totality axiom */ void addTotalityAxiom( Node n, int cardinality, OutputChannel* out ); - - class NodeTrie { - public: - bool add( std::vector< Node >& n, unsigned i = 0 ){ - Assert( i d_children; - }; /* class NodeTrie */ - - std::map< int, NodeTrie > d_clique_trie; - void addClique( int c, std::vector< Node >& clique ); - /** Are we in conflict */ context::CDO d_conflict; /** cardinality */ @@ -338,8 +316,6 @@ public: void propagate( Theory::Effort level, OutputChannel* out ); /** get next decision request */ Node getNextDecisionRequest(); - /** minimize */ - bool minimize( OutputChannel* out, TheoryModel* m ); /** assert cardinality */ void assertCardinality( OutputChannel* out, int c, bool val ); /** is in conflict */ @@ -393,8 +369,6 @@ public: Node getNextDecisionRequest( unsigned& priority ); /** preregister a term */ void preRegisterTerm( TNode n ); - /** notify restart */ - void notifyRestart(); /** identify */ std::string identify() const { return std::string("StrongSolverTheoryUF"); } //print debug @@ -407,8 +381,6 @@ public: int getCardinality( Node n ); /** get cardinality for type */ int getCardinality( TypeNode tn ); - /** minimize */ - bool minimize( TheoryModel* m = NULL ); /** has eqc */ bool hasEqc(Node a); -- 2.30.2