experiment with custom branching solver approach

[daejunpark]

This PR records experimental results from testing a custom branching solver approach.

The core idea was to implement a lightweight custom solver to handle branching decisions. This seemed potentially feasible, given that our current 1ms solver timeout doesn't permit much reasoning from SMT solvers. A custom solver could also enable alternative path exploration strategies; currently, we're limited to depth-first search due to the need to minimize solver context creation and switching by sharing a single solver instance.

Several quick custom solving strategies were prototyped. Initial results were promising, with many benchmark tests passing. However, some tests failed, revealing that certain cases require full SMT reasoning, like e-graphs and bitvectors, which are beyond the capabilities of this lightweight approach.

Some examples where the quick custom solver fails to prove unsat:

• inequality: x == 0 vs not (x >= 0)
• congruence closure: x == 2 vs map[x] == 0 and map[2] == 1
• bitvector: extract(31, 31, x) == 0 vs x != 0 and extract(i, i, x) == 0 for all 0 <= i <= 30

Some components of the custom solver have already been merged into main. The remaining experimental work is documented in this PR for future reference.