From 24073656e829914f664fa60ca63b822bc8436dd6 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Wed, 3 Dec 2025 09:27:25 -0800
Subject: [PATCH] document non-binary case for Boolean and bit-wise operators

This documents the current behavior of the non-binary case of the Boolean
operators and the bit-wise operators.
---
 src/util/bitvector_expr.h | 12 ++++++++++++
 src/util/std_expr.h       | 12 ++++++++++--
 2 files changed, 22 insertions(+), 2 deletions(-)

diff --git a/src/util/bitvector_expr.h b/src/util/bitvector_expr.h
index e6c3d6eedbf..ad935f6b3dd 100644
--- a/src/util/bitvector_expr.h
+++ b/src/util/bitvector_expr.h
@@ -121,6 +121,8 @@ inline bitnot_exprt &to_bitnot_expr(exprt &expr)
 }
 
 /// \brief Bit-wise OR
+/// Any number of operands that is greater or equal one.
+/// The type of all operands must be the same.
 class bitor_exprt : public multi_ary_exprt
 {
 public:
@@ -162,6 +164,8 @@ inline bitor_exprt &to_bitor_expr(exprt &expr)
 
 /// \brief Bit-wise NOR
 ///
+/// Any number of operands that is greater or equal one.
+/// The type of all operands must be the same.
 /// 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.
@@ -205,6 +209,8 @@ inline bitnor_exprt &to_bitnor_expr(exprt &expr)
 }
 
 /// \brief Bit-wise XOR
+/// Any number of operands that is greater or equal one.
+/// The type of all operands must be the same.
 class bitxor_exprt : public multi_ary_exprt
 {
 public:
@@ -246,6 +252,8 @@ inline bitxor_exprt &to_bitxor_expr(exprt &expr)
 
 /// \brief Bit-wise XNOR
 ///
+/// Any number of operands that is greater or equal one.
+/// The type of all operands must be the same.
 /// 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.
@@ -291,6 +299,8 @@ inline bitxnor_exprt &to_bitxnor_expr(exprt &expr)
 }
 
 /// \brief Bit-wise AND
+/// Any number of operands that is greater or equal one.
+/// The type of all operands must be the same.
 class bitand_exprt : public multi_ary_exprt
 {
 public:
@@ -332,6 +342,8 @@ inline bitand_exprt &to_bitand_expr(exprt &expr)
 
 /// \brief Bit-wise NAND
 ///
+/// Any number of operands that is greater or equal one.
+/// The type of all operands must be the same.
 /// 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.
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
index c076d6fcc2c..2b778f67107 100644
--- a/src/util/std_expr.h
+++ b/src/util/std_expr.h
@@ -2119,8 +2119,9 @@ inline typecast_exprt &to_typecast_expr(exprt &expr)
   return static_cast<typecast_exprt &>(expr);
 }
 
-
 /// \brief Boolean AND
+/// All operands must be boolean, and the result is always boolean.
+/// Any number of operands that is greater or equal one.
 class and_exprt:public multi_ary_exprt
 {
 public:
@@ -2189,6 +2190,8 @@ inline and_exprt &to_and_expr(exprt &expr)
 
 /// \brief Boolean NAND
 ///
+/// All operands must be boolean, and the result is always boolean.
+/// Any number of operands that is greater or equal one.
 /// 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.
@@ -2269,8 +2272,9 @@ inline implies_exprt &to_implies_expr(exprt &expr)
   return ret;
 }
 
-
 /// \brief Boolean OR
+/// All operands must be boolean, and the result is always boolean.
+/// Any number of operands that is greater or equal one.
 class or_exprt:public multi_ary_exprt
 {
 public:
@@ -2334,6 +2338,8 @@ inline or_exprt &to_or_expr(exprt &expr)
 
 /// \brief Boolean NOR
 ///
+/// All operands must be boolean, and the result is always boolean.
+/// Any number of operands that is greater or equal one.
 /// 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.
@@ -2371,6 +2377,8 @@ inline nor_exprt &to_nor_expr(exprt &expr)
 }
 
 /// \brief Boolean XOR
+/// All operands must be boolean, and the result is always boolean.
+/// Any number of operands that is greater or equal one.
 class xor_exprt:public multi_ary_exprt
 {
 public: