From 99376ab6cd7331b4bdd3380008b6849e2b713d4b Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Mon, 18 Nov 2024 13:35:50 +0000
Subject: [PATCH] SMT2: bvnor, bvnand are binary only; add bvxnor

The SMT-LIB2 expressions bvnor and bvnand are not multi-ary.

Furthermore, this adds the (binary) bvxnor expression.
---
 src/solvers/smt2/smt2_conv.cpp | 63 ++++++++++++++++++++++++++++++----
 src/util/bitvector_expr.h      |  4 ++-
 2 files changed, 60 insertions(+), 7 deletions(-)

diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index c1e26e2d0ec..7e80be518d2 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -1220,12 +1220,9 @@ void smt2_convt::convert_expr(const exprt &expr)
 
     convert_expr(expr.operands().front());
   }
-  else if(expr.id()==ID_concatenation ||
-          expr.id()==ID_bitand ||
-          expr.id()==ID_bitor ||
-          expr.id()==ID_bitxor ||
-          expr.id()==ID_bitnand ||
-          expr.id()==ID_bitnor)
+  else if(
+    expr.id() == ID_concatenation || expr.id() == ID_bitand ||
+    expr.id() == ID_bitor || expr.id() == ID_bitxor)
   {
     DATA_INVARIANT_WITH_DIAGNOSTICS(
       expr.operands().size() >= 2,
@@ -1255,6 +1252,60 @@ void smt2_convt::convert_expr(const exprt &expr)
 
     out << ")";
   }
+  else if(
+    expr.id() == ID_bitxnor || expr.id() == ID_bitnand ||
+    expr.id() == ID_bitnor)
+  {
+    // SMT-LIB only has these as a binary expression,
+    // owing to their ambiguity.
+    if(expr.operands().size() == 2)
+    {
+      const auto &binary_expr = to_binary_expr(expr);
+
+      out << '(';
+      if(binary_expr.id() == ID_bitxnor)
+        out << "bvxnor";
+      else if(binary_expr.id() == ID_bitnand)
+        out << "bvnand";
+      else if(binary_expr.id() == ID_bitnor)
+        out << "bvnor";
+      out << ' ';
+      flatten2bv(binary_expr.op0());
+      out << ' ';
+      flatten2bv(binary_expr.op1());
+      out << ')';
+    }
+    else if(expr.operands().size() == 1)
+    {
+      out << "(bvnot ";
+      flatten2bv(to_unary_expr(expr).op());
+      out << ')';
+    }
+    else if(expr.operands().size() >= 3)
+    {
+      out << "(bvnot (";
+      if(expr.id() == ID_bitxnor)
+        out << "bvxor";
+      else if(expr.id() == ID_bitnand)
+        out << "bvand";
+      else if(expr.id() == ID_bitnor)
+        out << "bvor";
+
+      for(const auto &op : expr.operands())
+      {
+        out << ' ';
+        flatten2bv(op);
+      }
+
+      out << "))"; // bvX, bvnot
+    }
+    else
+    {
+      DATA_INVARIANT(
+        expr.operands().size() >= 1,
+        expr.id_string() + " should have at least one operand");
+    }
+  }
   else if(expr.id()==ID_bitnot)
   {
     const bitnot_exprt &bitnot_expr = to_bitnot_expr(expr);
diff --git a/src/util/bitvector_expr.h b/src/util/bitvector_expr.h
index ec93a8006b4..e6c3d6eedbf 100644
--- a/src/util/bitvector_expr.h
+++ b/src/util/bitvector_expr.h
@@ -253,7 +253,7 @@ 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))
+    : multi_ary_exprt(_op0, ID_bitxnor, _op1, _op0.type())
   {
   }
 
@@ -278,6 +278,7 @@ inline bool can_cast_expr<bitxnor_exprt>(const exprt &base)
 inline const bitxnor_exprt &to_bitxnor_expr(const exprt &expr)
 {
   PRECONDITION(expr.id() == ID_bitxnor);
+  bitxnor_exprt::check(expr, validation_modet::INVARIANT);
   return static_cast<const bitxnor_exprt &>(expr);
 }
 
@@ -285,6 +286,7 @@ inline const bitxnor_exprt &to_bitxnor_expr(const exprt &expr)
 inline bitxnor_exprt &to_bitxnor_expr(exprt &expr)
 {
   PRECONDITION(expr.id() == ID_bitxnor);
+  bitxnor_exprt::check(expr, validation_modet::INVARIANT);
   return static_cast<bitxnor_exprt &>(expr);
 }