drastic simplification of quantifiers code regarding equality queries, instantiation strategies moved from instantiators to central instantiation engine, removed instantiator objects, simplified rewrite rules candidate generator to use central equality engine, efficient e-matching now uses central equality engine

5 files changed, 17 insertions, 82 deletions

diff --git a/src/theory/rewriterules/efficient_e_matching.cpp b/src/theory/rewriterules/efficient_e_matching.cpp
index 7f03bf8f8..2f39d8098 100755
--- a/src/theory/rewriterules/efficient_e_matching.cpp
+++ b/src/theory/rewriterules/efficient_e_matching.cpp
@@ -92,7 +92,8 @@ EfficientEMatcher::EfficientEMatcher( CVC4::theory::QuantifiersEngine* qe ) : d_
 }

 

 eq::EqualityEngine* EfficientEMatcher::getEqualityEngine(){

-  return ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getEqualityEngine();

+  //return ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getEqualityEngine();

+  return d_quantEngine->getMasterEqualityEngine();

 }

 

 /** new node */

diff --git a/src/theory/rewriterules/rr_candidate_generator.cpp b/src/theory/rewriterules/rr_candidate_generator.cpp
index 2957b4ddb..3f2895397 100644
--- a/src/theory/rewriterules/rr_candidate_generator.cpp
+++ b/src/theory/rewriterules/rr_candidate_generator.cpp
@@ -24,100 +24,44 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::rrinst;
 
-GenericCandidateGeneratorClasses::GenericCandidateGeneratorClasses(QuantifiersEngine * qe){
-  for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){
-    if(qe->getInstantiator(i) != NULL)
-      d_can_gen[i] = qe->getInstantiator(i)->getRRCanGenClasses();
-    else d_can_gen[i] = NULL;
-  }
+GenericCandidateGeneratorClasses::GenericCandidateGeneratorClasses(QuantifiersEngine * qe) : d_qe(qe){
+  d_master_can_gen = new eq::rrinst::CandidateGeneratorTheoryEeClasses(d_qe->getMasterEqualityEngine());
 }
 
 GenericCandidateGeneratorClasses::~GenericCandidateGeneratorClasses(){
-  for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){
-    delete(d_can_gen[i]);
-  }
+  delete d_master_can_gen;
 }
 
 void GenericCandidateGeneratorClasses::resetInstantiationRound(){
-  for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){
-    if(d_can_gen[i] != NULL) d_can_gen[i]->resetInstantiationRound();
-  }
-  d_can_gen_id=THEORY_FIRST;
+  d_master_can_gen->resetInstantiationRound();
 }
 
 void GenericCandidateGeneratorClasses::reset(TNode eqc){
-  Assert(eqc.isNull());
-  for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){
-    if(d_can_gen[i] != NULL) d_can_gen[i]->reset(eqc);
-  }
-  d_can_gen_id=THEORY_FIRST;
-  lookForNextTheory();
+  d_master_can_gen->reset(eqc);
 }
 
 TNode GenericCandidateGeneratorClasses::getNextCandidate(){
-  Assert(THEORY_FIRST <= d_can_gen_id && d_can_gen_id <= THEORY_LAST);
-  /** No more */
-  if(d_can_gen_id == THEORY_LAST) return TNode::null();
-  /** Try with this theory */
-  TNode cand = d_can_gen[d_can_gen_id]->getNextCandidate();
-  if( !cand.isNull() ) return cand;
-  lookForNextTheory();
-  return getNextCandidate();
+  return d_master_can_gen->getNextCandidate();
 }
 
-void GenericCandidateGeneratorClasses::lookForNextTheory(){
-  do{ /* look for the next available generator */
-    ++d_can_gen_id;
-  } while( d_can_gen_id < THEORY_LAST && d_can_gen[d_can_gen_id] == NULL);
-}
 
 GenericCandidateGeneratorClass::GenericCandidateGeneratorClass(QuantifiersEngine * qe): d_qe(qe) {
-  for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){
-    if(d_qe->getInstantiator(i) != NULL)
-      d_can_gen[i] = d_qe->getInstantiator(i)->getRRCanGenClass();
-    else d_can_gen[i] = NULL;
-  }
+  d_master_can_gen = new eq::rrinst::CandidateGeneratorTheoryEeClass(d_qe->getMasterEqualityEngine());
 }
 
 GenericCandidateGeneratorClass::~GenericCandidateGeneratorClass(){
-  for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){
-    delete(d_can_gen[i]);
-  }
+  delete d_master_can_gen;
 }
 
 void GenericCandidateGeneratorClass::resetInstantiationRound(){
-  for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){
-    if(d_can_gen[i] != NULL) d_can_gen[i]->resetInstantiationRound();
-  }
-  d_can_gen_id=THEORY_FIRST;
+  d_master_can_gen->resetInstantiationRound();
 }
 
 void GenericCandidateGeneratorClass::reset(TNode eqc){
-  for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){
-    if(d_can_gen[i] != NULL) d_can_gen[i]->reset(eqc);
-  }
-  d_can_gen_id=THEORY_FIRST;
-  d_node = eqc;
-  lookForNextTheory();
+  d_master_can_gen->reset(eqc);
 }
 
 TNode GenericCandidateGeneratorClass::getNextCandidate(){
-  Assert(THEORY_FIRST <= d_can_gen_id && d_can_gen_id <= THEORY_LAST);
-  /** No more */
-  if(d_can_gen_id == THEORY_LAST) return TNode::null();
-  /** Try with this theory */
-  TNode cand = d_can_gen[d_can_gen_id]->getNextCandidate();
-  if( !cand.isNull() ) return cand;
-  lookForNextTheory();
-  return getNextCandidate();
+  return d_master_can_gen->getNextCandidate();
 }
 
