remove duplicate function TheoryEngine::getTheory(TheoryId). It was a duplicate...

diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 4d91c8c9533130429c104e948a01ed6235447958..cbeeed8d05bd294b916fcc4855da4ea01c3e0c3d 100644 (file)
--- 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 bb8fafb142c03205c7b5ae47a28a6c38694b9a46..e1cd7e42cea725091f2141c44fb84e965c19ae8d 100644 (file)
--- 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 4bb85287ecd69b145d30a861394d6584c7160f2f..3bd2945e8805dcb5c9346382746c940b6693f58c 100644 (file)
--- 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 df08312b1b719aa2c09e4616c3825566e3b222a1..3dcd20d7863676eb40e2789c28778fa0ef023ce8 100644 (file)
--- 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 25b184fe2a1b227798e72ae73058569f966cf114..9ac3550366536a9e67c5a90d06789fed3af9067a 100644 (file)
--- 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<uf::TheoryUF *>(qe->getTheoryEngine()->getTheory( theory::THEORY_UF ));
+    uf::TheoryUF* uf = static_cast<uf::TheoryUF *>(qe->getTheoryEngine()->theoryOf( theory::THEORY_UF ));
     eq::EqualityEngine* ee = static_cast<eq::EqualityEngine*>(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<uf::TheoryUF::NotifyClass>* ee = (static_cast<uf::TheoryUF*>(qe->getTheoryEngine()->getTheory( theory::THEORY_UF )))->getEqualityEngine();
+    //   uf::EqualityEngine<uf::TheoryUF::NotifyClass>* ee = (static_cast<uf::TheoryUF*>(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<datatypes::TheoryDatatypes *>(qe->getTheoryEngine()->getTheory( theory::THEORY_DATATYPES ));
+    datatypes::TheoryDatatypes* dt = static_cast<datatypes::TheoryDatatypes *>(qe->getTheoryEngine()->theoryOf( theory::THEORY_DATATYPES ));
     eq::EqualityEngine* ee = static_cast<eq::EqualityEngine*>(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<arrays::TheoryArrays *>(qe->getTheoryEngine()->getTheory( theory::THEORY_ARRAY ));
+    arrays::TheoryArrays* ar = static_cast<arrays::TheoryArrays *>(qe->getTheoryEngine()->theoryOf( theory::THEORY_ARRAY ));
     eq::EqualityEngine* ee =
       static_cast<eq::EqualityEngine*>(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<uf::TheoryUF::NotifyClass>* ee = (static_cast<uf::TheoryUF*>(qe->getTheoryEngine()->getTheory( theory::THEORY_UF )))->getEqualityEngine();
+    //   uf::EqualityEngine<uf::TheoryUF::NotifyClass>* ee = (static_cast<uf::TheoryUF*>(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<datatypes::TheoryDatatypes *>(te->getTheory( theory::THEORY_DATATYPES ));
+      // datatypes::TheoryDatatypes* dt = static_cast<datatypes::TheoryDatatypes *>(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<arrays::TheoryArrays *>(te->getTheory( theory::THEORY_ARRAY ));
+      arrays::TheoryArrays* ar = static_cast<arrays::TheoryArrays *>(te->theoryOf( theory::THEORY_ARRAY ));
       eq::EqualityEngine* ee =
         static_cast<eq::EqualityEngine*>(ar->getEqualityEngine());
       return new CandidateGeneratorTheoryEeClasses(ee);
     } else {
-      uf::TheoryUF* uf = static_cast<uf::TheoryUF*>(te->getTheory( theory::THEORY_UF ));
+      uf::TheoryUF* uf = static_cast<uf::TheoryUF*>(te->theoryOf( theory::THEORY_UF ));
       eq::EqualityEngine* ee =
         static_cast<eq::EqualityEngine*>(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<uf::TheoryUF*>(qe->getTheoryEngine()->getTheory( theory::THEORY_UF ));
+    uf::TheoryUF* uf = static_cast<uf::TheoryUF*>(qe->getTheoryEngine()->theoryOf( theory::THEORY_UF ));
     eq::EqualityEngine* ee =
       static_cast<eq::EqualityEngine*>(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<uf::TheoryUF*>(qe->getTheoryEngine()->getTheory( theory::THEORY_UF ));
+    uf::TheoryUF* uf = static_cast<uf::TheoryUF*>(qe->getTheoryEngine()->theoryOf( theory::THEORY_UF ));
     eq::EqualityEngine* ee =
       static_cast<eq::EqualityEngine*>(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<uf::TheoryUF*>(qe->getTheoryEngine()->getTheory( theory::THEORY_UF )))->getEqualityEngine()->
+    false_term((static_cast<uf::TheoryUF*>(qe->getTheoryEngine()->theoryOf( theory::THEORY_UF )))->getEqualityEngine()->
                 getRepresentative(NodeManager::currentNM()->mkConst<bool>(false) )){};
   void resetInstantiationRound( QuantifiersEngine* qe ){
     d_cgm.resetInstantiationRound(qe);
@@ -970,7 +970,7 @@ Matcher* mkMatcher( Node pat, QuantifiersEngine* qe ){
       TestMatcher<ArithMatcher, LegalTypeTest>
         am2(am3,LegalTypeTest(pat.getType()));
       /* generator */
-      uf::TheoryUF* uf = static_cast<uf::TheoryUF*>(qe->getTheoryEngine()->getTheory( theory::THEORY_UF ));
+      uf::TheoryUF* uf = static_cast<uf::TheoryUF*>(qe->getTheoryEngine()->theoryOf( theory::THEORY_UF ));
       eq::EqualityEngine* ee =
         static_cast<eq::EqualityEngine*> (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 b4ae936539d7c409f44c59a8b5bbb60a1a71fc06..6bf4ca22d6733bf010057643c5b51db5dfaef3de 100644 (file)
--- 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<uf::TheoryUF *>(getQuantifiersEngine()->getTheoryEngine()->getTheory( theory::THEORY_UF ));
+    uf::TheoryUF* uf = static_cast<uf::TheoryUF *>(getQuantifiersEngine()->getTheoryEngine()->theoryOf( theory::THEORY_UF ));
     eq::EqualityEngine* ee =
       static_cast<eq::EqualityEngine*>(uf->getEqualityEngine());
 

diff --git a/src/theory/rewriterules/theory_rewriterules_rules.cpp b/src/theory/rewriterules/theory_rewriterules_rules.cpp
index edea7a3c0b7fbd9b1b0ec8e5e192f42d607e04ae..0356568c5a0d06db6164864788e585c3c17fa225 100644 (file)
--- 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 9dedc32923d361d84ba28c12bcd9673c53fd13f9..75f4d6a3746005cfb9c427bbb5de43dd4ea8fe6c 100644 (file)
--- 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.