Moved IteHandler into the preprocessing pipeline

[Tomaqa]

Fixes TermNames to also consider the mapping of internal terms to original user terms.
So far, I have only identified IteHandler to change the PTRef of the inserted formula in insertFormula and at the same time store it into the assertions, so that the changed PTRef is retrieved via getting the assertions or via PartitionaManager.
Without this, the UnsatCoreBuilder would consider some terms to be unnamed because it would not recognize them.

Resolves #857

[blishko]

Seems good, but I am not sure I fully understand the underlying problem.
There should be some very minimal example to reproduce the problem, no?
Can we find it and use it as the regression test, instead of these large files?
It would also help me to understand the problem properly.
ITEHandler has always been a bit of a hack.
Wouldn't it help if we resolved the TODO associated with its usage, and incorporate the ite processing to the preprocessing pipeline?

[Tomaqa]

Wouldn't it help if we resolved the TODO associated with its usage, and incorporate the ite processing to the preprocessing pipeline?

Are you referring to the comment at IteHandler.cc:45?

I am not too familiar with how the overall preprocessing and substitutions work. But I assume that in general, the top-level asserted PTRefs can be internally replaced by a different, potentially better term. For this reason, I introduced InternalToUserTermMap such that MainSolver can use it at whatever place and time.

I am not sure how this concept changes with incorporating or not incorporating ITEs into the preprocessing pipeline.

[Tomaqa]

There should be some very minimal example to reproduce the problem, no?

I identified some very small examples and added them. I believe that the problem appears when the top-level assertion is an ITE. I will also try to make some similar unit tests.

[Tomaqa]

I also included unit tests. As a consequence, I also added to possibility to retrieve the names from NamedUnsatCore and added several tests on this in the unit tests.

Even with the fix, we correctly handle the unsat cores such that the names are kept, but not the terms themselves. See e.g. test_UnsatCore.cc:395 (in the Bool_Trivial_ITE test).
Hence, for example, in the case of full cores where the names are ignored, the user cannot track which of the terms he/she asserted are kept/discarded from the core. That does not seem right, but I can fix it by storing the original terms instead of the internals into the core.

[Tomaqa]

My current feeling is that the transformation of internal terms to the original should already happen inside of api/PartitionManager.h:51 :

inline std::vector<PTRef> getPartitions() const { return partitionInfo.getTopLevelFormulas(); }

I am not sure if this is always the desired behavior, or if it should be optional - a parameter in PartitionManager would allow to do the mapping.
But since getPartitions() refers to top-level assertions, I think it should refer to the original PTRef provided to the insertFormula.

[Tomaqa]

I checked that the current fix resolves all the issues reported in #857 regarding the named terms, including minimal cores, except the cases reported in #859 where the issue is probably not related to the one discussed here.

However, the issue with not identifying the original PTRefs as a part of the core remains unresolved.

[Tomaqa]

ITEHandler has always been a bit of a hack. Wouldn't it help if we resolved the TODO associated with its usage, and incorporate the ite processing to the preprocessing pipeline?

I moved the use of the IteHandler into preprocessing, and it seems to resolve the issues.
Now, the partition manager knows the mapping and should always return the original PTRefs - which comprises both unsat cores and interpolants, which both could have returned internal PTRef, thus unknown to the user.

[Tomaqa]

(#859 seems to remain unresolved - but it can be caused by something completely different.)

[blishko]

Can you split this PR?
Can the changes to the ITE preprocessing be separated from the unsat-core changes?

[Tomaqa]

Can you split this PR? Can the changes to the ITE preprocessing be separated from the unsat-core changes?

I do not see the benefit here.
There are no tests that would identify the wrong behavior except for the new ones related to unsat cores.
Prepending the IteHandler as a standalone PR would prevent us from seeing that there was a point when the tests were failing.

[Tomaqa]

I would like to keep the order of having the tests first and the patch later.
Having this order, it is not possible to split the PR, because the first part would fail the tests without the final patch.

[blishko]

I have to refresh my memory why IteHandler needs a number.
I am not sure about the simplifiedFormulasCount.

What I don't quite like is that now, the same original formula can be preprocessed with IteHandler multiple times.
I am afraid this could lead to some performance regression in incremental solving.

[blishko]

Why not apply IteHandler once on the conjunction?
Wouldn't that be better?

[Tomaqa]

I have not realized that it works recursively. Yes, it's better!

[blishko]

Do we need this file in tests?
One, the core issue should be caught by the smaller tests, no?
Two, this one seems brittle, if the minimal unsat core is just smtcomp43 it seems weird to assert that OpenSMT will always find the unsat core consisting of

(
smtcomp14
smtcomp21
smtcomp43
)

[Tomaqa]

Yes, I can remove it.
Regarding how stable the tests are, this is a general issue that applies to all unsat cores and models. Even the "minimal" (irreducible) cores can be computed differently. Every time we make a change in the solver, we may need to update the expected results, or we will have to add support for multiple possible outputs in regression tests.

[Tomaqa]

I have to refresh my memory why IteHandler needs a number.

The only purpose is for the name of the auxiliary '.ite' variable.

What I don't quite like is that now, the same original formula can be preprocessed with IteHandler multiple times. I am afraid this could lead to some performance regression in incremental solving.

I will need to handle this more thoroughly. I think it would be best to first implement an array of counters for remembering how many formulas per assertion level have been preprocessed, to easily detect that the preprocessing has already taken place, even with arbitrary pushes and pops.

[Tomaqa]

Can you split this PR? ...

I moved one of the less related commits into a separate PR -> #887

[Tomaqa]

What I don't quite like is that now, the same original formula can be preprocessed with IteHandler multiple times.

I will need to handle this more thoroughly. I think it would be best to first implement an array of counters ...

Counters implemented in #889.

Now IteHandler is not being called multiple times: if trackPartitions(), then it is guaranteed thanks to the counters, not preprocessing already preprocessed formulas. In the other case, all frame formulas are always put into conjunction, potentially preprocessing some formulas again. We can use caching, but I realized that since the conjunctions are always different, there may never be a cache hit. We may instead separately remember the previous preprocessed formula and use it, and apply IteHandler only on the new part of the formula.