Revert change in lemma order in prop engine (#8911)

This reverts the change in lemma order from #8301.

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 91f1aaf7612d80cf6b3183564118b9a8e4a067d9..74e78d14d5fdfb6b56759a4492e33e991ff7596e 100644 (file)
--- 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<theory::SkolemLemma>& 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 71720ddc6988e1346c52cb86c921b03bfe993151..420497978b94d1374478f0cf0f8943be8cd5e81d 100644 (file)
--- 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 b34673942a442b88e1d42d00417ef00dc457989a..d8552fe7e31f9ee48396cb834693511d405f3878 100644 (file)
--- 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<Node>& assertions,
                            std::unordered_map<size_t, Node>& 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 ee6df9221f6608af85eda29a42126d8649ea9afb..1a159a942404af4b4b8cf28b8e0ea68823ee5164 100644 (file)
--- 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 (file)
index 0000000..ae26c32
--- /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)