From b10e383e5efc92f02c63eaf5eec07479ed385304 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 11 Feb 2021 07:17:53 -0600
Subject: [PATCH] Simplify interface for preprocessor (#5890)

This does a minor simplification to the interface for preprocessor. It has a postProcess call that is called after another unrelated call at the SmtSolver level (notifyPreprocessedAssertions) is made. This makes it so that Preprocessor::postProcess is inlined as the last step of process.
---
 src/smt/preprocessor.cpp | 10 +++++-----
 src/smt/preprocessor.h   |  6 ------
 src/smt/smt_solver.cpp   |  2 --
 3 files changed, 5 insertions(+), 13 deletions(-)

diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index ec7751a54..3e4ef0cdd 100644
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -80,12 +80,10 @@ bool Preprocessor::process(Assertions& as)
   }
 
   // process the assertions, return true if no conflict is discovered
-  return d_processor.apply(as);
-}
+  bool noConflict = d_processor.apply(as);
+
+  // now, post-process the assertions
 
-void Preprocessor::postprocess(Assertions& as)
-{
-  preprocessing::AssertionPipeline& ap = as.getAssertionPipeline();
   // if incremental, compute which variables are assigned
   if (options::incrementalSolving())
   {
@@ -94,6 +92,8 @@ void Preprocessor::postprocess(Assertions& as)
 
   // mark that we've processed assertions
   d_assertionsProcessed = true;
+
+  return noConflict;
 }
 
 void Preprocessor::clearLearnedLiterals()
diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h
index 367490306..22b585e05 100644
--- a/src/smt/preprocessor.h
+++ b/src/smt/preprocessor.h
@@ -55,12 +55,6 @@ class Preprocessor
    * true if no conflict was discovered while preprocessing them.
    */
   bool process(Assertions& as);
-  /**
-   * Postprocess assertions, called after the SmtEngine has finished
-   * giving the assertions to the SMT solver and before the assertions are
-   * cleared.
-   */
-  void postprocess(Assertions& as);
   /**
    * Clear learned literals from the Boolean propagator.
    */
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index c47d1c624..83f2146f4 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -236,8 +236,6 @@ void SmtSolver::processAssertions(Assertions& as)
   // end: INVARIANT to maintain: no reordering of assertions or
   // introducing new ones
 
-  d_pp.postprocess(as);
-
   // Push the formula to SAT
   {
     Chat() << "converting to CNF..." << endl;
-- 
2.30.2