diff options
Diffstat (limited to 'src/smt/quant_elim_solver.cpp')
-rw-r--r-- | src/smt/quant_elim_solver.cpp | 28 |
1 files changed, 24 insertions, 4 deletions
diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp index 38fd57790..59e9dfc9e 100644 --- a/src/smt/quant_elim_solver.cpp +++ b/src/smt/quant_elim_solver.cpp @@ -14,6 +14,7 @@ #include "smt/quant_elim_solver.h" +#include "expr/subs.h" #include "smt/smt_solver.h" #include "theory/quantifiers/extended_rewrite.h" #include "theory/rewriter.h" @@ -33,7 +34,7 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, Node q, bool doFull) { - Trace("smt-qe") << "Do quantifier elimination " << q << std::endl; + Trace("smt-qe") << "QuantElimSolver: get qe : " << q << std::endl; if (q.getKind() != EXISTS && q.getKind() != FORALL) { throw ModalException( @@ -73,6 +74,10 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, // failed, return original return q; } + // must use original quantified formula to compute QE, which ensures that + // e.g. term formula removal is not run on the body. Notice that we assume + // that the (single) quantified formula is preprocessed, rewritten + // version of the input quantified formula q. std::vector<Node> inst_qs; te->getInstantiatedQuantifiedFormulas(inst_qs); Assert(inst_qs.size() <= 1); @@ -81,9 +86,24 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, { Node topq = inst_qs[0]; Assert(topq.getKind() == FORALL); - Trace("smt-qe") << "Get qe for " << topq << std::endl; - ret = te->getInstantiatedConjunction(topq); - Trace("smt-qe") << "Returned : " << ret << std::endl; + Trace("smt-qe") << "Get qe based on preprocessed quantified formula " + << topq << std::endl; + std::vector<std::vector<Node>> insts; + te->getInstantiationTermVectors(topq, insts); + std::vector<Node> vars(ne[0].begin(), ne[0].end()); + std::vector<Node> conjs; + // apply the instantiation on the original body + for (const std::vector<Node>& inst : insts) + { + // note we do not convert to witness form here, since we could be + // an internal subsolver + Subs s; + s.add(vars, inst); + Node c = s.apply(ne[1].negate()); + conjs.push_back(c); + } + ret = nm->mkAnd(conjs); + Trace("smt-qe") << "QuantElimSolver returned : " << ret << std::endl; if (q.getKind() == EXISTS) { ret = Rewriter::rewrite(ret.negate()); |