simplify bitxnor

src/util/bitvector_expr.h

@@ -190,6 +190,41 @@
   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
 {

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));
   }

src/util/simplify_expr_int.cpp

@@ -745,6 +745,8 @@
       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;