Optimize SAT assumption handling and Saturation queue

[EpsilonPhoenix]

No description provided.

[quickbeam123]

Some of the changes are hard to understand without an accompanying justification (and there seem to be more changes than commits). Could you please explain the reasoning behind each individual fix/update/change?

[EpsilonPhoenix]

Some of the changes are hard to understand without an accompanying justification (and there seem to be more changes than commits). Could you please explain the reasoning behind each individual fix/update/change?

1. Indexing/ClauseCodeTree.cpp
   Changed literal-order optimization to reuse compiled literal-matching code during sharing checks, with lazy compilation and cleanup.
   Reason: reduces repeated compile & match overhead.

2. Indexing/ClauseCodeTree.hpp
   Updated evalSharing to accept precompiled the literal code (CodeStack&).
   Reason: needed for the ClauseCodeTree reuse optimization.

3. Kernel/ClauseQueue.cpp
   Bounded random skip-list height by MAX_HEIGHT.
   Reason: avoids overshooting queue height.

4. SAT/MinisatInterfacing.cpp
   Optimized Minisat interfacing by reusing buffers, preallocating where possible, and restructuring premise minimization mapping to use direct indexed storage.
   Reason: reduces memory overhead and makes premise minimization more consistent.

5. SAT/MinisatInterfacing.hpp
   Added a reusable clause buffer member used by Minisat clause insertion.
   Reason: needed for the Minisat buffer reuse optimization.

6. SAT/SATClause.cpp
   Reworked duplicate literal removal into a compaction pass that handles duplicate groups and tautology detection.
   Reason: improves correctness on edge cases and simplifies normalization.

7. SAT/SATSolver.cpp
   Changed failed assumption minimization to reuse one assumptions buffer and remove/restore assumptions in place instead of rebuilding each iteration.
   Reason: reduces repeated work in minimization loops.

8. Saturation/AWPassiveClauseContainers.cpp
   Reworked simulation bookkeeping by tracking remaining clauses and syncing simulation cursors before selection/limit derivation.
   Reason: makes simulation faster under queue deletions.

9. Saturation/AWPassiveClauseContainers.hpp
   Added declarations for simulation bookkeeping (_simulationRemaining and cursor sync helper).
   Reason: needed for the AW simulation optimization.

10. Saturation/LRS.cpp
    Added denominator checks before time & instruction estimate divisions.
    Reason: avoids divide-by-zero (values may be finicky in runtime?).

11. Saturation/PredicateSplitPassiveClauseContainers.cpp
    Added a per-clause cache for best queue index, reused cached routing in add/remove/pop/limit paths, and limited layered removals to relevant queue ranges.
    Reason: avoids repeated queue-routing recomputation and unnecessary queue operations.

12. Saturation/PredicateSplitPassiveClauseContainers.hpp
    Added cache storage and helper declarations for best-queue index lifecycle.
    Reason: needed for the split-queue routing cache optimization.

13. Saturation/SaturationAlgorithm.cpp
    Reserved queue vector capacity before constructing split-queue layers.
    Reason: avoids repeated vector reallocations during queue construction.

14. UnitTests/tSATClause.cpp
    Added tests for duplicate group normalization and tautology edge cases.
    Reason: validates SAT clause normalization.

15. UnitTests/tSATSolver.cpp
    Expanded tests to validate assumption minimization and premise minimization.
    Reason: adds coverage for the SAT solver & interfacing changes.

These changes should hopefully not affect outputs in any way; only removing redundant operations.