Split simplifyFormulas to sub-functions

This makes the preprocessing more maintainable, allows overriding particular parts and also allows preprocessing single formulas without necessarily giving them to the SMT solver

Author: Tomaqa

src/api/MainSolver.cc

@@ -213,68 +213,130 @@ Lit MainSolver::giveAnyDecisionPreferenceToSMTSolver(PTRef pref, FrameId frameId
 
 sstat MainSolver::simplifyFormulas() {
     status = s_Undef;
-    for (std::size_t i = firstNotSimplifiedFrame; i < frames.frameCount() && status != s_False; i++) {
+    for (std::size_t i = firstNotSimplifiedFrame; i < frames.frameCount(); ++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; }
-            }
+
+        if (not context.perPartition) {
+            PTRef frameFormula = preprocessFormulasDefault(frame.formulas, context);
+            status = giveToSolver(frameFormula, frameId);
         } 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;
+            vec<PTRef> processedFormulas = preprocessFormulasPerPartition(frame.formulas, context);
+            for (PTRef fla : processedFormulas) {
+                status = giveToSolver(fla, frameId);
+                if (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());
         }
+        if (status == s_False) { break; }
 
         for (PTRef pref : decisionPreferences.scope(i)) {
             giveDecisionPreferenceToSMTSolver(pref, frames[i].getId());
         }
     }
+
     if (status == s_False) {
         assert(firstNotSimplifiedFrame > 0);
         rememberUnsatFrame(firstNotSimplifiedFrame - 1);
     }
+
     return status;
 }
 
+PTRef MainSolver::preprocessFormulasDefault(vec<PTRef> const & frameFormulas, PreprocessingContext const & context) {
+    assert(not context.perPartition);
+
+    if (frameFormulas.size() == 0) { return logic.getTerm_true(); }
+
+    PTRef frameFormula = logic.mkAnd(frameFormulas);
+    return preprocessFormula(frameFormula, context);
+}
+
+vec<PTRef> MainSolver::preprocessFormulasPerPartition(vec<PTRef> const & frameFormulas,
+                                                      PreprocessingContext const & context) {
+    assert(context.perPartition);
+
+    if (frameFormulas.size() == 0) { return {}; }
+
+    vec<PTRef> processedFormulas;
+    for (PTRef fla : frameFormulas) {
+        PTRef processed = preprocessFormulaBeforeFinalTheoryPreprocessing(fla, context);
+        processedFormulas.push(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 {};
+    }
+
+    preprocessFormulaDoFinalTheoryPreprocessing(context);
+
+    for (PTRef & fla : processedFormulas) {
+        if (fla == logic.getTerm_true()) { continue; }
+        fla = preprocessFormulaAfterFinalTheoryPreprocessing(fla, context);
+    }
+
+    return processedFormulas;
+}
+
+PTRef MainSolver::preprocessFormula(PTRef fla, PreprocessingContext const & context) {
+    PTRef processed = preprocessFormulaBeforeFinalTheoryPreprocessing(fla, context);
+    preprocessFormulaDoFinalTheoryPreprocessing(context);
+    processed = preprocessFormulaAfterFinalTheoryPreprocessing(processed, context);
+    return processed;
+}
+
+PTRef MainSolver::preprocessFormulaBeforeFinalTheoryPreprocessing(PTRef fla, PreprocessingContext const & context) {
+    bool const perPartition = context.perPartition;
+    PTRef processed = fla;
+
+    if (not perPartition) {
+        if (context.frameCount > 0) { processed = applyLearntSubstitutions(processed); }
+        processed = theory->preprocessBeforeSubstitutions(processed, context);
+        processed = substitutionPass(processed, context);
+    }
+
+    processed = theory->preprocessAfterSubstitutions(processed, context);
+
+    if (perPartition) {
+        pmanager.transferPartitionMembership(fla, processed);
+    } else if (logic.isFalse(processed)) {
+        return logic.getTerm_false();
+    }
+
+    preprocessor.addPreprocessedFormula(processed);
+
+    return processed;
+}
+
+void MainSolver::preprocessFormulaDoFinalTheoryPreprocessing(PreprocessingContext const &) {
+    theory->afterPreprocessing(preprocessor.getPreprocessedFormulas());
+}
+
+PTRef MainSolver::preprocessFormulaAfterFinalTheoryPreprocessing(PTRef fla, PreprocessingContext const & context) {
+    bool const perPartition = context.perPartition;
+    PTRef processed = fla;
+
+    assert(not perPartition or pmanager.getPartitionIndex(processed) != -1);
+
+    // Optimize the dag for cnfization
+    if (logic.isBooleanOperator(processed)) {
+        processed = rewriteMaxArity(processed);
+        if (perPartition) { pmanager.transferPartitionMembership(fla, processed); }
+    }
+
+    if (perPartition) {
+        assert(pmanager.getPartitionIndex(processed) != -1);
+        pmanager.propagatePartitionMask(processed);
+    }
+
+    return processed;
+}
+
 vec<PTRef> MainSolver::getCurrentAssertions() const {
     vec<PTRef> assertions;
     size_t const cnt = frames.frameCount();
@@ -390,6 +452,8 @@ sstat MainSolver::giveToSolver(PTRef root, FrameId push_id) {
         void operator()(vec<Lit> && c) override { clauses.push_back(std::move(c)); }
     };
 
+    if (root == logic.getTerm_true()) { return s_Undef; }
+
     ClauseCallBack callBack;
     ts.setClauseCallBack(&callBack);
     ts.Cnfizer::cnfize(root, push_id);

src/api/MainSolver.h

@@ -300,6 +300,14 @@ class MainSolver {
     Lit giveBoolVarDecisionPreferenceToSMTSolver(PTRef);
     Lit giveAnyDecisionPreferenceToSMTSolver(PTRef, FrameId);
 
+    virtual PTRef preprocessFormulasDefault(vec<PTRef> const & frameFormulas, PreprocessingContext const &);
+    virtual vec<PTRef> preprocessFormulasPerPartition(vec<PTRef> const & frameFormulas, PreprocessingContext const &);
+
+    virtual PTRef preprocessFormula(PTRef, PreprocessingContext const &);
+    virtual PTRef preprocessFormulaBeforeFinalTheoryPreprocessing(PTRef, PreprocessingContext const &);
+    virtual void preprocessFormulaDoFinalTheoryPreprocessing(PreprocessingContext const &);
+    virtual PTRef preprocessFormulaAfterFinalTheoryPreprocessing(PTRef, PreprocessingContext const &);
+
     PTRef rewriteMaxArity(PTRef root);
 
     virtual sstat solve_(vec<FrameId> const & enabledFrames);