Further Optimize Initial Transposition

[SSoelvsten]

The initial transposition sweep seems to be an endless ground for optimization in many cases.

• From Remove all fancy transposition computations #654 we unexpectedly notice that the constant involved in a simple transposition is small enough to offset any potential cost of an additional nested sweep.
• From Add terminal pruning for initial transposition sweep #653 we see that terminal pruning during quantification can be worth it.
• From Internal/quantify/terminal heuristic (3) #647 we see that a single partial quantification is really good in some cases.

Which leads to more questions:

• Is the constant involved in a simpler Restrict-like sweep better?
  • Is it enough to not have to think about a transposition being faster?
    ANSWER: There is still a 2% overhead.
  • What is a heuristic to enable terminal pruning?
    HYPOTHESIS: look at the terminal count and possibly the width/nodes ratio.
• Is there any case, where deepest quantification is good?
  • If so, what is particular to these instances?
    HYPOTHESIS: this would be if the deepest variable is very shallow.
• Is partial quantification good/bad due to it shuffling the children around regardless of the original assignment?
  • Either way, what is a proper heuristic to enable a single partial quantification?

For implementation(s) of the above, we may want to add the following.

• Replace the __quantify__get_deepest with a __quantify__pred_profile that doesn't stop early but instead records a lot of information.
  • Total number of nodes.
  • Total number of variables.
  • Total number of variables quantified.
    • + Number of deep variables (last N/3 and beneath the widest level)
    • + Number of shallow variables (first N/3 and above the widest level)
  • The deepest to-be quantified variable (independent of the above "deep").
    • + the number of nodes beneath it.
    • + width of this level.
  • The shallowest to-be quantified variable (independent of the above "shallow").
    • + the number of nodes beneath it.
    • + width of this level.
  • The widest to-be quantified variable.
    • + the number of nodes beneath it.
    • + width of this level.
  • The narrowest to-be quantified variable.
    • + the number of nodes beneath it.
    • + width of this level.
  • Min/max distance between quantified variables.
• The __quantify__max_partial_sweeps should also use this profile instead, instead of reopening the file.