From 6beb76055b81510ec38a8b50f5ed35d2f5010139 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 20 Nov 2020 15:19:40 -0600 Subject: [PATCH] Support nested quantifier elimination for get-qe command (#5490) Uses new nested-qe utility for eliminating nested quantification before doing quantifier elimination. Fixes CVC4/cvc4-wishues#26 Fixes #5484. --- src/smt/quant_elim_solver.cpp | 5 +++++ src/theory/quantifiers/cegqi/nested_qe.cpp | 15 +++++++++++---- .../quantifiers/quantifiers_rewriter.cpp | 5 +++-- test/regress/CMakeLists.txt | 2 ++ .../regress1/quantifiers/issue5484-qe.smt2 | 9 +++++++++ .../regress1/quantifiers/issue5484b-qe.smt2 | 18 ++++++++++++++++++ 6 files changed, 48 insertions(+), 6 deletions(-) create mode 100644 test/regress/regress1/quantifiers/issue5484-qe.smt2 create mode 100644 test/regress/regress1/quantifiers/issue5484b-qe.smt2 diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp index 59e9dfc9e..e5ecafd4a 100644 --- a/src/smt/quant_elim_solver.cpp +++ b/src/smt/quant_elim_solver.cpp @@ -16,6 +16,7 @@ #include "expr/subs.h" #include "smt/smt_solver.h" +#include "theory/quantifiers/cegqi/nested_qe.h" #include "theory/quantifiers/extended_rewrite.h" #include "theory/rewriter.h" #include "theory/theory_engine.h" @@ -40,6 +41,10 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, throw ModalException( "Expecting a quantified formula as argument to get-qe."); } + // 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(); diff --git a/src/theory/quantifiers/cegqi/nested_qe.cpp b/src/theory/quantifiers/cegqi/nested_qe.cpp index 7f77a1daf..72e7ef66f 100644 --- a/src/theory/quantifiers/cegqi/nested_qe.cpp +++ b/src/theory/quantifiers/cegqi/nested_qe.cpp @@ -69,6 +69,14 @@ bool NestedQe::hasNestedQuantification(Node q) Node NestedQe::doNestedQe(Node q, bool keepTopLevel) { + NodeManager* nm = NodeManager::currentNM(); + Node qOrig = q; + bool inputExists = false; + if (q.getKind() == kind::EXISTS) + { + q = nm->mkNode(kind::FORALL, q[0], q[1].negate()); + inputExists = true; + } Assert(q.getKind() == kind::FORALL); std::unordered_set nqs; if (!getNestedQuantification(q, nqs)) @@ -77,7 +85,7 @@ Node NestedQe::doNestedQe(Node q, bool keepTopLevel) << "...no nested quantification" << std::endl; if (keepTopLevel) { - return q; + return qOrig; } // just do ordinary quantifier elimination Node qqe = doQe(q); @@ -114,13 +122,12 @@ Node NestedQe::doNestedQe(Node q, bool keepTopLevel) // reconstruct the body std::vector qargs; qargs.push_back(q[0]); - qargs.push_back(qeBody); + qargs.push_back(inputExists ? qeBody.negate() : qeBody); if (q.getNumChildren() == 3) { qargs.push_back(q[2]); } - NodeManager* nm = NodeManager::currentNM(); - return nm->mkNode(kind::FORALL, qargs); + return nm->mkNode(inputExists ? kind::EXISTS : kind::FORALL, qargs); } Node NestedQe::doQe(Node q) diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 034226474..6d7275fac 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -1865,8 +1865,9 @@ bool QuantifiersRewriter::doOperation(Node q, } else if (computeOption == COMPUTE_PROCESS_TERMS) { - return options::elimExtArithQuant() - || options::iteLiftQuant() != options::IteLiftQuantMode::NONE; + return is_std + && (options::elimExtArithQuant() + || options::iteLiftQuant() != options::IteLiftQuantMode::NONE); } else if (computeOption == COMPUTE_COND_SPLIT) { diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 7e87c337a..cb37b428e 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1616,6 +1616,8 @@ set(regress_1_tests regress1/quantifiers/issue5469-aext.smt2 regress1/quantifiers/issue5470-aext.smt2 regress1/quantifiers/issue5471-aext.smt2 + regress1/quantifiers/issue5484-qe.smt2 + regress1/quantifiers/issue5484b-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/issue5484-qe.smt2 b/test/regress/regress1/quantifiers/issue5484-qe.smt2 new file mode 100644 index 000000000..c2499ed16 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue5484-qe.smt2 @@ -0,0 +1,9 @@ +; SCRUBBER: sed 's/(.*)/()/g' +; EXPECT: () +; EXIT: 0 +(set-logic LIA) +(declare-fun v9 () Bool) +(declare-fun v18 () Bool) +(declare-fun i2 () Int) +(declare-fun v31 () Bool) +(get-qe (forall ((q23 Int) (q24 Int) (q25 Int) (q26 Int) (q27 Bool) (q28 Int) (q29 Int)) (xor (=> (not (not (distinct 83 407))) (> (- i2 31 722) 319)) (forall ((q23 Int) (q24 Int) (q25 Int) (q26 Int) (q27 Bool) (q28 Int) (q29 Int)) (not (not (not v9)))) v31 (> 665 (+ (mod 83 923) (div i2 850)) 319 (- 939 878)) v18))) diff --git a/test/regress/regress1/quantifiers/issue5484b-qe.smt2 b/test/regress/regress1/quantifiers/issue5484b-qe.smt2 new file mode 100644 index 000000000..86f999504 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue5484b-qe.smt2 @@ -0,0 +1,18 @@ +; SCRUBBER: sed 's/(.*)/()/g' +; EXPECT: () +; EXIT: 0 +(set-logic LIA) +(declare-fun v0 () Bool) +(declare-fun v1 () Bool) +(declare-fun v2 () Bool) +(declare-fun v3 () Bool) +(declare-fun v4 () Bool) +(declare-fun v7 () Bool) +(declare-fun v8 () Bool) +(declare-fun i6 () Int) +(declare-fun i9 () Int) +(declare-fun i11 () Int) +(declare-fun i13 () Int) +(declare-fun v9 () Bool) +(declare-fun i16 () Int) +(get-qe (forall ((q75 Bool)) (xor (< i9 52) (forall ((q75 Bool)) (not (and (< i16 37) q75 q75 v1))) v2 (and (distinct v4 v3 v4) v9 v9 (and v7 v0 (>= 24 56 i11 i6 7) v0 v8)) (= (+ (div i13 340) 268 i9) i13)))) -- 2.30.2