From 210734994076904f4770dfe7a1877bf3d2687f39 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 12 Mar 2021 12:26:55 -0800 Subject: [PATCH] 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 --- src/prop/prop_engine.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) 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); } -- 2.30.2