Merge pull request #8508 from diffblue/smt-bv

SMT2: bvnor, bvnand are binary only; add bvxnor

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

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,13 +278,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, validation_modet::INVARIANT);
   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, validation_modet::INVARIANT);
   return static_cast<bitxnor_exprt &>(expr);
 }