Fixes for quantifiers + incremental (#2009)

2 files changed, 36 insertions, 28 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;
 };