Placed the loop body of simplifyFormulas into another separate function

Author: Tomaqa

src/api/MainSolver.cc

@@ -141,23 +141,10 @@ bool MainSolver::tryAddTermNameFor(PTRef fla, std::string const & name) {
 sstat MainSolver::simplifyFormulas() {
     status = s_Undef;
     for (std::size_t i = firstNotPreprocessedFrame; i < frames.frameCount(); ++i) {
-        auto & frame = frames[i];
-        FrameId const frameId = frame.getId();
-        PreprocessingContext context{.frameCount = i, .perPartition = trackPartitions()};
-        preprocessor.prepareForProcessingFrame(i);
-        firstNotPreprocessedFrame = i + 1;
-
-        if (not context.perPartition) {
-            PTRef frameFormula = preprocessFormulasDefault(frame.formulas, context);
-            status = giveToSolver(frameFormula, frameId);
-        } else {
-            vec<PTRef> processedFormulas = preprocessFormulasPerPartition(frame.formulas, context);
-            for (PTRef fla : processedFormulas) {
-                status = giveToSolver(fla, frameId);
-                if (status == s_False) { break; }
-            }
-        }
-        if (status == s_False) { break; }
+        assert(status != s_False);
+        if (tryPreprocessFormulasOfFrame(i)) { continue; }
+        assert(status == s_False);
+        break;
     }
 
     if (status == s_False) {
@@ -168,6 +155,31 @@ sstat MainSolver::simplifyFormulas() {
     return status;
 }
 
+bool MainSolver::tryPreprocessFormulasOfFrame(std::size_t i) {
+    auto & frame = frames[i];
+    FrameId const frameId = frame.getId();
+    PreprocessingContext context{.frameCount = i, .perPartition = trackPartitions()};
+    preprocessor.prepareForProcessingFrame(i);
+    firstNotPreprocessedFrame = i + 1;
+
+    assert(status != s_False);
+
+    if (not context.perPartition) {
+        PTRef frameFormula = preprocessFormulasDefault(frame.formulas, context);
+        status = giveToSolver(frameFormula, frameId);
+        return status != s_False;
+    }
+
+    vec<PTRef> processedFormulas = preprocessFormulasPerPartition(frame.formulas, context);
+    for (PTRef fla : processedFormulas) {
+        status = giveToSolver(fla, frameId);
+        if (status == s_False) { return false; }
+    }
+
+    assert(status != s_False);
+    return true;
+}
+
 PTRef MainSolver::preprocessFormulasDefault(vec<PTRef> const & frameFormulas, PreprocessingContext const & context) {
     assert(not context.perPartition);
 

src/api/MainSolver.h

@@ -291,6 +291,8 @@ class MainSolver {
 
     inline bool trackPartitions() const;
 
+    virtual bool tryPreprocessFormulasOfFrame(std::size_t);
+
     virtual PTRef preprocessFormulasDefault(vec<PTRef> const & frameFormulas, PreprocessingContext const &);
     virtual vec<PTRef> preprocessFormulasPerPartition(vec<PTRef> const & frameFormulas, PreprocessingContext const &);