Added counters of already preprocessed assertions and possibly skipping those

Author: Tomaqa

src/api/MainSolver.cc

@@ -23,6 +23,8 @@
 #include <tsolvers/RDLTHandler.h>
 #include <unsatcores/UnsatCoreBuilder.h>
 
+#include <type_traits>
+
 namespace opensmt {
 
 MainSolver::MainSolver(Logic & logic, SMTConfig & conf, std::string name)
@@ -60,6 +62,7 @@ void MainSolver::initialize() {
     frames.push();
     frameTerms.push(logic.getTerm_true());
     preprocessor.initialize();
+    preprocessedAssertionsCountPerFrame.push_back(0);
     smt_solver->initialize();
     pair<CRef, CRef> iorefs{CRef_Undef, CRef_Undef};
     smt_solver->addOriginalSMTClause({term_mapper->getOrCreateLit(logic.getTerm_true())}, iorefs);
@@ -74,6 +77,7 @@ void MainSolver::push() {
     frames.push();
     preprocessor.push();
     frameTerms.push(newFrameTerm(frames.last().getId()));
+    preprocessedAssertionsCountPerFrame.push_back(0);
     termNames.pushScope();
     if (alreadyUnsat) { rememberLastFrameUnsat(); }
 }
@@ -92,7 +96,9 @@ bool MainSolver::pop() {
     }
     frames.pop();
     preprocessor.pop();
+    preprocessedAssertionsCountPerFrame.pop_back();
     termNames.popScope();
+    // goes back to frames.frameCount()-1 only if a formula is added via addAssertion
     firstNotPreprocessedFrame = std::min(firstNotPreprocessedFrame, frames.frameCount());
     if (not isLastFrameUnsat()) { getSMTSolver().restoreOK(); }
     return true;
@@ -158,9 +164,14 @@ sstat MainSolver::simplifyFormulas() {
 bool MainSolver::tryPreprocessFormulasOfFrame(std::size_t i) {
     auto & frame = frames[i];
     FrameId const frameId = frame.getId();
-    PreprocessingContext context{.frameCount = i, .perPartition = trackPartitions()};
+    auto & preprocessedFrameAssertionsCount = preprocessedAssertionsCountPerFrame[i];
+    assert(frame.formulas.size() == 0 or std::size_t(frame.formulas.size()) > preprocessedFrameAssertionsCount);
+    PreprocessingContext context{.frameCount = i,
+                                 .preprocessedFrameAssertionsCount = preprocessedFrameAssertionsCount,
+                                 .perPartition = trackPartitions()};
     preprocessor.prepareForProcessingFrame(i);
     firstNotPreprocessedFrame = i + 1;
+    preprocessedFrameAssertionsCount = frame.formulas.size();
 
     assert(status != s_False);
 
@@ -185,6 +196,7 @@ PTRef MainSolver::preprocessFormulasDefault(vec<PTRef> const & frameFormulas, Pr
 
     if (frameFormulas.size() == 0) { return logic.getTerm_true(); }
 
+    // Include even already preprocessed formulas which can still benefit from the new ones
     PTRef frameFormula = logic.mkAnd(frameFormulas);
     return preprocessFormula(frameFormula, context);
 }
@@ -193,16 +205,21 @@ vec<PTRef> MainSolver::preprocessFormulasPerPartition(vec<PTRef> const & frameFo
                                                       PreprocessingContext const & context) {
     assert(context.perPartition);
 
-    if (frameFormulas.size() == 0) { return {}; }
+    std::size_t const frameFormulasCount = frameFormulas.size();
+    static_assert(std::is_unsigned_v<decltype(context.preprocessedFrameAssertionsCount)>);
+    assert(context.preprocessedFrameAssertionsCount <= frameFormulasCount);
+    std::size_t const formulasCountToProcess = frameFormulasCount - context.preprocessedFrameAssertionsCount;
+    if (formulasCountToProcess == 0) { return {}; }
 
     vec<PTRef> processedFormulas;
-    for (PTRef fla : frameFormulas) {
+    for (std::size_t i = context.preprocessedFrameAssertionsCount; i < frameFormulasCount; ++i) {
+        PTRef fla = frameFormulas[i];
         PTRef processed = preprocessFormulaBeforeFinalTheoryPreprocessing(fla, context);
         processedFormulas.push(processed);
     }
 
-    assert(processedFormulas.size() == frameFormulas.size());
-    assert(processedFormulas.size() > 0);
+    assert(std::size_t(processedFormulas.size()) == formulasCountToProcess);
+    assert(std::size_t(processedFormulas.size()) > 0);
     if (std::all_of(processedFormulas.begin(), processedFormulas.end(),
                     [&](PTRef fla) { return fla == logic.getTerm_true(); })) {
         return {};

src/api/MainSolver.h

@@ -336,6 +336,7 @@ class MainSolver {
     vec<PTRef> frameTerms;
     std::size_t firstNotPreprocessedFrame = 0;
     std::size_t insertedAssertionsCount = 0;
+    std::vector<std::size_t> preprocessedAssertionsCountPerFrame;
 };
 
 bool MainSolver::trackPartitions() const {

src/logics/Theory.h

@@ -36,6 +36,7 @@ namespace opensmt {
 
 struct PreprocessingContext {
     std::size_t frameCount {0};
+    std::size_t preprocessedFrameAssertionsCount{0};
     bool perPartition {false};
 };