Merge pull request #8506 from diffblue/simplify-bitxnor

simplify bitxnor
diffblue · Nov 17, 2024 · e8d3409 · e8d3409
2 parents 0db546b + 8f55154
commit e8d3409
Show file tree

Hide file tree

Showing 3 changed files with 44 additions and 6 deletions.
diff --git a/src/util/bitvector_expr.h b/src/util/bitvector_expr.h
@@ -190,6 +190,41 @@ inline bitxor_exprt &to_bitxor_expr(exprt &expr)
   return static_cast<bitxor_exprt &>(expr);
 }
 
+/// \brief Bit-wise XNOR
+class bitxnor_exprt : public multi_ary_exprt
+{
+public:
+  bitxnor_exprt(exprt _op0, exprt _op1)
+    : multi_ary_exprt(std::move(_op0), ID_bitxnor, std::move(_op1))
+  {
+  }
+};
+
+template <>
+inline bool can_cast_expr<bitxnor_exprt>(const exprt &base)
+{
+  return base.id() == ID_bitxnor;
+}
+
+/// \brief Cast an exprt to a \ref bitxnor_exprt
+///
+/// \a expr must be known to be \ref bitxnor_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref bitxnor_exprt
+inline const bitxnor_exprt &to_bitxnor_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_bitxnor);
+  return static_cast<const bitxnor_exprt &>(expr);
+}
+
+/// \copydoc to_bitxnor_expr(const exprt &)
+inline bitxnor_exprt &to_bitxnor_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_bitxnor);
+  return static_cast<bitxnor_exprt &>(expr);
+}
+
 /// \brief Bit-wise AND
 class bitand_exprt : public multi_ary_exprt
 {

diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
@@ -950,9 +950,10 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
     {
       irep_idt op_id = expr.op().id();
 
-      if(op_id==ID_plus || op_id==ID_minus || op_id==ID_mult ||
-         op_id==ID_unary_minus ||
-         op_id==ID_bitxor || op_id==ID_bitor || op_id==ID_bitand)
+      if(
+        op_id == ID_plus || op_id == ID_minus || op_id == ID_mult ||
+        op_id == ID_unary_minus || op_id == ID_bitxor || op_id == ID_bitxnor ||
+        op_id == ID_bitor || op_id == ID_bitand)
       {
         exprt result = expr.op();
 
@@ -2949,9 +2950,9 @@ simplify_exprt::resultt<> simplify_exprt::simplify_node(const exprt &node)
   {
     r = simplify_bitnot(to_bitnot_expr(expr));
   }
-  else if(expr.id()==ID_bitand ||
-          expr.id()==ID_bitor ||
-          expr.id()==ID_bitxor)
+  else if(
+    expr.id() == ID_bitand || expr.id() == ID_bitor || expr.id() == ID_bitxor ||
+    expr.id() == ID_bitxnor)
   {
     r = simplify_bitwise(to_multi_ary_expr(expr));
   }

diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
@@ -745,6 +745,8 @@ simplify_exprt::simplify_bitwise(const multi_ary_exprt &expr)
       f = [](bool a, bool b) { return a || b; };
     else if(new_expr.id() == ID_bitxor)
       f = [](bool a, bool b) { return a != b; };
+    else if(new_expr.id() == ID_bitxnor)
+      f = [](bool a, bool b) { return a == b; };
     else
       UNREACHABLE;