Fixes for quantifiers + incremental (#2009)

1 files changed, 21 insertions, 6 deletions

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 456a268da..70a4ede0c 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -173,6 +173,8 @@ private:
  private:
   /** list of all quantifiers seen */
   std::map< Node, bool > d_quants;
+  /** quantifiers pre-registered */
+  NodeSet d_quants_prereg;
   /** quantifiers reduced */
   BoolMap d_quants_red;
   std::map< Node, Node > d_quants_red_lem;
@@ -277,8 +279,12 @@ public:
   void check( Theory::Effort e );
   /** notify that theories were combined */
   void notifyCombineTheories();
-  /** register quantifier */
-  bool registerQuantifier( Node f );
+  /** preRegister quantifier
+   *
+   * This function is called after registerQuantifier for quantified formulas
+   * that are pre-registered to the quantifiers theory.
+   */
+  void preRegisterQuantifier(Node q);
   /** register quantifier */
   void registerPattern( std::vector<Node> & pattern);
   /** assert universal quantifier */
@@ -288,10 +294,19 @@ public:
   /** get next decision request */
   Node getNextDecisionRequest( unsigned& priority );
 private:
-  /** reduceQuantifier, return true if reduced */
-  bool reduceQuantifier( Node q );
-  /** flush lemmas */
-  void flushLemmas();
+ /** (context-indepentent) register quantifier internal
+  *
+  * This is called when a quantified formula q is pre-registered to the
+  * quantifiers theory, and updates the modules in this class with
+  * context-independent information about how to handle q. This includes basic
+  * information such as which module owns q.
+  */
+ void registerQuantifierInternal(Node q);
+ /** reduceQuantifier, return true if reduced */
+ bool reduceQuantifier(Node q);
+ /** flush lemmas */
+ void flushLemmas();
+
 public:
   /** add lemma lem */
   bool addLemma( Node lem, bool doCache = true, bool doRewrite = true );