f312170f21
This PR implements cooper conflict resolution in the cutsat procedure.
It also fixes several bugs in the proof term construction. We still need
to add more tests, but we can already solve the following example that
`omega` fails to solve:
```lean
example (x y : Int) :
27 ≤ 11*x + 13*y →
11*x + 13*y ≤ 45 →
-10 ≤ 7*x - 9*y →
7*x - 9*y ≤ 4 → False := by
grind
```
|
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| bv_relation.lean | ||
| common.sh | ||
| lean-toolchain | ||