Recognise OR(X, Not(X)) and Add(X, Not(X)) in arith_simp

These can't be recognised by Ternary or Range due to losing the connection between the bits. The BDD can see this but we don't run that very often.

PiperOrigin-RevId: 597983344

Author: allight

xls/passes/BUILD

@@ -153,6 +153,7 @@ cc_test(
         "//xls/ir:op",
         "//xls/ir:value",
         "//xls/solvers:z3_ir_equivalence",
+        "//xls/solvers:z3_ir_equivalence_testutils",
     ],
 )
 

xls/passes/arith_simplification_pass.cc

@@ -705,6 +705,32 @@ absl::StatusOr<bool> MatchArithPatterns(int64_t opt_level, Node* n) {
     return true;
   }
 
+  //   Or(X, Not(X), ...)  => 1...
+  //
+  // Note that this won't be found through the ternary query engine because
+  // conservatively it determines `not(UNKNOWN) = UNKNOWN`.
+  if (n->op() == Op::kOr && has_inverted_operand()) {
+    XLS_VLOG(2) << "FOUND: replace Or(x, not(x)) with 1...";
+    XLS_RETURN_IF_ERROR(
+        n->ReplaceUsesWithNew<Literal>(Value(Bits::AllOnes(n->BitCountOrDie())))
+            .status());
+    return true;
+  }
+
+  //   Add(X, Not(X)) => 1...
+  //   Add(Not(X), X) => 1...
+  //
+  // Note that this won't be found through the ternary query engine because
+  // conservatively it determines `not(UNKNOWN) = UNKNOWN`.
+  if (n->op() == Op::kAdd && n->operand_count() == 2 &&
+      has_inverted_operand()) {
+    XLS_VLOG(2) << "FOUND: replace Add(x, not(x)) with 1...";
+    XLS_RETURN_IF_ERROR(
+        n->ReplaceUsesWithNew<Literal>(Value(Bits::AllOnes(n->BitCountOrDie())))
+            .status());
+    return true;
+  }
+
   // Xor(x, -1) => Not(x)
   if (n->op() == Op::kXor && n->operand_count() == 2 &&
       IsLiteralAllOnes(n->operand(1))) {

xls/passes/arith_simplification_pass_test.cc

@@ -39,6 +39,7 @@
 #include "xls/passes/optimization_pass.h"
 #include "xls/passes/pass_base.h"
 #include "xls/solvers/z3_ir_equivalence.h"
+#include "xls/solvers/z3_ir_equivalence_testutils.h"
 
 namespace m = ::xls::op_matchers;
 
@@ -48,6 +49,7 @@ namespace {
 constexpr absl::Duration kProverTimeout = absl::Seconds(10);
 
 using status_testing::IsOkAndHolds;
+using ::xls::solvers::z3::ScopedVerifyEquivalence;
 using ::xls::solvers::z3::TryProveEquivalence;
 
 using ::testing::AllOf;
@@ -329,7 +331,7 @@ TEST_F(ArithSimplificationPassTest, SubFallsToZero) {
   FunctionBuilder fb(TestName(), p.get());
   auto param = fb.Param("x", p->GetBitsType(32));
   fb.Subtract(param, param);
-  XLS_ASSERT_OK_AND_ASSIGN(Function* f, fb.Build());
+  XLS_ASSERT_OK_AND_ASSIGN(Function * f, fb.Build());
   ASSERT_THAT(Run(p.get()), IsOkAndHolds(true));
   EXPECT_THAT(f->return_value(), m::Literal(0));
 }
@@ -2177,5 +2179,45 @@ TEST_F(ArithSimplificationPassTest, ShiftLeftOfPowerOfTwo) {
               IsOkAndHolds(true));
 }
 
+TEST_F(ArithSimplificationPassTest, AddInverses) {
+  auto p = CreatePackage();
+  FunctionBuilder fb(TestName(), p.get());
+  BValue p1 = fb.Param("p1", p->GetBitsType(32));
+  fb.Tuple({
+      fb.Add(p1, fb.Not(p1)),
+      fb.Add(fb.Not(p1), p1),
+  });
+  XLS_ASSERT_OK_AND_ASSIGN(Function * f, fb.Build());
+
+  ScopedVerifyEquivalence sve(f);
+  ASSERT_THAT(Run(p.get()), IsOkAndHolds(true));
+
+  EXPECT_THAT(
+      f->return_value(),
+      m::Tuple(m::Literal(Bits::AllOnes(32)), m::Literal(Bits::AllOnes(32))));
+}
+
+TEST_F(ArithSimplificationPassTest, OrInverses) {
+  auto p = CreatePackage();
+  FunctionBuilder fb(TestName(), p.get());
+  BValue p1 = fb.Param("p1", p->GetBitsType(32));
+  BValue p2 = fb.Param("p2", p->GetBitsType(32));
+  fb.Tuple({
+      fb.Or(p1, fb.Not(p1)),
+      fb.Or(fb.Not(p1), p1),
+      fb.Or({p1, p2, fb.Not(p1)}),
+      fb.Or({p1, p2, fb.Not(p2)}),
+  });
+  XLS_ASSERT_OK_AND_ASSIGN(Function * f, fb.Build());
+
+  ScopedVerifyEquivalence sve(f);
+  ASSERT_THAT(Run(p.get()), IsOkAndHolds(true));
+
+  EXPECT_THAT(
+      f->return_value(),
+      m::Tuple(m::Literal(Bits::AllOnes(32)), m::Literal(Bits::AllOnes(32)),
+               m::Literal(Bits::AllOnes(32)), m::Literal(Bits::AllOnes(32))));
+}
+
 }  // namespace
 }  // namespace xls