53db221124
This PR disables model-based theory combination (`mbtc`) in `grind`'s `NoopConfig`, which is the base configuration used by the derived tactics `lia`, `linarith`, `cutsat`, `order`, and `ring`. Without this fix, these tactics could engage in wasteful reasoning via theory combination, causing them to run for a long time (or hit the deterministic timeout) on problems they are not designed to solve. With this fix, these tactics fail quickly on out-of-scope problems, as expected. Closes #13573.
48 lines
1.8 KiB
Text
48 lines
1.8 KiB
Text
|
|
/-!
|
|
The following nonlinear example should fail quickly without
|
|
a deterministic timeout.
|
|
-/
|
|
|
|
/--
|
|
error: `grind` failed
|
|
case grind
|
|
x1 x2 x3 x4 x5 x6 x7 x8 : Int
|
|
h : ¬x8 = x2
|
|
h_1 : -1 * x2 + 4294967296 * x6 + 4294967296 * x7 + x8 + -1 * ((x3 - 4294967296 * x4) * (x1 - 4294967296 * x5)) = 0
|
|
h_2 : -1 * x2 + 4294967296 * x6 + 4294967296 * x7 + -1 * ((x3 - 4294967296 * x4) * (x1 - 4294967296 * x5)) ≤ 0
|
|
h_3 : x2 + -4294967296 * x6 + -4294967296 * x7 + (x3 - 4294967296 * x4) * (x1 - 4294967296 * x5) + -4294967295 ≤ 0
|
|
h_4 : 4294967296 * x6 + -1 * ((x3 - 4294967296 * x4) * (x1 - 4294967296 * x5)) ≤ 0
|
|
h_5 : -4294967296 * x6 + (x3 - 4294967296 * x4) * (x1 - 4294967296 * x5) + -4294967295 ≤ 0
|
|
h_6 : -1 * x1 + 4294967296 * x5 ≤ 0
|
|
h_7 : x1 + -4294967296 * x5 + -4294967295 ≤ 0
|
|
h_8 : -1 * x3 + 4294967296 * x4 ≤ 0
|
|
h_9 : x3 + -4294967296 * x4 + -4294967295 ≤ 0
|
|
h_10 : -1 * x2 ≤ 0
|
|
h_11 : x2 + -4294967295 ≤ 0
|
|
h_12 : x3 * x1 + -4294967295 ≤ 0
|
|
h_13 : -1 * x3 ≤ 0
|
|
h_14 : x2 + x3 * x1 + -4294967295 ≤ 0
|
|
h_15 : -1 * x1 + 8 ≤ 0
|
|
h_16 : x1 + -4294967295 ≤ 0
|
|
⊢ False
|
|
-/
|
|
#guard_msgs in
|
|
example (x1 x2 x3 x4 x5 x6 x7 x8 : Int) :
|
|
¬x8 = x2 →
|
|
x8 = x2 + ((x3 - 2 ^ 32 * x4) * (x1 - 2 ^ 32 * x5) - 2 ^ 32 * x6) - 2 ^ 32 * x7 →
|
|
0 ≤ x2 + ((x3 - 2 ^ 32 * x4) * (x1 - 2 ^ 32 * x5) - 2 ^ 32 * x6) - 2 ^ 32 * x7 →
|
|
x2 + ((x3 - 2 ^ 32 * x4) * (x1 - 2 ^ 32 * x5) - 2 ^ 32 * x6) - 2 ^ 32 * x7 < 2 ^ 32 →
|
|
0 ≤ (x3 - 2 ^ 32 * x4) * (x1 - 2 ^ 32 * x5) - 2 ^ 32 * x6 →
|
|
(x3 - 2 ^ 32 * x4) * (x1 - 2 ^ 32 * x5) - 2 ^ 32 * x6 < 2 ^ 32 →
|
|
0 ≤ x1 - 2 ^ 32 * x5 →
|
|
x1 - 2 ^ 32 * x5 < 2 ^ 32 →
|
|
0 ≤ x3 - 2 ^ 32 * x4 →
|
|
x3 - 2 ^ 32 * x4 < 2 ^ 32 →
|
|
0 ≤ x2 →
|
|
x2 < 2 ^ 32 → x3 * x1 < 2 ^ 32 →
|
|
0 ≤ x3 →
|
|
x2 + x3 * x1 < 2 ^ 32 → 8 ≤ x1 →
|
|
x1 < 2 ^ 32 →
|
|
False := by
|
|
lia -verbose
|