From 6489cf590b441aeb5e1bdf9800c9718d06842149 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 30 Nov 2020 22:22:24 -0600 Subject: [PATCH] More fixes for quantifier elimination (#5533) Fixes #5506, fixes #5507. --- src/smt/quant_elim_solver.cpp | 14 ++++++++++++-- src/smt/quant_elim_solver.h | 13 ++++++++++++- src/smt/smt_engine.cpp | 3 ++- src/theory/quantifiers_engine.cpp | 2 ++ test/regress/CMakeLists.txt | 2 ++ .../regress1/quantifiers/issue5506-qe.smt2 | 6 ++++++ .../regress1/quantifiers/issue5507-qe.smt2 | 19 +++++++++++++++++++ 7 files changed, 55 insertions(+), 4 deletions(-) create mode 100644 test/regress/regress1/quantifiers/issue5506-qe.smt2 create mode 100644 test/regress/regress1/quantifiers/issue5507-qe.smt2 diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp index e5ecafd4a..4636cf17a 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/skolem_manager.h" #include "expr/subs.h" #include "smt/smt_solver.h" #include "theory/quantifiers/cegqi/nested_qe.h" @@ -33,7 +34,8 @@ QuantElimSolver::~QuantElimSolver() {} Node QuantElimSolver::getQuantifierElimination(Assertions& as, Node q, - bool doFull) + bool doFull, + bool isInternalSubsolver) { Trace("smt-qe") << "QuantElimSolver: get qe : " << q << std::endl; if (q.getKind() != EXISTS && q.getKind() != FORALL) @@ -41,11 +43,13 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, throw ModalException( "Expecting a quantified formula as argument to get-qe."); } + NodeManager* nm = NodeManager::currentNM(); + // ensure the body is rewritten + q = nm->mkNode(q.getKind(), q[0], Rewriter::rewrite(q[1])); // do nested quantifier elimination if necessary q = quantifiers::NestedQe::doNestedQe(q, true); Trace("smt-qe") << "QuantElimSolver: after nested quantifier elimination : " << q << std::endl; - NodeManager* nm = NodeManager::currentNM(); // tag the quantified formula with the quant-elim attribute TypeNode t = nm->booleanType(); Node n_attr = nm->mkSkolem("qe", t, "Auxiliary variable for qe attr."); @@ -121,6 +125,12 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, // do extended rewrite to minimize the size of the formula aggressively theory::quantifiers::ExtendedRewriter extr(true); ret = extr.extendedRewrite(ret); + // if we are not an internal subsolver, convert to witness form, since + // internally generated skolems should not escape + if (!isInternalSubsolver) + { + ret = SkolemManager::getWitnessForm(ret); + } return ret; } // otherwise, just true/false diff --git a/src/smt/quant_elim_solver.h b/src/smt/quant_elim_solver.h index 96ed1f73d..ca55fc618 100644 --- a/src/smt/quant_elim_solver.h +++ b/src/smt/quant_elim_solver.h @@ -79,8 +79,19 @@ class QuantElimSolver * extended command get-qe-disjunct, which can be used * for incrementally computing the result of a * quantifier elimination. + * + * @param as The assertions of the SmtEngine + * @param q The quantified formula we are eliminating quantifiers from + * @param doFull Whether we are doing full quantifier elimination on q + * @param isInternalSubsolver Whether the SmtEngine we belong to is an + * internal subsolver. If it is not, then we convert the final result to + * witness form. + * @return The result of eliminating quantifiers from q. */ - Node getQuantifierElimination(Assertions& as, Node q, bool doFull); + Node getQuantifierElimination(Assertions& as, + Node q, + bool doFull, + bool isInternalSubsolver); private: /** The SMT solver, which is used during doQuantifierElimination. */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 722f6a080..d3ba676fc 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1498,7 +1498,8 @@ Node SmtEngine::getQuantifierElimination(Node q, bool doFull, bool strict) if(!d_logic.isPure(THEORY_ARITH) && strict){ Warning() << "Unexpected logic for quantifier elimination " << d_logic << endl; } - return d_quantElimSolver->getQuantifierElimination(*d_asserts, q, doFull); + return d_quantElimSolver->getQuantifierElimination( + *d_asserts, q, doFull, d_isInternalSubsolver); } bool SmtEngine::getInterpol(const Node& conj, diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 297f11690..da9fdd022 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -336,6 +336,8 @@ bool QuantifiersEngine::getBoundElements(RepSetIterator* rsi, void QuantifiersEngine::presolve() { Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl; + d_lemmas_waiting.clear(); + d_phase_req_waiting.clear(); for( unsigned i=0; ipresolve(); } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 816202fa9..4445a28d0 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1622,6 +1622,8 @@ set(regress_1_tests regress1/quantifiers/issue5482-rtf-no-fv.smt2 regress1/quantifiers/issue5484-qe.smt2 regress1/quantifiers/issue5484b-qe.smt2 + regress1/quantifiers/issue5506-qe.smt2 + regress1/quantifiers/issue5507-qe.smt2 regress1/quantifiers/issue993.smt2 regress1/quantifiers/javafe.ast.StmtVec.009.smt2 regress1/quantifiers/lia-witness-div-pp.smt2 diff --git a/test/regress/regress1/quantifiers/issue5506-qe.smt2 b/test/regress/regress1/quantifiers/issue5506-qe.smt2 new file mode 100644 index 000000000..3839f2d75 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue5506-qe.smt2 @@ -0,0 +1,6 @@ +; SCRUBBER: sed 's/(.*)/()/g' +; EXPECT: () +; EXIT: 0 +(set-logic LIA) +(declare-fun a () Int) +(get-qe (forall ((b Int)) (= a 0))) diff --git a/test/regress/regress1/quantifiers/issue5507-qe.smt2 b/test/regress/regress1/quantifiers/issue5507-qe.smt2 new file mode 100644 index 000000000..3b7ddbcf3 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue5507-qe.smt2 @@ -0,0 +1,19 @@ +; EXPECT: false +; EXIT: 0 +(set-logic LIA) +(declare-fun v0 () Bool) +(declare-fun v1 () Bool) +(declare-fun v2 () Bool) +(declare-fun v3 () Bool) +(declare-fun v5 () Bool) +(declare-fun v6 () Bool) +(declare-fun v9 () Bool) +(declare-fun v10 () Bool) +(declare-fun v15 () Bool) +(declare-fun v16 () Bool) +(declare-fun i0 () Int) +(declare-fun i2 () Int) +(declare-fun i9 () Int) +(declare-fun v26 () Bool) +(declare-fun v33 () Bool) +(get-qe (exists ((q154 Bool) (q155 Int) (q156 Bool) (q157 Bool) (q158 Bool) (q159 Bool) (q160 Int)) (and (=> (distinct 309 i2) (or q157 v9 (distinct v16 v6 v5 v10) q159 (=> v15 v26))) (exists ((q154 Bool) (q155 Int) (q156 Bool) (q157 Bool) (q158 Bool) (q159 Bool) (q160 Int)) (=> (xor q156 v3 v2 q156 q156 q159 (>= 217 826 149 i0 i9) v1 v5 q157 q157) (distinct q160 q160))) v33 (distinct v16 v6 v5 v10) v0))) -- 2.30.2