From 135171f4a10ef709b8982d79f2e477c12b29f64d Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 1 Sep 2016 10:20:48 -0500
Subject: [PATCH] Cleanup quantifier elimination in smt engine.

---
 src/smt/smt_engine.cpp                        | 75 +------------------
 src/theory/quantifiers/inst_strategy_cbqi.cpp |  2 +-
 src/theory/quantifiers_engine.cpp             |  1 +
 3 files changed, 5 insertions(+), 73 deletions(-)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 82d3139b2..76a1e72c3 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -974,44 +974,6 @@ public:
     return d_managedReplayLog.getReplayLog();
   }
 
-  Node replaceQuantifiersWithInstantiations( Node n, std::map< Node, std::vector< Node > >& insts, std::map< Node, Node >& visited ){
-    std::map< Node, Node >::iterator itv = visited.find( n );
-    if( itv!=visited.end() ){
-      return itv->second;
-    }else{
-      Node ret = n;
-      if( n.getKind()==kind::FORALL ){
-        std::map< Node, std::vector< Node > >::iterator it = insts.find( n );
-        if( it==insts.end() ){
-          Trace("smt-qe-debug") << "* " << n << " has no instances" << std::endl;
-          ret = NodeManager::currentNM()->mkConst(true);
-        }else{
-          Trace("smt-qe-debug") << "* " << n << " has " << it->second.size() << " instances" << std::endl;
-          Node reti = it->second.empty() ? NodeManager::currentNM()->mkConst(true) : ( it->second.size()==1 ? it->second[0] : NodeManager::currentNM()->mkNode( kind::AND, it->second ) );
-          Trace("smt-qe-debug") << "   return : " << ret << std::endl;
-          //recursive (for nested quantification)
-          ret = replaceQuantifiersWithInstantiations( reti, insts, visited );
-        }
-      }else if( n.getNumChildren()>0 ){
-        bool childChanged = false;
-        std::vector< Node > children;
-        if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
-          children.push_back( n.getOperator() );
-        }
-        for( unsigned i=0; i<n.getNumChildren(); i++ ){
-          Node r = replaceQuantifiersWithInstantiations( n[i], insts, visited );
-          children.push_back( r );
-          childChanged = childChanged || r!=n[i];
-        }
-        if( childChanged ){
-          ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
-        }
-      }
-      visited[n] = ret;
-      return ret;
-    }
-  }
-
 };/* class SmtEnginePrivate */
 
 }/* namespace CVC4::smt */
@@ -5139,41 +5101,10 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict)
       InternalError(ss.str().c_str());
     }
     
- #if 1
-    //get the instantiations for all quantified formulas
-    std::map< Node, std::vector< Node > > insts;
-    d_theoryEngine->getInstantiations( insts );
-    //find the quantified formula that corresponds to the input
-    Node top_q;
-    for( std::map< Node, std::vector< Node > >::iterator it = insts.begin(); it != insts.end(); ++it ){
-      Trace("smt-qe-debug") << "* quantifier " << it->first << " had " << it->second.size() << " instances." << std::endl;
-      if( it->first.getNumChildren()==3 && it->first[2]==n_attr ){
-        top_q = it->first;
-      }
-    }
-    std::map< Node, Node > visited;
-    Node ret_n;
-    if( top_q.isNull() ){
-      //no instances needed
-      ret_n = NodeManager::currentNM()->mkConst(true);
-      visited[top_q] = ret_n;
-    }else{
-      //replace by a conjunction of instances
-      ret_n = d_private->replaceQuantifiersWithInstantiations( top_q, insts, visited );
-    }
-
-    //ensure all instantiations were accounted for
-    for( std::map< Node, std::vector< Node > >::iterator it = insts.begin(); it != insts.end(); ++it ){
-      if( !it->second.empty() && visited.find( it->first )==visited.end() ){
-        stringstream ss;
-        ss << "While performing quantifier elimination, processed a quantified formula : " << it->first;
-        ss << " that was not related to the query.  Try option --simplification=none.";
-        InternalError(ss.str().c_str());
-      }
-    }   
-#else
+    Node top_q = Rewriter::rewrite( nn_e ).negate();
+    Assert( top_q.getKind()==kind::FORALL );
+    Trace("smt-qe") << "Get qe for " << top_q << std::endl;
     Node ret_n = d_theoryEngine->getInstantiatedConjunction( top_q );
-#endif
     Trace("smt-qe") << "Returned : " << ret_n << std::endl;
     ret_n = Rewriter::rewrite( ret_n.negate() );
     return ret_n.toExpr();
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index f3061f575..71c0858bf 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -370,7 +370,7 @@ Node InstStrategyCbqi::doNestedQENode( Node q, Node ceq, Node n, std::vector< No
   // there is a nested quantified formula (forall y. nq[y,x]) such that 
   //    q is (forall y. nq[y,t]) for ground terms t,
   //    ceq is (forall y. nq[y,e]) for CE variables e.
-  // we call this function when we know (exists e. ceq[e,k]) is equivalent to quantifier-free formula C[k].
+  // we call this function when we know (forall y. nq[y,e]) is equivalent to quantifier-free formula C[e].
   // in this case, q is equivalent to the quantifier-free formula C[t].
   if( d_nested_qe.find( ceq )==d_nested_qe.end() ){
     d_nested_qe[ceq] = d_quantEngine->getInstantiatedConjunction( ceq );
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 57eb375d3..c412b2c3a 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -1464,6 +1464,7 @@ void QuantifiersEngine::getInstantiations( Node q, std::vector< Node >& insts  )
 }
 
 Node QuantifiersEngine::getInstantiatedConjunction( Node q ) {
+  Assert( q.getKind()==FORALL );
   std::vector< Node > insts;
   getInstantiations( q, insts );
   if( insts.empty() ){
-- 
2.30.2