diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-30 10:05:29 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-30 15:05:29 +0000 |
commit | 4948485775b04d95dbf69eee311bf452d0bfac3d (patch) | |
tree | 536a017cc5a8cce04cd9863c8fb0671cc9f7f5e1 /src/smt | |
parent | 05db3e9511c1c485b27a8e3467bcae74659dfd9a (diff) |
Implement simple tracking of instantiation lemmas (#6077)
We require tracking of instantiation lemmas for quantifier elimination. Recently, this feature was removed in favor of reconstructing instantiations via substitutions. This does not quite work if instantiation lemmas have more complex post-processing, e.g. virtual term substitution.
This PR reimplements a much simpler form of instantiation tracking that simply adds instantiation bodies to a vector, per quantified formula. It uses this vector for quantifier elimination.
Fixes #5899.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/quant_elim_solver.cpp | 20 |
1 files changed, 5 insertions, 15 deletions
diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp index 9a0178cfe..ba11319d3 100644 --- a/src/smt/quant_elim_solver.cpp +++ b/src/smt/quant_elim_solver.cpp @@ -99,21 +99,11 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, Assert(topq.getKind() == FORALL); Trace("smt-qe") << "Get qe based on preprocessed quantified formula " << topq << std::endl; - std::vector<std::vector<Node>> insts; - qe->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); + std::vector<Node> insts; + qe->getInstantiations(topq, insts); + // note we do not convert to witness form here, since we could be + // an internal subsolver (SmtEngine::isInternalSubsolver). + ret = nm->mkAnd(insts); Trace("smt-qe") << "QuantElimSolver returned : " << ret << std::endl; if (q.getKind() == EXISTS) { |