From 923769ff32b9ef9a029e7d2bbe7c2b27bfac9b30 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Mon, 16 Dec 2024 13:06:13 -0800
Subject: [PATCH] add mulit-ary constructor for xor_exprt, bitxor_exprt,
 bitand_exprt, bitor_exprt

This adds a constructor that takes an exprt::operandst argument, for
constructing xor_exprt, bitxor_exprt, bitand_exprt, bitor_exprt with more
than two operands.
---
 src/util/bitvector_expr.h | 15 +++++++++++++++
 src/util/std_expr.h       |  5 +++++
 2 files changed, 20 insertions(+)

diff --git a/src/util/bitvector_expr.h b/src/util/bitvector_expr.h
index cd2b2a11c15..e9e3a32fde8 100644
--- a/src/util/bitvector_expr.h
+++ b/src/util/bitvector_expr.h
@@ -128,6 +128,11 @@ class bitor_exprt : public multi_ary_exprt
     : multi_ary_exprt(_op0, ID_bitor, std::move(_op1), _op0.type())
   {
   }
+
+  bitor_exprt(exprt::operandst _operands, typet _type)
+    : multi_ary_exprt(ID_bitor, std::move(_operands), std::move(_type))
+  {
+  }
 };
 
 template <>
@@ -163,6 +168,11 @@ class bitxor_exprt : public multi_ary_exprt
     : multi_ary_exprt(std::move(_op0), ID_bitxor, std::move(_op1))
   {
   }
+
+  bitxor_exprt(exprt::operandst _operands, typet _type)
+    : multi_ary_exprt(ID_bitxor, std::move(_operands), std::move(_type))
+  {
+  }
 };
 
 template <>
@@ -233,6 +243,11 @@ class bitand_exprt : public multi_ary_exprt
     : multi_ary_exprt(_op0, ID_bitand, std::move(_op1), _op0.type())
   {
   }
+
+  bitand_exprt(exprt::operandst _operands, typet _type)
+    : multi_ary_exprt(ID_bitand, std::move(_operands), std::move(_type))
+  {
+  }
 };
 
 template <>
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
index 4fb4661ba78..8a4b0276f10 100644
--- a/src/util/std_expr.h
+++ b/src/util/std_expr.h
@@ -2299,6 +2299,11 @@ class xor_exprt:public multi_ary_exprt
     : multi_ary_exprt(std::move(_op0), ID_xor, std::move(_op1), bool_typet())
   {
   }
+
+  explicit xor_exprt(exprt::operandst _operands)
+    : multi_ary_exprt(ID_xor, std::move(_operands), bool_typet())
+  {
+  }
 };
 
 template <>