Merge quantifiers2-trunk:

   - new syntax for rewrite rules
   - better rewrite rules theory
   - remove the rewriting with rewrite rules during ppRewrite temporarily
   - theory can define their own candidate generator
   - define a general candidate generator (inefficient ask to every theory)
   - split inst_match between the pattern matching used for quantifiers (inst_match.*) and
     the one used for rewrite rules (rr_inst_match.*):
      - the pattern matching is less exhaustive for quantifiers,
      - the one for rewrite rules can use efficient-e-matching.

2 files changed, 19 insertions, 1 deletions

diff --git a/src/theory/arrays/theory_arrays_instantiator.cpp b/src/theory/arrays/theory_arrays_instantiator.cpp
index 2e446c57f..ca9001fe5 100644
--- a/src/theory/arrays/theory_arrays_instantiator.cpp
+++ b/src/theory/arrays/theory_arrays_instantiator.cpp
@@ -17,6 +17,7 @@
 #include "theory/theory_engine.h"
 #include "theory/arrays/theory_arrays_instantiator.h"
 #include "theory/arrays/theory_arrays.h"
+#include "theory/uf/theory_uf_candidate_generator.h"
 
 using namespace std;
 using namespace CVC4;
@@ -83,3 +84,16 @@ Node InstantiatorTheoryArrays::getRepresentative( Node a ){
   }
 }
 
+rrinst::CandidateGenerator* InstantiatorTheoryArrays::getRRCanGenClasses(){
+  arrays::TheoryArrays* ar = static_cast<arrays::TheoryArrays *>(getTheory());
+  eq::EqualityEngine* ee =
+    static_cast<eq::EqualityEngine*>(ar->getEqualityEngine());
+  return new eq::rrinst::CandidateGeneratorTheoryEeClasses(ee);
+}
+
+rrinst::CandidateGenerator* InstantiatorTheoryArrays::getRRCanGenClass(){
+  arrays::TheoryArrays* ar = static_cast<arrays::TheoryArrays *>(getTheory());
+  eq::EqualityEngine* ee =
+    static_cast<eq::EqualityEngine*>(ar->getEqualityEngine());
+  return new eq::rrinst::CandidateGeneratorTheoryEeClass(ee);
+}
diff --git a/src/theory/arrays/theory_arrays_instantiator.h b/src/theory/arrays/theory_arrays_instantiator.h
index ade43fdb0..f711229b2 100644
--- a/src/theory/arrays/theory_arrays_instantiator.h
+++ b/src/theory/arrays/theory_arrays_instantiator.h
@@ -21,6 +21,7 @@
 #define __CVC4__INSTANTIATOR_THEORY_ARRAYS_H
 
 #include "theory/quantifiers_engine.h"
+#include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
 namespace theory {
@@ -48,10 +49,13 @@ public:
   bool areEqual( Node a, Node b );
   bool areDisequal( Node a, Node b );
   Node getRepresentative( Node a );
+  /** general creators of candidate generators */
+  rrinst::CandidateGenerator* getRRCanGenClasses();
+  rrinst::CandidateGenerator* getRRCanGenClass();
 };/* class Instantiatior */
 
 }
 }
 }
 
-#endif
\ No newline at end of file
+#endif