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

@@ -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,28 @@ void smt2_convt::convert_expr(const exprt &expr)
 
     out << ")";
   }
+  else if(
+    expr.id() == ID_bitxnor || expr.id() == ID_bitnand ||
+    expr.id() == ID_bitnor)
+  {
+    // only exist as a binary expression
+    const auto &bitxnor = to_bitxnor_expr(expr);
+    DATA_INVARIANT(
+      expr.operands().size() == 2, "bitxnor should have two operands");
+
+    out << '(';
+    if(expr.id() == ID_bitxnor)
+      out << "bvxnor";
+    else if(expr.id() == ID_bitnand)
+      out << "bvnand";
+    else if(expr.id() == ID_bitnor)
+      out << "bvnor";
+    out << ' ';
+    flatten2bv(bitxnor.op0());
+    out << ' ';
+    flatten2bv(bitxnor.op1());
+    out << ')';
+  }
   else if(expr.id()==ID_bitnot)
   {
     const bitnot_exprt &bitnot_expr = to_bitnot_expr(expr);

src/util/bitvector_expr.h

@@ -191,11 +191,12 @@ inline bitxor_exprt &to_bitxor_expr(exprt &expr)
 }
 
 /// \brief Bit-wise XNOR
-class bitxnor_exprt : public multi_ary_exprt
+/// Binary, not multi-ary, to avoid the ambiguity.
+class bitxnor_exprt : public binary_exprt
 {
 public:
   bitxnor_exprt(exprt _op0, exprt _op1)
-    : multi_ary_exprt(std::move(_op0), ID_bitxnor, std::move(_op1))
+    : binary_exprt(std::move(_op0), ID_bitxnor, std::move(_op1))
   {
   }
 };
@@ -215,13 +216,15 @@ 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);
   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);
+  bitxnor_exprt::check(expr);
   return static_cast<bitxnor_exprt &>(expr);
 }