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, 9 insertions, 2 deletions

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index f55c7c258..449f4adc3 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -450,6 +450,13 @@ public:
   }
 
   /**
+   * Get a pointer to the underlying user context.
+   */
+  inline context::Context* getUserContext() const {
+    return d_userContext;
+  }
+
+  /**
    * Get a pointer to the underlying quantifiers engine.
    */
   theory::QuantifiersEngine* getQuantifiersEngine() const {
@@ -677,8 +684,8 @@ public:
   }
 
   /** Get the theory for id */
-  theory::Theory* getTheory(int id) {
-    return d_theoryTable[id];
+  theory::Theory* getTheory(theory::TheoryId theoryId) {
+    return d_theoryTable[theoryId];
   }
 
   /**