From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Fri, 12 Mar 2021 20:26:55 +0000 (-0800)
Subject: Schedule preregistration lemmas to be satisfied after user assertions (#6134)
X-Git-Tag: cvc5-1.0.0~2086
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=210734994076904f4770dfe7a1877bf3d2687f39;p=cvc5.git

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 d44122767..71b27d8ec 100644
--- 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);
 }