From 53d881246fba60c630d7b15ad2ea1acf3e0ce335 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 7 Aug 2017 03:14:07 -0500 Subject: [PATCH] Make quantifier elimination more robust to preprocessing. --- src/smt/smt_engine.cpp | 22 +++++++++++++++------- 1 file changed, 15 insertions(+), 7 deletions(-) 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(); -- 2.30.2