Split simplifyFormulas to sub-functions

[Tomaqa]

This is just a refactoring. The behavior or performance should not change.

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

Also added preprocess as an alias to simplifyFormulas.

[Tomaqa]

Also renamed internal MainSolver::firstNotSimplifiedFrame->firstNotPreprocessedFrame and insertedFormulasCount->insertedAssertionsCount

[Tomaqa]

Comparison with master, 2-minute timeout, QF_LRA, (non-|)incremental + unsat cores (i.e. unsat non-incremental and producing resolution proofs, hence tracking partitions).

2025-v2.9.2-21-gfe95a928.scatter.pdf

[Tomaqa]

To check also the case when trackPartitions() is true, I relied on unsat cores. However, they are only a subset of non-incremental benchmarks, and we also do not really care about the unsat core computation itself. Hence, I instead add more comparisons of only (non-|)incremental benchmarks, but using a hacked implementation that forces trackPartitions() to true. In the scatter plots below, these correspond to the versions with the -dirty suffix.

I again compare the new (v2.9.2-23-g883d2889) against master (v2.9.2-21-gfe95a928), using the 2-minute timeout, QF_LRA, (non-|)incremental.

Master -dirty vs. new -dirty:
2025-v2.9.2-21-gfe95a928-dirty_v2.9.2-23-g883d2889-dirty.scatter.pdf
That is, the behavior does not change when tracking partitions. In the previous scatter plot, I showed that it also does not change when not tracking partitions.

For completeness, I show that tracking partitions matters.
This is a comparison of master vs. master -dirty:
2025-v2.9.2-21-gfe95a928_v2.9.2-21-gfe95a928-dirty.scatter.pdf
It is almost the same when comparing the new vs. the new -dirty:
2025-v2.9.2-23-g883d2889_v2.9.2-23-g883d2889-dirty.scatter.pdf
As expected, tracking partitions overall harms the performance, although sometimes it is better, probably due to instability.

[BritikovKI]

It is a function which calls one function, why not use original function call?
(Also imho name's a bit too long)

[Tomaqa]

This way, it is clearer that this part must not be omitted. Without the auxiliary function, it could be missed. Besides, connecting the theory and preprocessor is not completely useless, prevents code duplication.

[BritikovKI]

I'm not sure I understand 🤔 Why would one assume this part can be ommited? It can also be highlighted by the comment in the code, what theory->afterPreprocessing does...

Can you elaborate on code duplication point? Because as I understand a single function function call is being replaced by a different function call + additional lines of code in MainSolver.cc and MainSolver.h

[BritikovKI]

I think it's too big of a name... I see that there is a naming convention, but that can be a pain to use inside the code...
Functionality can be described with a comment or documentation, but using this long func names feels a bit too much 🤔

Why not
initialPreprocessing
corePreprocessing
finalPreprocessing
or smth shorter...

[Tomaqa]

I wanted to use sth. like that, but I do not like that corePreprocessing (or body or whatever) would be just that one call, which is actually just a minor step within the whole process. The whole reason why it is separated is that in preprocessFormulasPerPartition, both preprocessFormulaBeforeFinalTheoryPreprocessing and preprocessFormulaAfterFinalTheoryPreprocessing are called on each particular frame formula, while preprocessFormulaDoFinalTheoryPreprocessing is called just once. In preprocessFormulasDefault, i.e., in preprocessFormula, all is called just once (because we mix all formulas into one conjunction).

What could potentially work is preprocessFormulaBegin, preprocessFormulaMiddle, preprocessFormulaEnd. This way, middle does not make the impression that it is the main part.
What do you think?

[BritikovKI]

I like your idea here!
Middle looks a little bit off, but I don't have a better idea for the name
There is also an option to ask LLM for the recommendation))

[BritikovKI]

Why not lambda?
(Not important, but tbh I just like lambdas 😊)

[Tomaqa]

To not use the variable at all if push_id == 0 (i.e., do not even initialize it on the stack). Maybe it would be worth to also add the [[maybe_unused]] attribute to the variable, to make it more explicit.

[BritikovKI]

Hmm, wouldn't it get optimized by compiler?
Main reason I like lambda is because it looks a little bit more compact here, it is not a major point of contention though...

[BritikovKI]

Overall 6 functions might be a little bit complex to navigate 🤔
To fully understand the code one needs to go back and forth, scrolling to the right func, then scrolling back...
This is the Software Engineering discussion but I'm supportive of function use if:
(1.) There is a piece of code that is used in many places or
(2.) There is a complex piece of code which serves one functional purpose...

[Tomaqa]

I need to use preprocessFormula later as a separate function in a different PR (#873).
Maybe encapsulating all related stuff into a class (e.g. PreprocessFormula) would help readability?

[BritikovKI]

I need to use preprocessFormula later as a separate function in a different PR (#873). Maybe encapsulating all related stuff into a class (e.g. PreprocessFormula) would help readability?

I think it actually can improve readability, especially if separated and split into private/public, to see which functions will be used outside and which are purely internal...