From 6edbfc98df1e9302f5051e33accc328ad7250c2b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 20 Nov 2020 17:49:27 -0600 Subject: [PATCH] Fix remove term formula policy for terms beneath quantifiers (#5497) Now that extended arithmetic symbols are not eliminated during expandDefinitions, this allowed for a chain of events that would not apply theory preprocessing on certain terms. In particular, a term t would not have theory preprocessing applied to it if it was a strict subterm of ITE-term s that occurred in a term position in a quantified formula body, and s did not have free variables. In this case, term formula removal would add a lemma corresponding to the ITE skolem definition, whose subterms did not have theory preprocessing applied. This meant that a (div a d) term was not being preprocessed in #5482, leading to solution unsoundness. This changes the policy in term formula removal to be in sync with theory preprocessing: term formula removal and theory preprocessing only apply to terms that are not beneath quantifiers. In particular, this means that ground terms in quantifier bodies are left untouched until they are introduced e.g. by instantiation. This fixes the solution soundness issue (fixes #5482). --- src/smt/term_formula_removal.cpp | 8 +++++--- src/theory/theory_engine.cpp | 13 +++++++++---- src/theory/theory_preprocessor.cpp | 5 ++++- test/regress/CMakeLists.txt | 1 + .../regress1/quantifiers/issue5482-rtf-no-fv.smt2 | 15 +++++++++++++++ 5 files changed, 34 insertions(+), 8 deletions(-) create mode 100644 test/regress/regress1/quantifiers/issue5482-rtf-no-fv.smt2 diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index 46135f12a..f3e0d0bd6 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -200,9 +200,11 @@ Node RemoveTermFormulas::runCurrent(std::pair& curr, // in the "non-variable Boolean term within term" case below. if (node.getKind() == kind::ITE && !nodeType.isBoolean()) { - // Here, we eliminate the ITE if we are not Boolean and if we do not contain - // a free variable. - if (!inQuant || !expr::hasFreeVar(node)) + // Here, we eliminate the ITE if we are not Boolean and if we are + // not in a quantified formula. This policy should be in sync with + // the policy for when to apply theory preprocessing to terms, see PR + // #5497. + if (!inQuant) { skolem = getSkolemForNode(node); if (skolem.isNull()) diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index dc59cbbf5..e771f8bb8 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -24,7 +24,6 @@ #include "expr/attribute.h" #include "expr/lazy_proof.h" #include "expr/node.h" -#include "expr/node_algorithm.h" #include "expr/node_builder.h" #include "expr/node_visitor.h" #include "options/bv_options.h" @@ -1171,19 +1170,21 @@ Node TheoryEngine::getModelValue(TNode var) { Node TheoryEngine::ensureLiteral(TNode n) { - Debug("ensureLiteral") << "rewriting: " << n << std::endl; + Trace("ensureLiteral") << "ensureLiteral rewriting: " << n << std::endl; Node rewritten = Rewriter::rewrite(n); - Debug("ensureLiteral") << " got: " << rewritten << std::endl; + Trace("ensureLiteral") << " got: " << rewritten << std::endl; std::vector newLemmas; std::vector newSkolems; TrustNode tpn = d_tpp.preprocess(n, newLemmas, newSkolems, true); // send lemmas corresponding to the skolems introduced by preprocessing n for (const TrustNode& tnl : newLemmas) { + Trace("ensureLiteral") << " lemma: " << tnl.getNode() << std::endl; lemma(tnl, LemmaProperty::NONE); } Node preprocessed = tpn.isNull() ? rewritten : tpn.getNode(); - Debug("ensureLiteral") << "preprocessed: " << preprocessed << std::endl; + Trace("ensureLiteral") << "ensureLiteral preprocessed: " << preprocessed + << std::endl; d_propEngine->ensureLiteral(preprocessed); return preprocessed; } @@ -1400,6 +1401,7 @@ theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma, // get the node Node node = tlemma.getNode(); Node lemma = tlemma.getProven(); + Trace("te-lemma") << "Lemma, input: " << lemma << std::endl; Assert(!expr::hasFreeVar(lemma)); @@ -1528,9 +1530,12 @@ theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma, } // now, send the lemmas to the prop engine + Trace("te-lemma") << "Lemma, output: " << tlemma.getProven() << std::endl; d_propEngine->assertLemma(tlemma.getProven(), false, removable); for (size_t i = 0, lsize = newLemmas.size(); i < lsize; ++i) { + Trace("te-lemma") << "Lemma, new lemma: " << newLemmas[i].getProven() + << std::endl; d_propEngine->assertLemma(newLemmas[i].getProven(), false, removable); } diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp index 9ebf12577..3b68a33ca 100644 --- a/src/theory/theory_preprocessor.cpp +++ b/src/theory/theory_preprocessor.cpp @@ -139,6 +139,8 @@ TrustNode TheoryPreprocessor::preprocess(TNode node, } if (node == retNode) { + Trace("tpp-debug") << "...TheoryPreprocessor::preprocess returned no change" + << std::endl; // no change Assert(newLemmas.empty()); return TrustNode::null(); @@ -217,7 +219,8 @@ TrustNode TheoryPreprocessor::preprocess(TNode node, Assert(!isProofEnabled() || newLemmas[i].getGenerator() != nullptr); newLemmas[i].debugCheckClosed("tpp-debug", "TheoryPreprocessor::lemma_new"); } - Trace("tpp-debug") << "Preprocessed: " << node << " " << retNode << std::endl; + Trace("tpp-debug") << "...TheoryPreprocessor::preprocess returned " + << tret.getNode() << std::endl; return tret; } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index cb37b428e..af238db18 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1616,6 +1616,7 @@ set(regress_1_tests regress1/quantifiers/issue5469-aext.smt2 regress1/quantifiers/issue5470-aext.smt2 regress1/quantifiers/issue5471-aext.smt2 + regress1/quantifiers/issue5482-rtf-no-fv.smt2 regress1/quantifiers/issue5484-qe.smt2 regress1/quantifiers/issue5484b-qe.smt2 regress1/quantifiers/issue993.smt2 diff --git a/test/regress/regress1/quantifiers/issue5482-rtf-no-fv.smt2 b/test/regress/regress1/quantifiers/issue5482-rtf-no-fv.smt2 new file mode 100644 index 000000000..b1e6911cd --- /dev/null +++ b/test/regress/regress1/quantifiers/issue5482-rtf-no-fv.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --fmf-bound +; EXPECT: unsat +(set-logic AUFNIA) +(declare-fun a () Int) +(declare-fun b () (Array Int Int)) +(declare-fun c () (Array Int Int)) +(declare-fun d () Int) +(assert + (exists ((e Int)) + (and (<= e 0) + (exists ((f Int)) + (and (<= 0 f e) + (> (select (store b 0 (select c (div a d))) f) + (select (store b 0 (select c (div a d))) e))))))) +(check-sat) -- 2.30.2