From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Mon, 7 Aug 2017 08:14:07 +0000 (-0500)
Subject: Make quantifier elimination more robust to preprocessing.
X-Git-Tag: cvc5-1.0.0~5694
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=53d881246fba60c630d7b15ad2ea1acf3e0ce335;p=cvc5.git

Make quantifier elimination more robust to preprocessing.
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 704303826..20209fdcb 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -5246,13 +5246,21 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict)
       ss << "While performing quantifier elimination, unexpected result : " << r << " for query.";
       InternalError(ss.str().c_str());
     }
-
-    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 );
-    Trace("smt-qe") << "Returned : " << ret_n << std::endl;
-    ret_n = Rewriter::rewrite( ret_n.negate() );
+    std::vector< Node > inst_qs;
+    d_theoryEngine->getInstantiatedQuantifiedFormulas( inst_qs );
+    Assert( inst_qs.size()<=1 );
+    Node ret_n;
+    if( inst_qs.size()==1 ){
+      Node top_q = inst_qs[0]; 
+      //Node top_q = Rewriter::rewrite( nn_e ).negate();
+      Assert( top_q.getKind()==kind::FORALL );
+      Trace("smt-qe") << "Get qe for " << top_q << std::endl;
+      ret_n = d_theoryEngine->getInstantiatedConjunction( top_q );
+      Trace("smt-qe") << "Returned : " << ret_n << std::endl;
+      ret_n = Rewriter::rewrite( ret_n.negate() );
+    }else{
+      ret_n = NodeManager::currentNM()->mkConst(false);
+    }
     return ret_n.toExpr();
   }else {
     return NodeManager::currentNM()->mkConst(true).toExpr();