add nand_exprt, nor_exprt, xnor_exprt, bitnand_exprt, bitnor_exprt

This adds classes for the nand, nor, bitnand, and bitnor expressions,
documenting already existing expressions.

This furthermore adds a class for the new xnor expression, to mirror the
existing bitxnor expression.

The comments clarify the meaning when those expressions are not binary.

Author: kroening

src/util/bitvector_expr.h

@@ -160,6 +160,50 @@ inline bitor_exprt &to_bitor_expr(exprt &expr)
   return static_cast<bitor_exprt &>(expr);
 }
 
+/// \brief Bit-wise NOR
+///
+/// When given one operand, this is equivalent to the bit-wise negation.
+/// When given three or more operands, this is equivalent to the bit-wise
+/// negation of the bitand expression with the same operands.
+class bitnor_exprt : public multi_ary_exprt
+{
+public:
+  bitnor_exprt(exprt _op0, exprt _op1)
+    : multi_ary_exprt(std::move(_op0), ID_bitnor, std::move(_op1))
+  {
+  }
+
+  bitnor_exprt(exprt::operandst _operands, typet _type)
+    : multi_ary_exprt(ID_bitnor, std::move(_operands), std::move(_type))
+  {
+  }
+};
+
+template <>
+inline bool can_cast_expr<bitnor_exprt>(const exprt &base)
+{
+  return base.id() == ID_bitnor;
+}
+
+/// \brief Cast an exprt to a \ref bitnor_exprt
+///
+/// \a expr must be known to be \ref bitnor_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref bitnor_exprt
+inline const bitnor_exprt &to_bitnor_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_bitnor);
+  return static_cast<const bitnor_exprt &>(expr);
+}
+
+/// \copydoc to_bitnor_expr(const exprt &)
+inline bitnor_exprt &to_bitnor_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_bitnor);
+  return static_cast<bitnor_exprt &>(expr);
+}
+
 /// \brief Bit-wise XOR
 class bitxor_exprt : public multi_ary_exprt
 {
@@ -201,13 +245,22 @@ inline bitxor_exprt &to_bitxor_expr(exprt &expr)
 }
 
 /// \brief Bit-wise XNOR
+///
+/// When given one operand, this is equivalent to the bit-wise negation.
+/// When given three or more operands, this is equivalent to the bit-wise
+/// negation of the bitxor expression with the same operands.
 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))
   {
   }
+
+  bitxnor_exprt(exprt::operandst _operands, typet _type)
+    : multi_ary_exprt(ID_bitxnor, std::move(_operands), std::move(_type))
+  {
+  }
 };
 
 template <>
@@ -275,6 +328,50 @@ inline bitand_exprt &to_bitand_expr(exprt &expr)
   return static_cast<bitand_exprt &>(expr);
 }
 
+/// \brief Bit-wise NAND
+///
+/// When given one operand, this is equivalent to the bit-wise negation.
+/// When given three or more operands, this is equivalent to the bit-wise
+/// negation of the bitand expression with the same operands.
+class bitnand_exprt : public multi_ary_exprt
+{
+public:
+  bitnand_exprt(exprt _op0, exprt _op1)
+    : multi_ary_exprt(std::move(_op0), ID_bitnand, std::move(_op1))
+  {
+  }
+
+  bitnand_exprt(exprt::operandst _operands, typet _type)
+    : multi_ary_exprt(ID_bitnand, std::move(_operands), std::move(_type))
+  {
+  }
+};
+
+template <>
+inline bool can_cast_expr<bitnand_exprt>(const exprt &base)
+{
+  return base.id() == ID_bitnand;
+}
+
+/// \brief Cast an exprt to a \ref bitnand_exprt
+///
+/// \a expr must be known to be \ref bitnand_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref bitnand_exprt
+inline const bitnand_exprt &to_bitnand_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_bitnand);
+  return static_cast<const bitnand_exprt &>(expr);
+}
+
+/// \copydoc to_bitnand_expr(const exprt &)
+inline bitnand_exprt &to_bitnand_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_bitnand);
+  return static_cast<bitnand_exprt &>(expr);
+}
+
 /// \brief A base class for shift and rotate operators
 class shift_exprt : public binary_exprt
 {

src/util/irep_ids.def

@@ -48,6 +48,7 @@ IREP_ID_ONE(nand)
 IREP_ID_ONE(or)
 IREP_ID_ONE(nor)
 IREP_ID_ONE(xor)
+IREP_ID_ONE(xnor)
 IREP_ID_ONE(not)
 IREP_ID_ONE(bitand)
 IREP_ID_ONE(bitor)

src/util/std_expr.h

@@ -2182,6 +2182,43 @@ inline and_exprt &to_and_expr(exprt &expr)
   return static_cast<and_exprt &>(expr);
 }
 
