SMT2: implement nand, nor

This adds the multi-ary Boolean operators nand and nor to the SMT2 backend.

Author: kroening

src/solvers/smt2/smt2_conv.cpp

@@ -1362,6 +1362,34 @@ void smt2_convt::convert_expr(const exprt &expr)
     }
     out << ")";
   }
+  else if(expr.id() == ID_nand || expr.id() == ID_nor)
+  {
+    DATA_INVARIANT(
+      expr.is_boolean(),
+      "logical nand, nor expressions should have Boolean type");
+    DATA_INVARIANT(
+      expr.operands().size() >= 1,
+      "logical nand, nor expressions should have at least one operand");
+
+    // SMT-LIB doesn't have nand, nor
+    out << "(not ";
+    if(expr.operands().size() == 1)
+      convert_expr(to_multi_ary_expr(expr).op0());
+    else
+    {
+      if(expr.id() == ID_nand)
+        out << "(and";
+      else
+        out << "(or";
+      for(const auto &op : expr.operands())
+      {
+        out << " ";
+        convert_expr(op);
+      }
+      out << ')'; // or, and
+    }
+    out << ')'; // not
+  }
   else if(expr.id()==ID_implies)
   {
     const implies_exprt &implies_expr = to_implies_expr(expr);