quantifiers now uses master equality engine, preparation work to cleanup code

5 files changed, 82 insertions, 112 deletions

diff --git a/src/theory/uf/inst_strategy.cpp b/src/theory/uf/inst_strategy.cpp
index 433ceee85..8c90d569a 100644
--- a/src/theory/uf/inst_strategy.cpp
+++ b/src/theory/uf/inst_strategy.cpp
@@ -75,10 +75,11 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){
       if( processTrigger ){
         //if( d_user_gen[f][i]->isMultiTrigger() )
           //Notice() << "  Process (user) " << (*d_user_gen[f][i]) << " for " << f << "..." << std::endl;
-        int numInst = d_user_gen[f][i]->addInstantiations( d_th->d_baseMatch[f] );
+        InstMatch baseMatch;
+        int numInst = d_user_gen[f][i]->addInstantiations( baseMatch );
         //if( d_user_gen[f][i]->isMultiTrigger() )
           //Notice() << "  Done, numInst = " << numInst << "." << std::endl;
-        d_th->d_statistics.d_instantiations_user_pattern += numInst;
+        //d_statistics.d_instantiations += numInst;
         if( d_user_gen[f][i]->isMultiTrigger() ){
           d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
         }
@@ -106,6 +107,17 @@ void InstStrategyUserPatterns::addUserPattern( Node f, Node pat ){
                                                  options::smartTriggers() ) );
   }
 }
+/*
+InstStrategyUserPatterns::Statistics::Statistics():
+  d_instantiations("InstStrategyUserPatterns::Instantiations", 0)
+{
+  StatisticsRegistry::registerStat(&d_instantiations);
+}
+
+InstStrategyUserPatterns::Statistics::~Statistics(){
+  StatisticsRegistry::unregisterStat(&d_instantiations);
+}
+*/
 
 void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort effort ){
   //reset triggers
@@ -153,14 +165,15 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e )
         if( processTrigger ){
           //if( tr->isMultiTrigger() )
             Debug("quant-uf-strategy-auto-gen-triggers") << "  Process " << (*tr) << "..." << std::endl;
-          int numInst = tr->addInstantiations( d_th->d_baseMatch[f] );
+          InstMatch baseMatch;
+          int numInst = tr->addInstantiations( baseMatch );
           //if( tr->isMultiTrigger() )
             Debug("quant-uf-strategy-auto-gen-triggers") << "  Done, numInst = " << numInst << "." << std::endl;
-          if( d_tr_strategy==Trigger::TS_MIN_TRIGGER ){
-            d_th->d_statistics.d_instantiations_auto_gen_min += numInst;
-          }else{
-            d_th->d_statistics.d_instantiations_auto_gen += numInst;
-          }
+          //if( d_tr_strategy==Trigger::TS_MIN_TRIGGER ){
+          //  d_statistics.d_instantiations_min += numInst;
+          //}else{
+          //  d_statistics.d_instantiations += numInst;
+          //}
           if( tr->isMultiTrigger() ){
             d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
           }
@@ -321,6 +334,20 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
     }
   }
 }
+/*
+InstStrategyAutoGenTriggers::Statistics::Statistics():
+  d_instantiations("InstStrategyAutoGenTriggers::Instantiations", 0),
+  d_instantiations_min("InstStrategyAutoGenTriggers::Instantiations_min", 0)
+{
+  StatisticsRegistry::registerStat(&d_instantiations);
+  StatisticsRegistry::registerStat(&d_instantiations_min);
+}
+
+InstStrategyAutoGenTriggers::Statistics::~Statistics(){
+  StatisticsRegistry::unregisterStat(&d_instantiations);
+  StatisticsRegistry::unregisterStat(&d_instantiations_min);
+}
+*/
 
 void InstStrategyFreeVariable::processResetInstantiationRound( Theory::Effort effort ){
 }
