From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 11 Feb 2021 13:17:53 +0000 (-0600)
Subject: Simplify interface for preprocessor (#5890)
X-Git-Tag: cvc5-1.0.0~2289
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b10e383e5efc92f02c63eaf5eec07479ed385304;p=cvc5.git

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 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;