Small refactoring of partition information

[blishko]

This PR proposes moving the partition information of clauses directly to the proof structure, as this is needed only for building resolution proof for interpolation.
This change allows to clean up the interface of adding clauses to the SAT solver and removes the dependency of Cnfizer on PartitionManager.

[aehyvari]

This looks good!

I'm thinking about the interface though. Could we pass the partitionIndex as an argument to the newSMTClause methods in {Core,Simp}SMTSolver, and therefore also at insertFormula in MainSolver? I think it would be good not to rely on the state in the SMT solver. For instance the partitions of true and false are not very explicit in the current implementation, and the partitions of the satelite-simplified clauses (which we hopefully are not doing) would be explicit. This was probably an issue in the old code already, but could be good to discuss at this PR. I made quickly the change on my local working directory, and could commit it here if you want.

[aehyvari]

Change to logsProofForInterpolation()?

[aehyvari]

This old code seems a little redundant. Maybe we could fix it on this commit as well.

[blishko]

I agree that the interface is not entirely clear.
The partitioning is only needed for interpolation and needs to be synchronized with the interpolation interface where user specifies the binary partitioning. The question is how to keep in sync what the user thinks forms a partition of given index and what solvers thinks about which clauses belong to partition of the given index.
There is exactly this problem of where the clauses true and not false should belong, or any of these 'satellite clauses' (which are now disabled).

For some reason I don't like the idea of explicitly passing the index in the addClause methods, as under normal circumstances, the solver does not care about the partitions.

If you have some proposal, maybe commit to a separate branch and send a link?

Now I feel that it might be good to change the interpolation interface to not use ipartitions_texplicitly, but use something along the interpolation standard proposal, to use the formulas directly to specify the partitioning. This would free us to implement the actual handling of partitioning in different ways.