more major cleanup of quantifiers code, separating rewrite-rules-specific code from quantifiers-specific code

5 files changed, 26 insertions, 8 deletions

diff --git a/src/theory/rewriterules/rr_inst_match.cpp b/src/theory/rewriterules/rr_inst_match.cpp
index 572ccfad2..af4cdeb50 100644
--- a/src/theory/rewriterules/rr_inst_match.cpp
+++ b/src/theory/rewriterules/rr_inst_match.cpp
@@ -23,6 +23,7 @@
 #include "theory/rewriterules/rr_trigger.h"
 #include "theory/rewriterules/rr_inst_match_impl.h"
 #include "theory/rewriterules/rr_candidate_generator.h"
+#include "theory/quantifiers/candidate_generator.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
@@ -140,7 +141,8 @@ ApplyMatcher::ApplyMatcher( Node pat, QuantifiersEngine* qe): d_pattern(pat){
 
   //set-up d_variables, d_constants, d_childrens
   for( size_t i=0; i< d_pattern.getNumChildren(); ++i ){
-    EqualityQuery* q = qe->getEqualityQuery(d_pattern[i].getType());
+    //EqualityQuery* q = qe->getEqualityQuery(d_pattern[i].getType());
+    EqualityQuery* q = qe->getEqualityQuery();
     Assert( q != NULL );
     if( d_pattern[i].hasAttribute(InstConstantAttribute()) ){
       if( d_pattern[i].getKind()==INST_CONSTANT ){
@@ -327,7 +329,8 @@ class VarMatcher: public Matcher{
   EqualityQuery* d_q;
 public:
   VarMatcher(Node var, QuantifiersEngine* qe): d_var(var), d_binded(false){
-    d_q = qe->getEqualityQuery(var.getType());
+    //d_q = qe->getEqualityQuery(var.getType());
+    d_q = qe->getEqualityQuery();
   }
   void resetInstantiationRound( QuantifiersEngine* qe ){};
   bool reset( TNode n, InstMatch& m, QuantifiersEngine* qe ){
@@ -600,9 +603,9 @@ private:
 public:
   void mkCandidateGenerator(){
     if(classes)
-      d_cg = d_qe->getRRCanGenClasses();
+      d_cg = new GenericCandidateGeneratorClasses(d_qe);
     else
-     d_cg = d_qe->getRRCanGenClass();
+      d_cg = new GenericCandidateGeneratorClass(d_qe);
   }
 
   GenericCandidateGeneratorClasses(QuantifiersEngine* qe):
diff --git a/src/theory/rewriterules/rr_inst_match.h b/src/theory/rewriterules/rr_inst_match.h
index 14873b501..63728a95b 100644
--- a/src/theory/rewriterules/rr_inst_match.h
+++ b/src/theory/rewriterules/rr_inst_match.h
@@ -30,6 +30,7 @@
 #include "context/cdlist.h"
 
 #include "theory/quantifiers/inst_match.h"
+#include "theory/quantifiers/term_database.h"
 #include "expr/node_manager.h"
 #include "expr/node_builder.h"
 
@@ -55,7 +56,7 @@ public:
         Node cand = cg->getNextCandidate();
         //.......
       }while( !cand.isNull() );
-      
+
       eqc is the equivalence class you are searching in
   */
   virtual void reset( TNode eqc ) = 0;
diff --git a/src/theory/rewriterules/rr_inst_match_impl.h b/src/theory/rewriterules/rr_inst_match_impl.h
index 43161a9e5..388d1a702 100644
--- a/src/theory/rewriterules/rr_inst_match_impl.h
+++ b/src/theory/rewriterules/rr_inst_match_impl.h
@@ -31,7 +31,7 @@ template<bool modEq>
 InstMatchTrie2Gen<modEq>::InstMatchTrie2Gen(context::Context* c,  QuantifiersEngine* qe):
   d_context(c), d_mods(c) {
   d_eQ = qe->getEqualityQuery();
-  d_cG = qe->getRRCanGenClass();
+  d_cG = new GenericCandidateGeneratorClass(qe);
 };
 
 /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */
diff --git a/src/theory/rewriterules/theory_rewriterules.h b/src/theory/rewriterules/theory_rewriterules.h
index 5e06bfd0b..4a27b4559 100644
--- a/src/theory/rewriterules/theory_rewriterules.h
+++ b/src/theory/rewriterules/theory_rewriterules.h
@@ -263,6 +263,9 @@ private:
                          rewriter::Subst & pvars,
                          rewriter::Subst & vars);
 
+  //create inst variable
+  std::vector<Node> createInstVariable( std::vector<Node> & vars );
+
     /** statistics class */
   class Statistics {
   public:
diff --git a/src/theory/rewriterules/theory_rewriterules_rules.cpp b/src/theory/rewriterules/theory_rewriterules_rules.cpp
index cc01a01ff..20e5fa084 100644
--- a/src/theory/rewriterules/theory_rewriterules_rules.cpp
+++ b/src/theory/rewriterules/theory_rewriterules_rules.cpp
@@ -151,8 +151,7 @@ void TheoryRewriteRules::addRewriteRule(const Node r)
     vars.push_back(*v);
   };
   /* Instantiation version */
-  std::vector<Node> inst_constants =
-    getQuantifiersEngine()->createInstVariable(vars);
+  std::vector<Node> inst_constants = createInstVariable(vars);
   /* Body/Remove_term/Guards/Triggers */
   Node body = r[2][1];
   TNode new_terms = r[2][1];
@@ -377,6 +376,18 @@ bool TheoryRewriteRules::addRewritePattern(TNode pattern, TNode body,
 
 }
 
+std::vector<Node> TheoryRewriteRules::createInstVariable( std::vector<Node> & vars ){
+  std::vector<Node> inst_constant;
+  inst_constant.reserve(vars.size());
+  for( std::vector<Node>::const_iterator v = vars.begin();
+       v != vars.end(); ++v ){
+    //make instantiation constants
+    Node ic = NodeManager::currentNM()->mkInstConstant( (*v).getType() );
+    inst_constant.push_back( ic );
+  };
+  return inst_constant;
+}
+
 
 }/* CVC4::theory::rewriterules namespace */
 }/* CVC4::theory namespace */