From: Morgan Deters Date: Mon, 20 Aug 2012 22:01:14 +0000 (+0000) Subject: remove duplicate function TheoryEngine::getTheory(TheoryId). It was a duplicate... X-Git-Tag: cvc5-1.0.0~7858 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=59046763d2e5b26d720a3a320b351292bad867ac;p=cvc5.git remove duplicate function TheoryEngine::getTheory(TheoryId). It was a duplicate of TheoryEngine::theoryOf(TheoryId) --- diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 4d91c8c95..cbeeed8d0 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -50,7 +50,7 @@ d_rel_domain( qe->getModel() ){ void ModelEngine::check( Theory::Effort e ){ if( e==Theory::EFFORT_LAST_CALL && !d_quantEngine->hasAddedLemma() ){ //first, check if we can minimize the model further - if( !((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->getTheory( THEORY_UF ))->getStrongSolver()->minimize() ){ + if( !((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->minimize() ){ return; } //the following will attempt to build a model and test that it satisfies all asserted universal quantifiers diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index bb8fafb14..e1cd7e42c 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -104,7 +104,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ addedLemmas += d_ith->d_op_triggers[op][i]->addTerm( n ); } //Message() << "Terms, added lemmas: " << addedLemmas << std::endl; - d_quantEngine->flushLemmas( &d_quantEngine->getTheoryEngine()->getTheory( THEORY_QUANTIFIERS )->getOutputChannel() ); + d_quantEngine->flushLemmas( &d_quantEngine->getTheoryEngine()->theoryOf( THEORY_QUANTIFIERS )->getOutputChannel() ); } } } diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 4bb85287e..3bd2945e8 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -97,7 +97,7 @@ d_quantEngine( qe ), d_f( f ){ } //Notice() << "Trigger : " << (*this) << " for " << f << std::endl; if( options::eagerInstQuant() ){ - Theory* th_uf = qe->getTheoryEngine()->getTheory( theory::THEORY_UF ); + Theory* th_uf = qe->getTheoryEngine()->theoryOf( theory::THEORY_UF ); uf::InstantiatorTheoryUf* ith = (uf::InstantiatorTheoryUf*)th_uf->getInstantiator(); for( int i=0; i<(int)d_nodes.size(); i++ ){ ith->registerTrigger( this, d_nodes[i].getOperator() ); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index df08312b1..3dcd20d78 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -101,19 +101,19 @@ QuantifiersEngine::~QuantifiersEngine(){ } Instantiator* QuantifiersEngine::getInstantiator( theory::TheoryId id ){ - return d_te->getTheory( id )->getInstantiator(); + return d_te->theoryOf( id )->getInstantiator(); } context::Context* QuantifiersEngine::getSatContext(){ - return d_te->getTheory( THEORY_QUANTIFIERS )->getSatContext(); + return d_te->theoryOf( THEORY_QUANTIFIERS )->getSatContext(); } OutputChannel& QuantifiersEngine::getOutputChannel(){ - return d_te->getTheory( THEORY_QUANTIFIERS )->getOutputChannel(); + return d_te->theoryOf( THEORY_QUANTIFIERS )->getOutputChannel(); } /** get default valuation for the quantifiers engine */ Valuation& QuantifiersEngine::getValuation(){ - return d_te->getTheory( THEORY_QUANTIFIERS )->getValuation(); + return d_te->theoryOf( THEORY_QUANTIFIERS )->getValuation(); } void QuantifiersEngine::check( Theory::Effort e ){ @@ -211,7 +211,7 @@ void QuantifiersEngine::registerQuantifier( Node f ){ generatePhaseReqs( quants[q], ceBody ); //also register it with the strong solver if( options::finiteModelFind() ){ - ((uf::TheoryUF*)d_te->getTheory( THEORY_UF ))->getStrongSolver()->registerQuantifier( quants[q] ); + ((uf::TheoryUF*)d_te->theoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( quants[q] ); } } } @@ -723,7 +723,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a ){ } eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){ - return ((uf::TheoryUF*)d_qe->getTheoryEngine()->getTheory( THEORY_UF ))->getEqualityEngine(); + return ((uf::TheoryUF*)d_qe->getTheoryEngine()->theoryOf( THEORY_UF ))->getEqualityEngine(); } void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a, std::vector< Node >& eqc ){ diff --git a/src/theory/rewriterules/rr_inst_match.cpp b/src/theory/rewriterules/rr_inst_match.cpp index 25b184fe2..9ac355036 100644 --- a/src/theory/rewriterules/rr_inst_match.cpp +++ b/src/theory/rewriterules/rr_inst_match.cpp @@ -436,7 +436,7 @@ class OpMatcher: public Matcher{ /** Keep only the one that have the good operator */ AuxMatcher2 am2(am3,LegalOpTest(pat.getOperator())); /** Iter on the equivalence class of the given term */ - uf::TheoryUF* uf = static_cast(qe->getTheoryEngine()->getTheory( theory::THEORY_UF )); + uf::TheoryUF* uf = static_cast(qe->getTheoryEngine()->theoryOf( theory::THEORY_UF )); eq::EqualityEngine* ee = static_cast(uf->getEqualityEngine()); CandidateGeneratorTheoryEeClass cdtUfEq(ee); /* Create a matcher from the candidate generator */ @@ -456,7 +456,7 @@ public: bool reset( TNode t, InstMatch& m, QuantifiersEngine* qe ){ // size_t m_size = m.d_map.size(); // if(m_size == d_num_var){ - // uf::EqualityEngine* ee = (static_cast(qe->getTheoryEngine()->getTheory( theory::THEORY_UF )))->getEqualityEngine(); + // uf::EqualityEngine* ee = (static_cast(qe->getTheoryEngine()->theoryOf( theory::THEORY_UF )))->getEqualityEngine(); // std::cout << "!"; // return ee->areEqual(m.subst(d_pat),t); // }else{ @@ -483,7 +483,7 @@ class DatatypesMatcher: public Matcher{ /** Keep only the one that have the good operator */ AuxMatcher2 am2(am3,LegalOpTest(pat.getOperator())); /** Iter on the equivalence class of the given term */ - datatypes::TheoryDatatypes* dt = static_cast(qe->getTheoryEngine()->getTheory( theory::THEORY_DATATYPES )); + datatypes::TheoryDatatypes* dt = static_cast(qe->getTheoryEngine()->theoryOf( theory::THEORY_DATATYPES )); eq::EqualityEngine* ee = static_cast(dt->getEqualityEngine()); CandidateGeneratorTheoryEeClass cdtDtEq(ee); /* Create a matcher from the candidate generator */ @@ -521,7 +521,7 @@ class ArrayMatcher: public Matcher{ /** Keep only the one that have the good operator */ AuxMatcher2 am2(am3, LegalKindTest(pat.getKind())); /** Iter on the equivalence class of the given term */ - arrays::TheoryArrays* ar = static_cast(qe->getTheoryEngine()->getTheory( theory::THEORY_ARRAY )); + arrays::TheoryArrays* ar = static_cast(qe->getTheoryEngine()->theoryOf( theory::THEORY_ARRAY )); eq::EqualityEngine* ee = static_cast(ar->getEqualityEngine()); CandidateGeneratorTheoryEeClass cdtUfEq(ee); @@ -542,7 +542,7 @@ public: bool reset( TNode t, InstMatch& m, QuantifiersEngine* qe ){ // size_t m_size = m.d_map.size(); // if(m_size == d_num_var){ - // uf::EqualityEngine* ee = (static_cast(qe->getTheoryEngine()->getTheory( theory::THEORY_UF )))->getEqualityEngine(); + // uf::EqualityEngine* ee = (static_cast(qe->getTheoryEngine()->theoryOf( theory::THEORY_UF )))->getEqualityEngine(); // std::cout << "!"; // return ee->areEqual(m.subst(d_pat),t); // }else{ @@ -715,16 +715,16 @@ public: Debug("inst-match-gen") << "MetaCandidateGenerator for type: " << ty << " Theory : " << Theory::theoryOf(ty) << std::endl; if( Theory::theoryOf(ty) == theory::THEORY_DATATYPES ){ - // datatypes::TheoryDatatypes* dt = static_cast(te->getTheory( theory::THEORY_DATATYPES )); + // datatypes::TheoryDatatypes* dt = static_cast(te->theoryOf( theory::THEORY_DATATYPES )); // return new datatypes::rrinst::CandidateGeneratorTheoryClasses(dt); Unimplemented("MetaCandidateGeneratorClasses for THEORY_DATATYPES"); }else if ( Theory::theoryOf(ty) == theory::THEORY_ARRAY ){ - arrays::TheoryArrays* ar = static_cast(te->getTheory( theory::THEORY_ARRAY )); + arrays::TheoryArrays* ar = static_cast(te->theoryOf( theory::THEORY_ARRAY )); eq::EqualityEngine* ee = static_cast(ar->getEqualityEngine()); return new CandidateGeneratorTheoryEeClasses(ee); } else { - uf::TheoryUF* uf = static_cast(te->getTheory( theory::THEORY_UF )); + uf::TheoryUF* uf = static_cast(te->theoryOf( theory::THEORY_UF )); eq::EqualityEngine* ee = static_cast(uf->getEqualityEngine()); return new CandidateGeneratorTheoryEeClasses(ee); @@ -860,7 +860,7 @@ private: /** Keep only the one that have the good type */ AuxMatcher2 am2(am3,LegalTypeTest(ty)); /** Generate one term by eq classes */ - uf::TheoryUF* uf = static_cast(qe->getTheoryEngine()->getTheory( theory::THEORY_UF )); + uf::TheoryUF* uf = static_cast(qe->getTheoryEngine()->theoryOf( theory::THEORY_UF )); eq::EqualityEngine* ee = static_cast(uf->getEqualityEngine()); CandidateGeneratorTheoryEeClasses cdtUfEq(ee); @@ -916,7 +916,7 @@ private: /** Keep only the one that have the good type */ AuxMatcher2 am2(am3,EqTest(ty)); /** Will generate all the terms of the eq class of false */ - uf::TheoryUF* uf = static_cast(qe->getTheoryEngine()->getTheory( theory::THEORY_UF )); + uf::TheoryUF* uf = static_cast(qe->getTheoryEngine()->theoryOf( theory::THEORY_UF )); eq::EqualityEngine* ee = static_cast(uf->getEqualityEngine()); CandidateGeneratorTheoryEeClass cdtUfEq(ee); @@ -927,7 +927,7 @@ private: public: UfDeqMatcher( Node pat, QuantifiersEngine* qe ): d_cgm(createCgm(pat, qe)), - false_term((static_cast(qe->getTheoryEngine()->getTheory( theory::THEORY_UF )))->getEqualityEngine()-> + false_term((static_cast(qe->getTheoryEngine()->theoryOf( theory::THEORY_UF )))->getEqualityEngine()-> getRepresentative(NodeManager::currentNM()->mkConst(false) )){}; void resetInstantiationRound( QuantifiersEngine* qe ){ d_cgm.resetInstantiationRound(qe); @@ -970,7 +970,7 @@ Matcher* mkMatcher( Node pat, QuantifiersEngine* qe ){ TestMatcher am2(am3,LegalTypeTest(pat.getType())); /* generator */ - uf::TheoryUF* uf = static_cast(qe->getTheoryEngine()->getTheory( theory::THEORY_UF )); + uf::TheoryUF* uf = static_cast(qe->getTheoryEngine()->theoryOf( theory::THEORY_UF )); eq::EqualityEngine* ee = static_cast (uf->getEqualityEngine()); CandidateGeneratorTheoryEeClass cdtUfEq(ee); @@ -1402,7 +1402,7 @@ public: d_direct_patterns.push_back(new ApplyMatcher(pats[i],qe)); } }; - Theory* th_uf = qe->getTheoryEngine()->getTheory( theory::THEORY_UF ); + Theory* th_uf = qe->getTheoryEngine()->theoryOf( theory::THEORY_UF ); uf::InstantiatorTheoryUf* ith = (uf::InstantiatorTheoryUf*)th_uf->getInstantiator(); ith->registerEfficientHandler(d_eh, pats); }; diff --git a/src/theory/rewriterules/theory_rewriterules.cpp b/src/theory/rewriterules/theory_rewriterules.cpp index b4ae93653..6bf4ca22d 100644 --- a/src/theory/rewriterules/theory_rewriterules.cpp +++ b/src/theory/rewriterules/theory_rewriterules.cpp @@ -526,7 +526,7 @@ void TheoryRewriteRules::propagateRule(const RuleInst * inst, TCache cache){ if ( compute_opt && !rule->body_match.empty() ){ - uf::TheoryUF* uf = static_cast(getQuantifiersEngine()->getTheoryEngine()->getTheory( theory::THEORY_UF )); + uf::TheoryUF* uf = static_cast(getQuantifiersEngine()->getTheoryEngine()->theoryOf( theory::THEORY_UF )); eq::EqualityEngine* ee = static_cast(uf->getEqualityEngine()); diff --git a/src/theory/rewriterules/theory_rewriterules_rules.cpp b/src/theory/rewriterules/theory_rewriterules_rules.cpp index edea7a3c0..0356568c5 100644 --- a/src/theory/rewriterules/theory_rewriterules_rules.cpp +++ b/src/theory/rewriterules/theory_rewriterules_rules.cpp @@ -371,7 +371,7 @@ bool TheoryRewriteRules::addRewritePattern(TNode pattern, TNode body, if (i == d_registeredRRPpRewrite.end()){ p = new rewriter::RRPpRewrite(); d_registeredRRPpRewrite.insert(std::make_pair(op,p)); - ((uf::TheoryUF*)getQuantifiersEngine()->getTheoryEngine()->getTheory( THEORY_UF ))-> + ((uf::TheoryUF*)getQuantifiersEngine()->getTheoryEngine()->theoryOf( THEORY_UF ))-> registerPpRewrite(op,p); } else p = i->second; diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 9dedc3292..75f4d6a37 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -639,22 +639,14 @@ public: } /** - * Get the theory associated to a the given theory id. It will also mark the - * theory as currently active, we assume that theories are called only through - * theoryOf. + * Get the theory associated to a the given theory id. * - * @returns the theory, or NULL if the TNode is - * of built-in type. + * @returns the theory */ inline theory::Theory* theoryOf(theory::TheoryId theoryId) const { return d_theoryTable[theoryId]; } - /** Get the theory for id */ - theory::Theory* getTheory(theory::TheoryId theoryId) const { - return d_theoryTable[theoryId]; - } - /** * Returns the equality status of the two terms, from the theory * that owns the domain type. The types of a and b must be the same.