diff options
| -rw-r--r-- | src/smt/term_formula_removal.cpp | 8 | ||||
| -rw-r--r-- | src/theory/theory_engine.cpp | 13 | ||||
| -rw-r--r-- | src/theory/theory_preprocessor.cpp | 5 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/quantifiers/issue5482-rtf-no-fv.smt2 | 15 |
5 files changed, 34 insertions, 8 deletions
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<Node, uint32_t>& 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<TrustNode> newLemmas; std::vector<Node> 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) |