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

diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 517786400..1e42abd22 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -30,10 +30,11 @@
 #include <map>
 
 namespace CVC4 {
+class TheoryEngine;
+
 namespace theory {
 namespace quantifiers {
 
-class TheoryEngine;
 class ModelEngine;
 class InstantiationEngine;