17 files changed, 78 insertions, 74 deletions
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
index 4b79c4e79..678d87156 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
@@ -344,39 +344,46 @@ Node InstStrategyCbqi::getIdMarkedQuantNode( Node n, std::map< Node, Node >& vis
   }
 }
 
-void InstStrategyCbqi::preRegisterQuantifier( Node q ) {
+void InstStrategyCbqi::checkOwnership(Node q)
+{
   if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){
     if (d_do_cbqi[q] == CEG_HANDLED)
     {
       //take full ownership of the quantified formula
       d_quantEngine->setOwner( q, this );
-      
-      //mark all nested quantifiers with id
-      if( options::cbqiNestedQE() ){
-        std::map< Node, Node > visited;
-        Node mq = getIdMarkedQuantNode( q[1], visited );
-        if( mq!=q[1] ){
-          // do not do cbqi, we are reducing this quantified formula to a marked
-          // one
-          d_do_cbqi[q] = CEG_UNHANDLED;
-          //instead do reduction
-          std::vector< Node > qqc;
-          qqc.push_back( q[0] );
-          qqc.push_back( mq );
-          if( q.getNumChildren()==3 ){
-            qqc.push_back( q[2] );
-          }
-          Node qq = NodeManager::currentNM()->mkNode( FORALL, qqc );
-          Node mlem = NodeManager::currentNM()->mkNode( IMPLIES, q, qq );
-          Trace("cbqi-lemma") << "Mark quant id lemma : " << mlem << std::endl;
-          d_quantEngine->getOutputChannel().lemma( mlem );
-        }
-      }
     }
   }
 }
 