+/// \brief Boolean NAND
+///
+/// When given one operand, this is equivalent to the negation.
+/// When given three or more operands, this is equivalent to the negation
+/// of the and expression with the same operands.
+class nand_exprt : public multi_ary_exprt
+{
+public:
+  nand_exprt(exprt op0, exprt op1)
+    : multi_ary_exprt(std::move(op0), ID_nand, std::move(op1), bool_typet())
+  {
+  }
+
+  explicit nand_exprt(exprt::operandst _operands)
+    : multi_ary_exprt(ID_nand, std::move(_operands), bool_typet())
+  {
+  }
+};
+
+/// \brief Cast an exprt to a \ref nand_exprt
+///
+/// \a expr must be known to be \ref nand_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref nand_exprt
+inline const nand_exprt &to_nand_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_nand);
+  return static_cast<const nand_exprt &>(expr);
+}
+
+/// \copydoc to_nand_expr(const exprt &)
+inline nand_exprt &to_nand_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_nand);
+  return static_cast<nand_exprt &>(expr);
+}
 
 /// \brief Boolean implication
 class implies_exprt:public binary_exprt
@@ -2290,6 +2327,43 @@ inline or_exprt &to_or_expr(exprt &expr)
   return static_cast<or_exprt &>(expr);
 }
 
+/// \brief Boolean NOR
+///
+/// When given one operand, this is equivalent to the negation.
+/// When given three or more operands, this is equivalent to the negation
+/// of the and expression with the same operands.
+class nor_exprt : public multi_ary_exprt
+{
+public:
+  nor_exprt(exprt op0, exprt op1)
+    : multi_ary_exprt(std::move(op0), ID_nor, std::move(op1), bool_typet())
+  {
+  }
+
+  explicit nor_exprt(exprt::operandst _operands)
+    : multi_ary_exprt(ID_nor, std::move(_operands), bool_typet())
+  {
+  }
+};
+
+/// \brief Cast an exprt to a \ref nor_exprt
+///
+/// \a expr must be known to be \ref nor_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref nor_exprt
+inline const nor_exprt &to_nor_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_nor);
+  return static_cast<const nor_exprt &>(expr);
+}
+
+/// \copydoc to_nor_expr(const exprt &)
+inline nor_exprt &to_nor_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_nor);
+  return static_cast<nor_exprt &>(expr);
+}
 
 /// \brief Boolean XOR
 class xor_exprt:public multi_ary_exprt
@@ -2331,6 +2405,49 @@ inline xor_exprt &to_xor_expr(exprt &expr)
   return static_cast<xor_exprt &>(expr);
 }
 
+/// \brief Boolean XNOR
+///
+/// When given one operand, this is equivalent to the negation.
+/// When given three or more operands, this is equivalent to the negation
+/// of the xor expression with the same operands.
+class xnor_exprt : public multi_ary_exprt
+{
+public:
+  xnor_exprt(exprt _op0, exprt _op1)
+    : multi_ary_exprt(std::move(_op0), ID_xnor, std::move(_op1), bool_typet())
+  {
+  }
+
+  explicit xnor_exprt(exprt::operandst _operands)
+    : multi_ary_exprt(ID_xnor, std::move(_operands), bool_typet())
+  {
+  }
+};
+
+template <>
+inline bool can_cast_expr<xnor_exprt>(const exprt &base)
+{
+  return base.id() == ID_xnor;
+}
+
+/// \brief Cast an exprt to a \ref xnor_exprt
+///
+/// \a expr must be known to be \ref xnor_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref xnor_exprt
+inline const xnor_exprt &to_xnor_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_xnor);
+  return static_cast<const xnor_exprt &>(expr);
+}
+
+/// \copydoc to_xnor_expr(const exprt &)
+inline xnor_exprt &to_xnor_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_xnor);
+  return static_cast<xnor_exprt &>(expr);
+}
 
 /// \brief Boolean negation
 class not_exprt:public unary_exprt