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.

Author: kroening

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);