1 files changed, 11 insertions, 2 deletions
diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h
index a9a2f9b46..f85803617 100644
--- a/src/theory/quantifiers/rewrite_engine.h
+++ b/src/theory/quantifiers/rewrite_engine.h
@@ -29,19 +29,28 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+class QuantInfo;
+
 class RewriteEngine : public QuantifiersModule
 {
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
   typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
   std::vector< Node > d_rr_quant;
-  std::map< Node, Node > d_rr_guard;
+  std::vector< Node > d_priority_order;
+  std::map< Node, Node > d_rr;
   Node d_true;
   /** explicitly provided patterns */
   std::map< Node, std::vector< inst::Trigger* > > d_rr_triggers;
+  /** get the quantifer info object */
+  std::map< Node, Node > d_qinfo_n;
+  std::map< Node, QuantInfo > d_qinfo;
   double getPriority( Node f );
+  bool d_needsSort;
+  std::map< Node, std::map< Node, Node > > d_inst_const_node;
+  Node getInstConstNode( Node n, Node q );
 private:
-  int checkRewriteRule( Node f );
+  int checkRewriteRule( Node f, Theory::Effort e );
 public:
   RewriteEngine( context::Context* c, QuantifiersEngine* qe );