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.

1 files changed, 10 insertions, 0 deletions

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 7d003bf25..0cf7a8774 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -52,6 +52,10 @@ class InstStrategy;
 class QuantifiersEngine;
 class TheoryModel;
 
+namespace rrinst{
+class CandidateGenerator;
+}
+
 /**
  * Information about an assertion for the theories.
  */
@@ -834,6 +838,12 @@ public:
   virtual bool areDisequal( Node a, Node b ) { return false; }
   virtual Node getRepresentative( Node a ) { return a; }
   virtual Node getInternalRepresentative( Node a ) { return getRepresentative( a ); }
+public:
+  /** A Creator of CandidateGenerator for classes (one element in each
+      equivalence class) and class (every element of one equivalence
+      class) */
+  virtual rrinst::CandidateGenerator* getRRCanGenClasses(){ return NULL; };
+  virtual rrinst::CandidateGenerator* getRRCanGenClass(){ return NULL; };
 };/* class Instantiator */
 
 inline Assertion Theory::get() {