Add new simplifier rules (#8902)

* Add rewrite rules

* remove unnecessary parentheses

* uncomment

Author: stevenraphael

src/Simplify_Sub.cpp

@@ -384,10 +384,12 @@ Expr Simplify::visit(const Sub *op, ExprInfo *info) {
          (no_overflow_int(op->type) && EVAL_IN_LAMBDA  //
           (rewrite(c0 - (c1 - x) / c2, (fold(c0 * c2 - c1 + c2 - 1) + x) / c2, c2 > 0) ||
            rewrite(c0 - (x + c1) / c2, (fold(c0 * c2 - c1 + c2 - 1) - x) / c2, c2 > 0) ||
+           rewrite(x - x / c0, (x * fold(c0 - 1) + fold(c0 - 1)) / c0, c0 > 0) ||
            rewrite(x - (x + y) / c0, (x * fold(c0 - 1) - y + fold(c0 - 1)) / c0, c0 > 0) ||
            rewrite(x - (x - y) / c0, (x * fold(c0 - 1) + y + fold(c0 - 1)) / c0, c0 > 0) ||
            rewrite(x - (y + x) / c0, (x * fold(c0 - 1) - y + fold(c0 - 1)) / c0, c0 > 0) ||
            rewrite(x - (y - x) / c0, (x * fold(c0 + 1) - y + fold(c0 - 1)) / c0, c0 > 0) ||
+           rewrite(x / c0 - x, (x * fold(1 - c0)) / c0) ||
            rewrite((x + y) / c0 - x, (x * fold(1 - c0) + y) / c0) ||
            rewrite((y + x) / c0 - x, (y + x * fold(1 - c0)) / c0) ||
            rewrite((x - y) / c0 - x, (x * fold(1 - c0) - y) / c0) ||

test/correctness/simplify.cpp

@@ -432,6 +432,8 @@ void check_algebra() {
     check((y + (x / 3 * 3)) + x % 3, x + y);
     check((y + (x / 3)) * 3 + x % 3, y * 3 + x);
 
+    check(x - (x / 2), (x + 1) / 2);
+    check((x / 3) - x, (x * -2) / 3);
     check(x / 2 + x % 2, (x + 1) / 2);
     check(x % 2 + x / 2, (x + 1) / 2);
     check(((x + 1) / 2) * 2 - x, x % 2);