@@ -334,10 +361,21 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){
       Debug("quant-uf-alg") << "Add guessed instantiation" << std::endl;
       InstMatch m;
       if( d_quantEngine->addInstantiation( f, m ) ){
-        ++(d_th->d_statistics.d_instantiations_guess);
+        //++(d_statistics.d_instantiations);
         //d_quantEngine->d_hasInstantiated[f] = true;
       }
     }
     return STATUS_UNKNOWN;
   }
 }
+/*
+InstStrategyFreeVariable::Statistics::Statistics():
+  d_instantiations("InstStrategyGuess::Instantiations", 0)
+{
+  StatisticsRegistry::registerStat(&d_instantiations);
+}
+
+InstStrategyFreeVariable::Statistics::~Statistics(){
+  StatisticsRegistry::unregisterStat(&d_instantiations);
+}
+*/
\ No newline at end of file
diff --git a/src/theory/uf/inst_strategy.h b/src/theory/uf/inst_strategy.h
index aaa5f27a1..42d401126 100644
--- a/src/theory/uf/inst_strategy.h
+++ b/src/theory/uf/inst_strategy.h
@@ -58,6 +58,15 @@ public:
   inst::Trigger* getUserGenerator( Node f, int i ) { return d_user_gen[f][ i ]; }
   /** identify */
   std::string identify() const { return std::string("UserPatterns"); }
+public:
+  /** statistics class */
+  //class Statistics {
+  //public:
+  //  IntStat d_instantiations;
+  //  Statistics();
+  //  ~Statistics();
+  //};
+  //Statistics d_statistics;
 };/* class InstStrategyUserPatterns */
 
 class InstStrategyAutoGenTriggers : public InstStrategy{
@@ -114,6 +123,16 @@ public:
   }
   /** set generate additional */
   void setGenerateAdditional( bool val ) { d_generate_additional = val; }
+public:
+  /** statistics class */
+  //class Statistics {
+  //public:
+  //  IntStat d_instantiations;
+  //  IntStat d_instantiations_min;
+  //  Statistics();
+  //  ~Statistics();
+  //};
+  //Statistics d_statistics;
 };/* class InstStrategyAutoGenTriggers */
 
 class InstStrategyFreeVariable : public InstStrategy{
@@ -131,6 +150,15 @@ public:
   ~InstStrategyFreeVariable(){}
   /** identify */
   std::string identify() const { return std::string("FreeVariable"); }
+public:
+  /** statistics class */
+  //class Statistics {
+  //public:
+  //  IntStat d_instantiations;
+  //  Statistics();
+  //  ~Statistics();
+  //};
+  //Statistics d_statistics;
 };/* class InstStrategyFreeVariable */
 
 }/* CVC4::theory::uf namespace */
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index e6ae3747c..23f100f74 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -22,6 +22,8 @@
 #include "theory/uf/theory_uf_strong_solver.h"
 #include "theory/model.h"
 #include "theory/type_enumerator.h"
+//included since efficient e matching needs notifications from UF
+#include "theory/rewriterules/efficient_e_matching.h"
 
 using namespace std;
 using namespace CVC4;
@@ -479,13 +481,13 @@ void TheoryUF::eqNotifyNewClass(TNode t) {
   }
   // this can be called very early, during initialization
   if (!getLogicInfo().isLocked() || getLogicInfo().isQuantified()) {
-    ((InstantiatorTheoryUf*) getInstantiator())->newEqClass(t);
+    //getQuantifiersEngine()->addTermToDatabase( t );
   }
 }
 
 void TheoryUF::eqNotifyPreMerge(TNode t1, TNode t2) {
   if (getLogicInfo().isQuantified()) {
-    ((InstantiatorTheoryUf*) getInstantiator())->merge(t1, t2);
+    getQuantifiersEngine()->getEfficientEMatcher()->merge( t1, t2 );
   }
 }
 
@@ -499,9 +501,6 @@ void TheoryUF::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
   if (d_thss != NULL) {
     d_thss->assertDisequal(t1, t2, reason);
   }
