feat: Partition goals extract from InstCombine into success/failure based on whether the goal is a clean QF_BV goal

[bollu]

The purpose of extract_goals is to give us clean QF_BV goals. So, we test this by running the file with open BitVec and no imports. This gives us:

(venv) bollu@grosser-7950x3d ~/m/e/s/S/P/I/t/goals (extract-goals-partition-success-and-failure)> ls failure/ | wc -l
3870
(venv) bollu@grosser-7950x3d ~/m/e/s/S/P/I/t/goals (extract-goals-partition-success-and-failure)> ls success/ | wc -l
4108
(venv) bollu@grosser-7950x3d ~/m/e/s/S/P/I/t/goals (extract-goals-partition-success-and-failure)> python3
Python 3.12.3 (main, Aug 14 2025, 17:47:21) [GCC 13.3.0] on linux
Type "help", "copyright", "credits" or "license" for more information.
>>> 3870 + 4108
7978

@alexkeizer , the ball is now in your court to improve simp_alive_peephole so that poison semantics no longer remains :)

[alexkeizer]

I'm not sure what you want me to review exactly; I'm not familiar enough with the python bits to say sensible things beyond that I support the move to pure bitvector stuff.

The CI failing is presumably caused by the fact that we sometimes still have PoisonOr remaining in the goals, or is there something else to be fixed there?

[bollu]

@alexkeizer Well, I wanted to see what you thought of the change, and that you agree that these goals ought to be QF_BV goals

[bollu]

(venv) bollu@grosser-7950x3d ~/m/e/s/S/P/I/t/goals (extract-goals-partition-success-and-failure)> ls failure/ | wc -l
2332
(venv) bollu@grosser-7950x3d ~/m/e/s/S/P/I/t/goals (extract-goals-partition-success-and-failure)> ls success/ | wc -l
5646
(venv) bollu@grosser-7950x3d ~/m/e/s/S/P/I/t/goals (extract-goals-partition-success-and-failure)> python3
Python 3.12.3 (main, Aug 14 2025, 17:47:21) [GCC 13.3.0] on linux
Type "help", "copyright", "credits" or "license" for more information.
>>> 5646 + 2332
7978

[bollu]

(venv) bollu@grosser-7950x3d ~/m/e/s/S/P/I/t/goals (extract-goals-partition-success-and-failure)> git rev-parse HEAD
8d4bef980608c4cc5ce7e70c975db3ee55afdc85
(venv) bollu@grosser-7950x3d ~/m/e/s/S/P/I/t/goals (extract-goals-partition-success-and-failure)> ls success/ | wc -l
7978
(venv) bollu@grosser-7950x3d ~/m/e/s/S/P/I/t/goals (extract-goals-partition-success-and-failure)> ls failure/ | wc -l
0

[tobiasgrosser]

I am not sure we want this split. AFAIU all goals are pure bitvector goals, no?

[bollu]

@tobiasgrosser they're not necessarily: If simp_alive_peephole has a bug, we can get goal states that are not pure QF_BV, but instead goal states that contain LLVM-level concepts.

The output of the files is the goals that are produced by simp_alive_peephole. If simp_alive_peephole is incomplete, some goals that are produced could have LLVM-level semantic objects floating around.

For example, Until I paired with Alex today, the goals used to have unrelated LLVM-level PoisonOr.Refinements.

We now have every file in success, which means that simp_alive_peephole preprocessing is good enough to produce pure QF_BV goals with no LLVM leaking through. I would like to retain the split into success/ and failure. This gives @alexkeizer the flexibility to evolve simp_alive_peephole preprocessing, while allowing me to easily triage what the failures are when it comes to going from lean-mlir -> QF_BV.

[alexkeizer]

To be precise: the goals in question were of the form "value is-refined-by poison", which of course is equivalent to False; these goals were still solvable by bv_decide because the (contradictory) hypotheses were pure BV statements, but, these goals still required the PoisonOr stuff to be imported to make sense. The change was to add the rewrite to False to the simpset.

More generally, ensuring all goals are purely BV will make it easier to add goals that come from other dialects (e.g., LLVM + memory) without having to add all dialects to the imports of each test case, so this is a nice change!