Schedule preregistration lemmas to be satisfied after user assertions (#6134)

Commit d47a8708171f1cf488fe9ce05f56f2566db53093 refactored the interface of
prop engine. In doing so, it changed the order in which preregistration lemmas
were asserted. Before the commit, they were asserted after all the user
assertions. After the commit, they were asserted after each user assertion that
generated them. This, however, seems to have a negative performance impact,
especially for string benchmarks because the justification heuristic tries to
justify the assertions in the order in which they appear. Intuitively, it makes
sense to first try to satisfy the user assertions before trying to satisfy the
preregistration lemmas.

Signed-off-by: Andres Noetzli <noetzli@amazon.com>

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index d4412276717965634f5e156536e2a3215f5d1c90..71b27d8ec39bdf67f96f01b429ccf2d271bc120e 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -176,12 +176,15 @@ void PropEngine::notifyPreprocessedAssertions(
 {
   // notify the theory engine of preprocessed assertions
   d_theoryEngine->notifyPreprocessedAssertions(assertions);
+  for (const Node& assertion : assertions)
+  {
+    d_decisionEngine->addAssertion(assertion);
+  }
 }
 
 void PropEngine::assertFormula(TNode node) {
   Assert(!d_inCheckSat) << "Sat solver in solve()!";
   Debug("prop") << "assertFormula(" << node << ")" << std::endl;
-  d_decisionEngine->addAssertion(node);
   assertInternal(node, false, false, true);
 }