-void InstStrategyCbqi::registerQuantifier( Node q ) {
+void InstStrategyCbqi::preRegisterQuantifier(Node q)
+{
+  // mark all nested quantifiers with id
+  if (options::cbqiNestedQE())
+  {
+    if( d_quantEngine->getOwner(q)==this )
+    {
+      std::map<Node, Node> visited;
+      Node mq = getIdMarkedQuantNode(q[1], visited);
+      if (mq != q[1])
+      {
+        // do not do cbqi, we are reducing this quantified formula to a marked
+        // one
+        d_do_cbqi[q] = CEG_UNHANDLED;
+        // instead do reduction
+        std::vector<Node> qqc;
+        qqc.push_back(q[0]);
+        qqc.push_back(mq);
+        if (q.getNumChildren() == 3)
+        {
+          qqc.push_back(q[2]);
+        }
+        Node qq = NodeManager::currentNM()->mkNode(FORALL, qqc);
+        Node mlem = NodeManager::currentNM()->mkNode(IMPLIES, q, qq);
+        Trace("cbqi-lemma") << "Mark quant id lemma : " << mlem << std::endl;
+        d_quantEngine->addLemma(mlem);
+      }
+    }
+  }
   if( doCbqi( q ) ){
     if( registerCbqiLemma( q ) ){
       Trace("cbqi") << "Registered cbqi lemma for quantifier : " << q << std::endl;
@@ -673,7 +680,8 @@ CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) {
   }
 }
 
-void InstStrategyCegqi::registerQuantifier( Node q ) {
+void InstStrategyCegqi::preRegisterQuantifier(Node q)
+{
   if( doCbqi( q ) ){
     // get the instantiator  
     if( options::cbqiPreRegInst() ){
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h
index 5a4db0e53..3445c3f9f 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h
@@ -103,8 +103,8 @@ class InstStrategyCbqi : public QuantifiersModule {
   void check(Theory::Effort e, QEffort quant_e) override;
   bool checkComplete() override;
   bool checkCompleteFor(Node q) override;
+  void checkOwnership(Node q) override;
   void preRegisterQuantifier(Node q) override;
-  void registerQuantifier(Node q) override;
   /** get next decision request */
   Node getNextDecisionRequest(unsigned& priority) override;
 };
@@ -147,8 +147,8 @@ class InstStrategyCegqi : public InstStrategyCbqi {
 
   //get instantiator for quantifier
   CegInstantiator * getInstantiator( Node q );
-  //register quantifier
-  void registerQuantifier(Node q) override;
+  /** pre-register quantifier */
+  void preRegisterQuantifier(Node q) override;
   //presolve
   void presolve() override;
 };
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 404f64471..807a7a58c 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -923,14 +923,6 @@ unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, in
   return addedLemmas;
 }
 
-void ConjectureGenerator::registerQuantifier( Node q ) {
-
-}
-
-void ConjectureGenerator::assertNode( Node n ) {
-
-}
-
 bool ConjectureGenerator::considerTermCanon( Node ln, bool genRelevant ){
   if( !ln.isNull() ){
     //do not consider if it is non-canonical, and either:
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index 2db175fae..8a6339a85 100644
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -428,9 +428,6 @@ public:
   void reset_round(Theory::Effort e) override;
   /* Call during quantifier engine's check */
   void check(Theory::Effort e, QEffort quant_e) override;
-  /* Called for new quantifiers */
-  void registerQuantifier(Node q) override;
-  void assertNode(Node n) override;
   /** Identify this module (for debugging, dynamic configuration, etc..) */
   std::string identify() const override { return "ConjectureGenerator"; }
   // options
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index 184add8c3..bd95b316d 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -157,7 +157,8 @@ bool InstantiationEngine::checkCompleteFor( Node q ) {
   return false;
 }
 
-void InstantiationEngine::preRegisterQuantifier( Node q ) {
+void InstantiationEngine::checkOwnership(Node q)
+{
   if( options::strictTriggers() && q.getNumChildren()==3 ){
     //if strict triggers, take ownership of this quantified formula
     bool hasPat = false;
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h
index 32ddb19ed..e4cb986da 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.h
+++ b/src/theory/quantifiers/ematching/instantiation_engine.h
@@ -81,7 +81,7 @@ class InstantiationEngine : public QuantifiersModule {
   void reset_round(Theory::Effort e) override;
   void check(Theory::Effort e, QEffort quant_e) override;
   bool checkCompleteFor(Node q) override;
-  void preRegisterQuantifier(Node q) override;
+  void checkOwnership(Node q) override;
   void registerQuantifier(Node q) override;
   Node explain(TNode n) { return Node::null(); }
   /** add user pattern */
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index d96fb4e05..b493d6a0c 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -384,10 +384,11 @@ void BoundedIntegers::setBoundedVar( Node q, Node v, unsigned bound_type ) {
   Trace("bound-int-var") << "Bound variable #" << d_set_nums[q][v] << " : " << v << std::endl; 
 }
 
-void BoundedIntegers::preRegisterQuantifier( Node f ) {
+void BoundedIntegers::checkOwnership(Node f)
+{
   //this needs to be done at preregister since it affects e.g. QuantDSplit's preregister
-  Trace("bound-int") << "preRegister quantifier " << f << std::endl;
-  
+  Trace("bound-int") << "check ownership quantifier " << f << std::endl;
+
   bool success;
   do{
     std::map< Node, unsigned > bound_lit_type_map;
@@ -546,10 +547,6 @@ void BoundedIntegers::preRegisterQuantifier( Node f ) {
   }
 }
 
-void BoundedIntegers::registerQuantifier( Node q ) {
-
-}
-
 void BoundedIntegers::assertNode( Node n ) {
   Trace("bound-int-assert") << "Assert " << n << std::endl;
   Node nlit = n.getKind()==NOT ? n[0] : n;
diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h
index 3e990067a..93b6436d5 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.h
+++ b/src/theory/quantifiers/fmf/bounded_integers.h
@@ -146,8 +146,7 @@ public:
   void presolve() override;
   bool needsCheck(Theory::Effort e) override;
   void check(Theory::Effort e, QEffort quant_e) override;
-  void registerQuantifier(Node q) override;
-  void preRegisterQuantifier(Node q) override;
+  void checkOwnership(Node q) override;
   void assertNode(Node n) override;
   Node getNextDecisionRequest(unsigned& priority) override;
   bool isBoundVar( Node q, Node v ) { return std::find( d_set[q].begin(), d_set[q].end(), v )!=d_set[q].end(); }
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp
index 54689b32a..743e7ccc8 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.cpp
+++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp
@@ -295,7 +295,6 @@ bool InstStrategyEnum::process(Node f, bool fullEffort)
   return false;
 }
 
-void InstStrategyEnum::registerQuantifier(Node q) {}
 } /* CVC4::theory::quantifiers namespace */
 } /* CVC4::theory namespace */
 } /* CVC4 namespace */
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h
index cf97518fc..51c0c1d0c 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.h
+++ b/src/theory/quantifiers/inst_strategy_enumerative.h
@@ -72,8 +72,6 @@ class InstStrategyEnum : public QuantifiersModule
    * quantified formulas via calls to process(...)
    */
   void check(Theory::Effort e, QEffort quant_e) override;
-  /** Register quantifier. */
-  void registerQuantifier(Node q) override;
   /** Identify. */
   std::string identify() const override
   {
diff --git a/src/theory/quantifiers/local_theory_ext.cpp b/src/theory/quantifiers/local_theory_ext.cpp
index 375754b26..c76d97255 100644
--- a/src/theory/quantifiers/local_theory_ext.cpp
+++ b/src/theory/quantifiers/local_theory_ext.cpp
@@ -32,7 +32,8 @@ QuantifiersModule( qe ), d_wasInvoked( false ), d_needsCheck( false ){
 }
 
 /** add quantifier */
-void LtePartialInst::preRegisterQuantifier( Node q ) {
+void LtePartialInst::checkOwnership(Node q)
+{
   if( !q.getAttribute(LtePartialInstAttribute()) ){
     if( d_do_inst.find( q )!=d_do_inst.end() ){
       if( d_do_inst[q] ){
diff --git a/src/theory/quantifiers/local_theory_ext.h b/src/theory/quantifiers/local_theory_ext.h
index 76a781e1c..2390eb40c 100644
--- a/src/theory/quantifiers/local_theory_ext.h
+++ b/src/theory/quantifiers/local_theory_ext.h
@@ -56,7 +56,7 @@ private:
 public:
   LtePartialInst( QuantifiersEngine * qe, context::Context* c );
   /** determine whether this quantified formula will be reduced */
-  void preRegisterQuantifier(Node q) override;
+  void checkOwnership(Node q) override;
   /** was invoked */
   bool wasInvoked() { return d_wasInvoked; }
   
@@ -64,11 +64,8 @@ public:
   bool needsCheck(Theory::Effort e) override;
   /* Call during quantifier engine's check */
   void check(Theory::Effort e, QEffort quant_e) override;
-  /* Called for new quantifiers */
-  void registerQuantifier(Node q) override {}
   /* check complete */
   bool checkComplete() override { return !d_wasInvoked; }
-  void assertNode(Node n) override {}
   /** Identify this module (for debugging, dynamic configuration, etc..) */
   std::string identify() const override { return "LtePartialInst"; }
 };
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index 68a0f30dc..da6b0a6b4 100644
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -31,8 +31,8 @@ QuantifiersModule( qe ), d_added_split( qe->getUserContext() ){
 
 }
 
-/** pre register quantifier */
-void QuantDSplit::preRegisterQuantifier( Node q ) {
+void QuantDSplit::checkOwnership(Node q)
+{
   int max_index = -1;
   int max_score = -1;
   if( q.getNumChildren()==3 ){
diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h
index 1ea57433a..94bfa0f20 100644
--- a/src/theory/quantifiers/quant_split.h
+++ b/src/theory/quantifiers/quant_split.h
@@ -34,7 +34,7 @@ private:
 public:
   QuantDSplit( QuantifiersEngine * qe, context::Context* c );
   /** determine whether this quantified formula will be reduced */
-  void preRegisterQuantifier(Node q) override;
+  void checkOwnership(Node q) override;
 
   /* whether this module needs to check this round */
   bool needsCheck(Theory::Effort e) override;
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index f3fdfa6f4..874baa482 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -108,19 +108,27 @@ class QuantifiersModule {
    * we are incomplete for other reasons.
    */
   virtual bool checkCompleteFor( Node q ) { return false; }
-  /** Pre register quantifier.
+  /** Check ownership
    *
-   * Called once for new quantified formulas that are
-   * pre-registered by the quantifiers theory.
+   * Called once for new quantified formulas that are registered by the
+   * quantifiers theory. The primary purpose of this function is to establish
+   * if this module is the owner of quantified formula q.
    */
-  virtual void preRegisterQuantifier( Node q ) { }
+  virtual void checkOwnership(Node q) {}
   /** Register quantifier
    *
+   * Called once for new quantified formulas q that are pre-registered by the
+   * quantifiers theory, after internal ownership of quantified formulas is
+   * finalized. This does context-dependent initialization of this module.
+   */
+  virtual void registerQuantifier(Node q) {}
+  /** Pre-register quantifier
+   *
    * Called once for new quantified formulas that are
    * pre-registered by the quantifiers theory, after
    * internal ownership of quantified formulas is finalized.
    */
-  virtual void registerQuantifier( Node q ) = 0;
+  virtual void preRegisterQuantifier(Node q) {}
   /** Assert node.
    *
    * Called when a quantified formula q is asserted to the quantifiers theory
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 5016bd87f..79b7d9a99 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -83,13 +83,23 @@ void TheoryQuantifiers::finishInit()
 }
 
 void TheoryQuantifiers::preRegisterTerm(TNode n) {
+  if (n.getKind() != FORALL)
+  {
+    return;
+  }
   Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() " << n << endl;
-  if( n.getKind()==FORALL ){
-    if( !options::cbqi() || options::recurseCbqi() || !TermUtil::hasInstConstAttr(n) ){
-      getQuantifiersEngine()->registerQuantifier( n );
-      Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() done " << n << endl;
-    }
+  if (options::cbqi() && !options::recurseCbqi()
+      && TermUtil::hasInstConstAttr(n))
+  {
+    Debug("quantifiers-prereg")
+        << "TheoryQuantifiers::preRegisterTerm() done, unused " << n << endl;
+    return;
   }
+  // Preregister the quantified formula.
+  // This initializes the modules used for handling n in this user context.
+  getQuantifiersEngine()->preRegisterQuantifier(n);
+  Debug("quantifiers-prereg")
+      << "TheoryQuantifiers::preRegisterTerm() done " << n << endl;
 }
 
 
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 4f0302bf3..b82dccd73 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -65,9 +65,6 @@ class TheoryQuantifiers : public Theory {
   void assertUniversal( Node n );
   void assertExistential( Node n );
   void computeCareGraph() override;
-
-  using BoolMap = context::CDHashMap<Node, bool, NodeHashFunction>;
-
   /** number of instantiations */
   int d_numInstantiations;
   int d_baseDecLevel;