Further Optimize Initial Transposition

[SSoelvsten]

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

• From #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 #653 we see that terminal pruning during quantification can be worth it.
• From #647 we see that a single partial quantification is really good in some cases.

Which leads to more questions:

• [x] Is the constant involved in a simpler Restrict-like sweep better?
  • [x] 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.

• [x] Replace the __quantify__get_deepest with a __quantify__pred_profile that doesn't stop early but instead records a lot of information.
  • [x] Total number of nodes.
  • [x] Total number of variables.
  • [x] 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)
  • [x] The deepest to-be quantified variable (independent of the above "deep").
    • + the number of nodes beneath it.
    • + width of this level.
  • [x] The shallowest to-be quantified variable (independent of the above "shallow").
    • + the number of nodes beneath it.
    • + width of this level.
  • [x] The widest to-be quantified variable.
    • + the number of nodes beneath it.
    • + width of this level.
  • [x] The narrowest to-be quantified variable.
    • + the number of nodes beneath it.
    • + width of this level.
  • [ ] Min/max distance between quantified variables.
• [x] The __quantify__max_partial_sweeps should also use this profile instead, instead of reopening the file.