Do not postpone preprocessing of ITEs when UF is combined with LA

Author: Tomaqa

src/api/MainSolver.cc

@@ -114,6 +114,11 @@ void MainSolver::insertFormula(PTRef fla) {
         throw ApiException("Top-level assertion sort must be Bool, got " + logic.sortToString(logic.getSortRef(fla)));
     }
 
+    if (preprocessItesWhenAsserting()) {
+        assert(not trackPartitions());
+        fla = preprocessFormulaItes(fla, {.perPartition = false}, {.useCache = false});
+    }
+
     if (trackPartitions()) {
         // MB: Important for HiFrog! partition index is the index of the formula in an virtual array of inserted
         // formulas,
@@ -202,6 +207,7 @@ vec<PTRef> MainSolver::preprocessFormulasPerPartition(vec<PTRef> const & frameFo
     for (std::size_t i = context.preprocessedFrameAssertionsCount; i < frameFormulasCount; ++i) {
         PTRef fla = frameFormulas[i];
         PTRef processed = fla;
+        assert(not preprocessItesWhenAsserting());
         // Do not use the cache, it is processed for the first time
         processed = preprocessFormulaItes(processed, context, {.useCache = false});
         processed = preprocessFormulaBeforeFinalTheoryPreprocessing(processed, context);
@@ -257,7 +263,7 @@ PTRef MainSolver::preprocessFormulaItesImpl(PTRef fla, PreprocessingContext cons
 PTRef MainSolver::preprocessFormula(PTRef fla, PreprocessingContext const & context,
                                     PreprocessFormulaItesConfig const & iteConfig) {
     PTRef processed = fla;
-    processed = preprocessFormulaItes(processed, context, iteConfig);
+    if (not preprocessItesWhenAsserting()) { processed = preprocessFormulaItes(processed, context, iteConfig); }
     processed = preprocessFormulaBeforeFinalTheoryPreprocessing(processed, context);
     preprocessFormulaDoFinalTheoryPreprocessing(context);
     processed = preprocessFormulaAfterFinalTheoryPreprocessing(processed, context);

src/api/MainSolver.h

@@ -306,6 +306,8 @@ class MainSolver {
     }
     PTRef preprocessFormulaItesImpl(PTRef, PreprocessingContext const &);
 
+    inline bool preprocessItesWhenAsserting() const;
+
     virtual PTRef preprocessFormula(PTRef, PreprocessingContext const &, PreprocessFormulaItesConfig const &);
     PTRef preprocessFormula(PTRef fla, PreprocessingContext const & context) {
         return preprocessFormula(fla, context, {});
@@ -366,6 +368,21 @@ bool MainSolver::trackPartitions() const {
 
     return false;
 }
+
+bool MainSolver::preprocessItesWhenAsserting() const {
+    // We still must keep tracking the terms which only happens in the pipeline
+    if (trackPartitions()) { return false; }
+
+    // If combining UF, it may be beneficial to introduce the auxiliary ITE variables right away, especially when sat
+    if (logic.hasUFs()) {
+        // In UFLIA, it significantly improves
+        if (logic.hasIntegers()) { return true; }
+        // In UFLRA, it slightly improves, so it is still worth
+        if (logic.hasReals()) { return true; }
+    }
+
+    return false;
+}
 } // namespace opensmt
 
 #endif // MAINSOLVER_H