Split simplifyFormulas to another parametrized function

Author: Tomaqa

src/api/MainSolver.cc

@@ -196,67 +196,86 @@ void MainSolver::propagateDecisionPreferenceToSMTSolver(PTRef pref, FrameId fram
 sstat MainSolver::simplifyFormulas() {
     status = s_Undef;
     for (std::size_t i = firstNotSimplifiedFrame; i < frames.frameCount() && status != s_False; i++) {
+        auto & frame = frames[i];
+        FrameId const frameId = frame.getId();
         PreprocessingContext context{.frameCount = i, .perPartition = trackPartitions()};
         preprocessor.prepareForProcessingFrame(i);
         firstNotSimplifiedFrame = i + 1;
-        if (context.perPartition) {
-            vec<PTRef> frameFormulas;
-            for (PTRef fla : frames[i].formulas) {
-                PTRef processed = theory->preprocessAfterSubstitutions(fla, context);
-                pmanager.transferPartitionMembership(fla, processed);
-                frameFormulas.push(processed);
-                preprocessor.addPreprocessedFormula(processed);
-            }
-            if (frameFormulas.size() == 0 or std::all_of(frameFormulas.begin(), frameFormulas.end(),
-                                                         [&](PTRef fla) { return fla == logic.getTerm_true(); })) {
-                continue;
-            }
-            theory->afterPreprocessing(preprocessor.getPreprocessedFormulas());
-            assert(frameFormulas.size() == frames[i].formulas.size());
-            for (PTRef & fla : frameFormulas) {
-                if (fla == logic.getTerm_true()) { continue; }
-                assert(pmanager.getPartitionIndex(fla) != -1);
-                // Optimize the dag for cnfization
-                if (logic.isBooleanOperator(fla)) {
-                    PTRef old = fla;
-                    fla = rewriteMaxArity(fla);
-                    pmanager.transferPartitionMembership(old, fla);
-                }
-                assert(pmanager.getPartitionIndex(fla) != -1);
-                pmanager.propagatePartitionMask(fla);
-                status = giveToSolver(fla, frames[i].getId());
-                if (status == s_False) { break; }
-            }
-        } else {
-            PTRef frameFormula = logic.mkAnd(frames[i].formulas);
-            if (context.frameCount > 0) { frameFormula = applyLearntSubstitutions(frameFormula); }
-            frameFormula = theory->preprocessBeforeSubstitutions(frameFormula, context);
-            frameFormula = substitutionPass(frameFormula, context);
-            frameFormula = theory->preprocessAfterSubstitutions(frameFormula, context);
-
-            if (logic.isFalse(frameFormula)) {
-                giveToSolver(logic.getTerm_false(), frames[i].getId());
-                status = s_False;
-                break;
-            }
-            preprocessor.addPreprocessedFormula(frameFormula);
-            theory->afterPreprocessing(preprocessor.getPreprocessedFormulas());
-            // Optimize the dag for cnfization
-            if (logic.isBooleanOperator(frameFormula)) { frameFormula = rewriteMaxArity(frameFormula); }
-            status = giveToSolver(frameFormula, frames[i].getId());
-        }
+        simplifyFormulas(frame.formulas, frameId, context);
+        if (status == s_False) { break; }
 
         for (PTRef pref : decisionPreferences.scope(i)) {
-            propagateDecisionPreferenceToSMTSolver(pref, frames[i].getId());
+            propagateDecisionPreferenceToSMTSolver(pref, frameId);
         }
     }
+
     if (status == s_False) {
         assert(firstNotSimplifiedFrame > 0);
         rememberUnsatFrame(firstNotSimplifiedFrame - 1);
     }
+
     return status;
 }
 
+void MainSolver::simplifyFormulas(vec<PTRef> const & frameFormulas, FrameId frameId,
+                                  PreprocessingContext const & context) {
+    if (frameFormulas.size() == 0) { return; }
+
+    if (not context.perPartition) {
+        PTRef frameFormula = logic.mkAnd(frameFormulas);
+        if (context.frameCount > 0) { frameFormula = applyLearntSubstitutions(frameFormula); }
+        frameFormula = theory->preprocessBeforeSubstitutions(frameFormula, context);
+        frameFormula = substitutionPass(frameFormula, context);
+        frameFormula = theory->preprocessAfterSubstitutions(frameFormula, context);
+
+        if (logic.isFalse(frameFormula)) {
+            giveToSolver(logic.getTerm_false(), frameId);
+            status = s_False;
+            return;
+        }
+
+        preprocessor.addPreprocessedFormula(frameFormula);
+        theory->afterPreprocessing(preprocessor.getPreprocessedFormulas());
+        // Optimize the dag for cnfization
+        if (logic.isBooleanOperator(frameFormula)) { frameFormula = rewriteMaxArity(frameFormula); }
+        status = giveToSolver(frameFormula, frameId);
+        return;
+    }
+
+    vec<PTRef> processedFormulas;
+    for (PTRef fla : frameFormulas) {
+        PTRef processed = theory->preprocessAfterSubstitutions(fla, context);
+        pmanager.transferPartitionMembership(fla, processed);
+        processedFormulas.push(processed);
+        preprocessor.addPreprocessedFormula(processed);
+    }
+
+    assert(processedFormulas.size() == frameFormulas.size());
+    assert(processedFormulas.size() > 0);
+    if (std::all_of(processedFormulas.begin(), processedFormulas.end(),
+                    [&](PTRef fla) { return fla == logic.getTerm_true(); })) {
+        return;
+    }
+
+    theory->afterPreprocessing(preprocessor.getPreprocessedFormulas());
+    for (PTRef & fla : processedFormulas) {
+        if (fla == logic.getTerm_true()) { continue; }
+        assert(pmanager.getPartitionIndex(fla) != -1);
+        // Optimize the dag for cnfization
+        if (logic.isBooleanOperator(fla)) {
+            PTRef old = fla;
+            fla = rewriteMaxArity(fla);
+            pmanager.transferPartitionMembership(old, fla);
+        }
+        assert(pmanager.getPartitionIndex(fla) != -1);
+        pmanager.propagatePartitionMask(fla);
+        status = giveToSolver(fla, frameId);
+        if (status == s_False) { return; }
+    }
+
+    // if needed, return processedFormulas
+}
+
 vec<PTRef> MainSolver::getCurrentAssertions() const {
     vec<PTRef> assertions;
     size_t const cnt = frames.frameCount();

src/api/MainSolver.h

@@ -297,6 +297,8 @@ class MainSolver {
 
     void propagateDecisionPreferenceToSMTSolver(PTRef, FrameId);
 
+    void simplifyFormulas(vec<PTRef> const & frameFormulas, FrameId, PreprocessingContext const &);
+
     PTRef rewriteMaxArity(PTRef root);
 
     virtual sstat solve_(vec<FrameId> const & enabledFrames);