From b71fcbb8aa09fdd14142a3349615f4eaea491c91 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 27 Jun 2022 15:46:04 -0500 Subject: [PATCH] Revert change in lemma order in prop engine (#8911) This reverts the change in lemma order from #8301. --- src/prop/prop_engine.cpp | 37 +++++++++++++------ src/prop/theory_proxy.cpp | 11 +++++- src/prop/theory_proxy.h | 7 +++- test/regress/cli/CMakeLists.txt | 1 + .../regress1/strings/prop-engine-order.smt2 | 12 ++++++ 5 files changed, 54 insertions(+), 14 deletions(-) create mode 100644 test/regress/cli/regress1/strings/prop-engine-order.smt2 diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 91f1aaf76..74e78d14d 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -223,6 +223,7 @@ void PropEngine::assertLemma(TrustNode tlemma, theory::LemmaProperty p) Trace("te-lemma") << "Lemma, new lemma: " << lem.d_lemma.getProven() << " (skolem is " << lem.d_skolem << ")" << std::endl; } + Trace("te-lemma") << "removable = " << removable << std::endl; } // now, assert the lemmas @@ -292,18 +293,37 @@ void PropEngine::assertLemmasInternal( const std::vector& ppLemmas, bool removable) { - // Assert to decision engine first. + if (!removable) + { + // notify skolem definitions first to ensure that the computation of + // when a literal contains a skolem is accurate in the calls below. + Trace("prop") << "Notify skolem definitions..." << std::endl; + for (const theory::SkolemLemma& lem : ppLemmas) + { + d_theoryProxy->notifySkolemDefinition(lem.getProven(), lem.d_skolem); + } + } + // Assert to the SAT solver first + Trace("prop") << "Push to SAT..." << std::endl; + if (!trn.isNull()) + { + assertTrustedLemmaInternal(trn, removable); + } + for (const theory::SkolemLemma& lem : ppLemmas) + { + assertTrustedLemmaInternal(lem.d_lemma, removable); + } // Note that this order is important for theories that send lemmas during // preregistration, as it impacts the order in which lemmas are processed // by default by the decision engine. In particular, sending to the SAT // solver first means that lemmas sent during preregistration in response to // the current lemma are processed after that lemma. This makes a difference // e.g. for string reduction lemmas, where preregistration lemmas are - // introduced for skolems that appear in reductions. Moving this - // block after the one below has mixed (trending negative) performance on - // SMT-LIB strings logics. + // introduced for skolems that appear in reductions. Moving the above + // block after the one below has mixed performance on SMT-LIB strings logics. if (!removable) { + Trace("prop") << "Notify assertions..." << std::endl; // also add to the decision engine, where notice we don't need proofs if (!trn.isNull()) { @@ -315,14 +335,7 @@ void PropEngine::assertLemmasInternal( d_theoryProxy->notifyAssertion(lem.getProven(), lem.d_skolem, true); } } - if (!trn.isNull()) - { - assertTrustedLemmaInternal(trn, removable); - } - for (const theory::SkolemLemma& lem : ppLemmas) - { - assertTrustedLemmaInternal(lem.d_lemma, removable); - } + Trace("prop") << "Finish " << trn << std::endl; } void PropEngine::requirePhase(TNode n, bool phase) { diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 71720ddc6..420497978 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -108,6 +108,10 @@ void TheoryProxy::notifyInputFormulas( { skolem = it->second; } + if (!skolem.isNull()) + { + notifySkolemDefinition(assertions[i], skolem); + } notifyAssertion(assertions[i], skolem, false); } @@ -119,6 +123,12 @@ void TheoryProxy::notifyInputFormulas( } } +void TheoryProxy::notifySkolemDefinition(Node a, TNode skolem) +{ + Assert(!skolem.isNull()); + d_skdm->notifySkolemDefinition(skolem, a); +} + void TheoryProxy::notifyAssertion(Node a, TNode skolem, bool isLemma) { if (skolem.isNull()) @@ -127,7 +137,6 @@ void TheoryProxy::notifyAssertion(Node a, TNode skolem, bool isLemma) } else { - d_skdm->notifySkolemDefinition(skolem, a); d_decisionEngine->addSkolemDefinition(a, skolem, isLemma); } } diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index b34673942..d8552fe7e 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -85,9 +85,14 @@ class TheoryProxy : protected EnvObj, public Registrar */ void notifyInputFormulas(const std::vector& assertions, std::unordered_map& skolemMap); + /** + * Notify that lem is a skolem definition for the given skolem. This is called + * before pushing the lemma to the SAT solver. + */ + void notifySkolemDefinition(Node lem, TNode skolem); /** * Notify a lemma or input assertion, possibly corresponding to a skolem - * definition. + * definition. This is called after pushing the lemma to the SAT solver. */ void notifyAssertion(Node lem, TNode skolem = TNode::null(), diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index ee6df9221..1a159a942 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -2661,6 +2661,7 @@ set(regress_1_tests regress1/strings/proj-issue281.smt2 regress1/strings/proj-issue331.smt2 regress1/strings/proj-issue502-merge-type.smt2 + regress1/strings/prop-engine-order.smt2 regress1/strings/query4674.smt2 regress1/strings/query8485.smt2 regress1/strings/re-all-char-hard.smt2 diff --git a/test/regress/cli/regress1/strings/prop-engine-order.smt2 b/test/regress/cli/regress1/strings/prop-engine-order.smt2 new file mode 100644 index 000000000..ae26c32d1 --- /dev/null +++ b/test/regress/cli/regress1/strings/prop-engine-order.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: sat +(set-logic ALL) +(declare-const x3 Bool) +(declare-const x Int) +(declare-const w String) +(declare-const a String) +(assert (str.contains (str.substr (str.++ a ":" a w) 0 x) "-p")) +(assert (not (str.prefixof "abcdefghijklmnop" (str.++ "" a)))) +(assert (or x3 (str.prefixof "ABCDEFGHIJKLMNO" (str.++ a "")))) +(assert (str.in_re a (re.* (re.range "a" "z")))) +(check-sat) -- 2.30.2