86dc07c20d
This PR improves support for nonlinear monomials in `grind cutsat`. For example, given a monomial `a * b`, if `cutsat` discovers that `a = 2`, it now propagates that `a * b = 2 * b`. Recall that nonlinear monomials like `a * b` are treated as variables in `cutsat`, a procedure designed for linear integer arithmetic. Example: ```lean example (a : Nat) (ha : a < 8) (b c : Nat) : 2 ≤ b → c = 1 → b ≤ c + 1 → a * b < 8 * b := by grind example (x y z w : Int) : z * x * y = 4 → x = z + w → z = 1 → w = 2 → False := by grind ```
32 lines
1.1 KiB
Text
32 lines
1.1 KiB
Text
example (x y z w : Int) : z * x * y = 4 → x = z + w → z = 1 → w = 2 → False := by
|
|
grind -ring
|
|
|
|
example (x y z w : Int) : y * z * x = 4 → x = z + w → z = 1 → w = 2 → False := by
|
|
grind -ring
|
|
|
|
example (x y z w : Int) : y * z * x * w = 4 → x = 0 → False := by
|
|
grind -ring
|
|
|
|
example (x y z w : Int) : x = z + w → z = 1 → w = 2 → z * x * y = 4 → False := by
|
|
grind -ring
|
|
|
|
example (x y z : Int) : x = 3 → z = 1 → z * x * y = 4 → False := by
|
|
grind -ring
|
|
|
|
example (x y z w : Int) : x = 1 → y = 2 → z = 3 → w = 4 → x * y * z * w = 24 := by
|
|
grind -ring
|
|
|
|
example (x y z w : Int) : 1 ≤ x → x < 2 → y = 2 → z = 3 → w = 4 → x * y * z * w = 24 := by
|
|
grind -ring
|
|
|
|
example (x y z w : Int) : x = 1 → y = 2 → z = 3 → w = 4 → x * (y * z) * w = 24 := by
|
|
grind -ring
|
|
|
|
example (x y : Int) : 1 ≤ x → x ≤ 1 → 2 ≤ y → y ≤ 2 → x * y = 2 := by
|
|
grind -ring
|
|
|
|
example (a : Nat) (ha : a < 8) (b : Nat) (hb : b = 2) : a * b < 8 * b := by
|
|
grind -ring
|
|
|
|
example (a : Nat) (ha : a < 8) (b c : Nat) : 2 ≤ b → c = 1 → b ≤ c + 1 → a * b < 8 * b := by
|
|
grind -ring
|