Moved preprocessing of ITE terms into the preprocessing pipeline

Author: Tomaqa

src/api/MainSolver.cc

@@ -113,8 +113,6 @@ void MainSolver::insertFormula(PTRef fla) {
     if (logic.getSortRef(fla) != logic.getSort_bool()) {
         throw ApiException("Top-level assertion sort must be Bool, got " + logic.sortToString(logic.getSortRef(fla)));
     }
-    // TODO: Move this to preprocessing of the formulas
-    fla = IteHandler(logic, getPartitionManager().getNofPartitions()).rewrite(fla);
 
     if (trackPartitions()) {
         // MB: Important for HiFrog! partition index is the index of the formula in an virtual array of inserted
@@ -186,6 +184,7 @@ PTRef MainSolver::preprocessFormulasDefault(vec<PTRef> const & frameFormulas, Pr
 
     // Include even already preprocessed formulas which can still benefit from the new ones
     PTRef frameFormula = logic.mkAnd(frameFormulas);
+    preprocessedAssertionsCount += frameFormulas.size();
     return preprocessFormula(frameFormula, context);
 }
 
@@ -206,6 +205,8 @@ vec<PTRef> MainSolver::preprocessFormulasPerPartition(vec<PTRef> const & frameFo
         processedFormulas.push(processed);
     }
 
+    preprocessedAssertionsCount += processedFormulas.size();
+
     assert(std::size_t(processedFormulas.size()) == formulasCountToProcess);
     assert(std::size_t(processedFormulas.size()) > 0);
     if (std::all_of(processedFormulas.begin(), processedFormulas.end(),
@@ -234,6 +235,9 @@ PTRef MainSolver::preprocessFormulaBeforeFinalTheoryPreprocessing(PTRef fla, Pre
     bool const perPartition = context.perPartition;
     PTRef processed = fla;
 
+    std::size_t const partitionNumber = perPartition ? pmanager.getPartitionIndex(fla) : preprocessedAssertionsCount;
+    processed = IteHandler(logic, partitionNumber).rewrite(processed);
+
     if (not perPartition) {
         if (context.frameCount > 0) { processed = applyLearntSubstitutions(processed); }
         processed = theory->preprocessBeforeSubstitutions(processed, context);
@@ -569,6 +573,7 @@ PTRef MainSolver::applyLearntSubstitutions(PTRef fla) {
 }
 
 PTRef MainSolver::substitutionPass(PTRef fla, PreprocessingContext const & context) {
+    assert(not trackPartitions());
     if (not config.do_substitutions()) { return fla; }
     auto res = computeSubstitutions(fla);
     vec<PTRef> args;

src/api/MainSolver.h

@@ -264,7 +264,6 @@ class MainSolver {
     Theory & getTheory() { return *theory; }
     Theory const & getTheory() const { return *theory; }
     TermMapper & getTermMapper() const { return *term_mapper; }
-    PartitionManager & getPartitionManager() { return pmanager; }
 
     // TODO: inefficient
     vec<PTRef> getCurrentAssertionsViewImpl() const { return getCurrentAssertions(); }
@@ -334,6 +333,7 @@ class MainSolver {
     vec<PTRef> frameTerms;
     std::size_t firstNotPreprocessedFrame = 0;
     std::size_t insertedAssertionsCount = 0;
+    std::size_t preprocessedAssertionsCount = 0;
     std::vector<std::size_t> preprocessedAssertionsCountPerFrame;
 };