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.

diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index ec7751a54504b6c033549f43af7d56bd5732dd1c..3e4ef0cdd67f3c8ff7b840ab66cff21ecd4996d8 100644 (file)
--- 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 367490306fcf5b4e48c08b0befb6945bbc42bc97..22b585e0543ac44f45807d8c2386c2b31dc9ef83 100644 (file)
--- 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 c47d1c62416b1b495a21166506a5a075c084cb45..83f2146f4d0165a806f2c6d3d730ee6aebfa4ff0 100644 (file)
--- 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;