-void GenericCandidateGeneratorClass::lookForNextTheory(){
-  do{ /* look for the next available generator, where the element is */
-    ++d_can_gen_id;
-  } while(
-          d_can_gen_id < THEORY_LAST &&
-          (d_can_gen[d_can_gen_id] == NULL ||
-           !d_qe->getInstantiator( d_can_gen_id )->hasTerm( d_node ))
-          );
-}
diff --git a/src/theory/rewriterules/rr_candidate_generator.h b/src/theory/rewriterules/rr_candidate_generator.h
index 8ebaae343..97c710219 100644
--- a/src/theory/rewriterules/rr_candidate_generator.h
+++ b/src/theory/rewriterules/rr_candidate_generator.h
@@ -166,10 +166,9 @@ public:
 class GenericCandidateGeneratorClasses: public rrinst::CandidateGenerator{
 
   /** The candidate generators */
-  rrinst::CandidateGenerator* d_can_gen[theory::THEORY_LAST];
-  /** The current theory which candidategenerator is used */
-  TheoryId d_can_gen_id;
-
+  rrinst::CandidateGenerator* d_master_can_gen;
+  /** QuantifierEngine */
+  QuantifiersEngine* d_qe;
 public:
   GenericCandidateGeneratorClasses(QuantifiersEngine * qe);
   ~GenericCandidateGeneratorClasses();
@@ -183,22 +182,15 @@ public:
 class GenericCandidateGeneratorClass: public rrinst::CandidateGenerator{
 
   /** The candidate generators */
-  rrinst::CandidateGenerator* d_can_gen[theory::THEORY_LAST];
-  /** The current theory which candidategenerator is used */
-  TheoryId d_can_gen_id;
-  /** current node to look for equivalence class */
-  Node d_node;
+  rrinst::CandidateGenerator* d_master_can_gen;
   /** QuantifierEngine */
   QuantifiersEngine* d_qe;
-
 public:
   GenericCandidateGeneratorClass(QuantifiersEngine * qe);
   ~GenericCandidateGeneratorClass();
   void resetInstantiationRound();
-
   void reset(TNode eqc);
   TNode getNextCandidate();
-  void lookForNextTheory();
 };
 
 }/* CVC4::theory namespace */
diff --git a/src/theory/rewriterules/rr_inst_match.cpp b/src/theory/rewriterules/rr_inst_match.cpp
index 5f10e1daa..5c3a55831 100644
--- a/src/theory/rewriterules/rr_inst_match.cpp
+++ b/src/theory/rewriterules/rr_inst_match.cpp
@@ -15,7 +15,6 @@
 #include "theory/quantifiers/inst_match.h"
 #include "theory/theory_engine.h"
 #include "theory/quantifiers_engine.h"
-#include "theory/uf/theory_uf_instantiator.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/arrays/theory_arrays.h"
 #include "theory/datatypes/theory_datatypes.h"
diff --git a/src/theory/rewriterules/rr_trigger.cpp b/src/theory/rewriterules/rr_trigger.cpp
index ad77f0bcb..4f48a72ae 100644
--- a/src/theory/rewriterules/rr_trigger.cpp
+++ b/src/theory/rewriterules/rr_trigger.cpp
@@ -15,7 +15,6 @@
 #include "theory/rewriterules/rr_trigger.h"
 #include "theory/theory_engine.h"
 #include "theory/quantifiers_engine.h"
-#include "theory/uf/theory_uf_instantiator.h"
 #include "theory/rewriterules/rr_candidate_generator.h"
 #include "theory/uf/equality_engine.h"