From b8f18021875c299d28638e7321ef8cd130c56082 Mon Sep 17 00:00:00 2001 From: Steven Raphael Date: Fri, 12 Dec 2025 02:46:29 -0500 Subject: [PATCH 1/3] Add rewrite rules --- src/Simplify_Sub.cpp | 2 ++ test/correctness/simplify.cpp | 2 ++ 2 files changed, 4 insertions(+) diff --git a/src/Simplify_Sub.cpp b/src/Simplify_Sub.cpp index 828cbeec2b2d..0b525f306d69 100644 --- a/src/Simplify_Sub.cpp +++ b/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) || diff --git a/test/correctness/simplify.cpp b/test/correctness/simplify.cpp index 08119357fb4b..d1e31804292a 100644 --- a/test/correctness/simplify.cpp +++ b/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); From c1c944402838e6ba204b6446133af58b4dd1ff3d Mon Sep 17 00:00:00 2001 From: Steven Raphael Date: Fri, 12 Dec 2025 06:23:43 -0500 Subject: [PATCH 2/3] remove unnecessary parentheses --- src/Simplify_Sub.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Simplify_Sub.cpp b/src/Simplify_Sub.cpp index 0b525f306d69..7e5b4e316926 100644 --- a/src/Simplify_Sub.cpp +++ b/src/Simplify_Sub.cpp @@ -384,12 +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 / 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 / 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) || From 38ecb30e09aa887c50aefa695fa3b20991d383dd Mon Sep 17 00:00:00 2001 From: Steven Raphael Date: Fri, 12 Dec 2025 15:29:00 -0500 Subject: [PATCH 3/3] uncomment --- src/Simplify_Sub.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Simplify_Sub.cpp b/src/Simplify_Sub.cpp index 7e5b4e316926..29bd02c78ed6 100644 --- a/src/Simplify_Sub.cpp +++ b/src/Simplify_Sub.cpp @@ -384,12 +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 / 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 / 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) ||