-  if (getLogicInfo().isQuantified()) {
-    ((InstantiatorTheoryUf*) getInstantiator())->assertDisequal(t1, t2, reason);
-  }
 }
 
 Node TheoryUF::ppRewrite(TNode node) {
diff --git a/src/theory/uf/theory_uf_instantiator.cpp b/src/theory/uf/theory_uf_instantiator.cpp
index e45842481..9ae6bbd37 100644
--- a/src/theory/uf/theory_uf_instantiator.cpp
+++ b/src/theory/uf/theory_uf_instantiator.cpp
@@ -41,6 +41,7 @@ Instantiator( c, qe, th )
     //if( options::cbqi() ){
     //  addInstStrategy( new InstStrategyCheckCESolved( this, qe ) );
     //}
+    //these are the instantiation strategies for basic E-matching
     if( options::userPatternsQuant() ){
       d_isup = new InstStrategyUserPatterns( this, qe );
       addInstStrategy( d_isup );
@@ -69,7 +70,7 @@ void InstantiatorTheoryUf::assertNode( Node assertion )
 {
   Debug("quant-uf-assert") << "InstantiatorTheoryUf::check: " << assertion << std::endl;
   //preRegisterTerm( assertion );
-  d_quantEngine->addTermToDatabase( assertion );
+  //INST_ELIM_TRY//d_quantEngine->addTermToDatabase( assertion );
   if( options::cbqi() ){
     if( assertion.hasAttribute(InstConstantAttribute()) ){
       setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) );
@@ -150,52 +151,6 @@ void InstantiatorTheoryUf::getEquivalenceClass( Node a, std::vector< Node >& eqc
   }
 }
 
-InstantiatorTheoryUf::Statistics::Statistics():
-  //d_instantiations("InstantiatorTheoryUf::Total_Instantiations", 0),
-  d_instantiations_ce_solved("InstantiatorTheoryUf::Instantiations_CE-Solved", 0),
-  d_instantiations_e_induced("InstantiatorTheoryUf::Instantiations_E-Induced", 0),
-  d_instantiations_user_pattern("InstantiatorTheoryUf::Instantiations_User_Pattern", 0),
-  d_instantiations_guess("InstantiatorTheoryUf::Instantiations_Free_Var", 0),
-  d_instantiations_auto_gen("InstantiatorTheoryUf::Instantiations_Auto_Gen", 0),
-  d_instantiations_auto_gen_min("InstantiatorTheoryUf::Instantiations_Auto_Gen_Min", 0),
-  d_splits("InstantiatorTheoryUf::Total_Splits", 0)
-{
-  //StatisticsRegistry::registerStat(&d_instantiations);
-  StatisticsRegistry::registerStat(&d_instantiations_ce_solved);
-  StatisticsRegistry::registerStat(&d_instantiations_e_induced);
-  StatisticsRegistry::registerStat(&d_instantiations_user_pattern );
-  StatisticsRegistry::registerStat(&d_instantiations_guess );
-  StatisticsRegistry::registerStat(&d_instantiations_auto_gen );
-  StatisticsRegistry::registerStat(&d_instantiations_auto_gen_min );
-  StatisticsRegistry::registerStat(&d_splits);
-}
-
-InstantiatorTheoryUf::Statistics::~Statistics(){
-  //StatisticsRegistry::unregisterStat(&d_instantiations);
-  StatisticsRegistry::unregisterStat(&d_instantiations_ce_solved);
-  StatisticsRegistry::unregisterStat(&d_instantiations_e_induced);
-  StatisticsRegistry::unregisterStat(&d_instantiations_user_pattern );
-  StatisticsRegistry::unregisterStat(&d_instantiations_guess );
-  StatisticsRegistry::unregisterStat(&d_instantiations_auto_gen );
-  StatisticsRegistry::unregisterStat(&d_instantiations_auto_gen_min );
-  StatisticsRegistry::unregisterStat(&d_splits);
-}
-
-/** new node */
-void InstantiatorTheoryUf::newEqClass( TNode n ){
-  d_quantEngine->addTermToDatabase( n );
-}
-
-/** merge */
-void InstantiatorTheoryUf::merge( TNode a, TNode b ){
-  d_quantEngine->getEfficientEMatcher()->merge( a, b );
-}
-
-/** assert terms are disequal */
-void InstantiatorTheoryUf::assertDisequal( TNode a, TNode b, TNode reason ){
-
-}
-
 void InstantiatorTheoryUf::outputEqClass( const char* c, Node n ){
   if( ((TheoryUF*)d_th)->d_equalityEngine.hasTerm( n ) ){
     eq::EqClassIterator eqc_iter( getRepresentative( n ),
diff --git a/src/theory/uf/theory_uf_instantiator.h b/src/theory/uf/theory_uf_instantiator.h
index b5a3aa765..fe34c9487 100644
--- a/src/theory/uf/theory_uf_instantiator.h
+++ b/src/theory/uf/theory_uf_instantiator.h
@@ -40,15 +40,6 @@ namespace quantifiers{
 namespace uf {
 
 class InstantiatorTheoryUf : public Instantiator{
-  friend class ::CVC4::theory::inst::InstMatchGenerator;
-  friend class ::CVC4::theory::quantifiers::TermDb;
-protected:
-  typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap;
-  typedef context::CDHashMap<Node, int, NodeHashFunction> IntMap;
-  typedef context::CDChunkList<Node> NodeList;
-  typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeLists;
-  /** map to representatives used */
-  //std::map< Node, Node > d_ground_reps;
 protected:
   /** instantiation strategies */
   InstStrategyUserPatterns* d_isup;
@@ -71,25 +62,6 @@ private:
   /** calculate matches for quantifier f at effort */
   int process( Node f, Theory::Effort effort, int e );
 public:
-  /** statistics class */
-  class Statistics {
-  public:
-    //IntStat d_instantiations;
-    IntStat d_instantiations_ce_solved;
-    IntStat d_instantiations_e_induced;
-    IntStat d_instantiations_user_pattern;
-    IntStat d_instantiations_guess;
-    IntStat d_instantiations_auto_gen;
-    IntStat d_instantiations_auto_gen_min;
-    IntStat d_splits;
-    Statistics();
-    ~Statistics();
-  };
-  Statistics d_statistics;
-public:
-  /** the base match */
-  std::map< Node, InstMatch > d_baseMatch;
-public:
   /** general queries about equality */
   bool hasTerm( Node a );
   bool areEqual( Node a, Node b );
@@ -101,34 +73,12 @@ public:
   /** general creators of candidate generators */
   rrinst::CandidateGenerator* getRRCanGenClasses();
   rrinst::CandidateGenerator* getRRCanGenClass();
-  /** new node */
-  void newEqClass( TNode n );
-  /** merge */
-  void merge( TNode a, TNode b );
-  /** assert terms are disequal */
-  void assertDisequal( TNode a, TNode b, TNode reason );
 public:
   /** output eq class */
   void outputEqClass( const char* c, Node n );
 };/* class InstantiatorTheoryUf */
 
-/** equality query object using instantiator theory uf */
-class EqualityQueryInstantiatorTheoryUf : public EqualityQuery
-{
-private:
-  /** pointer to instantiator uf class */
-  InstantiatorTheoryUf* d_ith;
-public:
-  EqualityQueryInstantiatorTheoryUf( InstantiatorTheoryUf* ith ) : d_ith( ith ){}
-  ~EqualityQueryInstantiatorTheoryUf(){}
-  /** general queries about equality */
-  bool hasTerm( Node a ) { return d_ith->hasTerm( a ); }
-  Node getRepresentative( Node a ) { return d_ith->getRepresentative( a ); }
-  bool areEqual( Node a, Node b ) { return d_ith->areEqual( a, b ); }
-  bool areDisequal( Node a, Node b ) { return d_ith->areDisequal( a, b ); }
-  eq::EqualityEngine* getEngine() { return d_ith->getEqualityEngine(); }
-  void getEquivalenceClass( Node a, std::vector< Node >& eqc ) { d_ith->getEquivalenceClass( a, eqc ); }
-}; /* EqualityQueryInstantiatorTheoryUf */
+
 
 }
 }/* CVC4::theory namespace */