Merge pull request #8964 from diffblue/smt2-reduction-operators

SMT2 backend: reduction operators

Author: tautschnig

src/solvers/smt2/smt2_conv.cpp

@@ -2724,6 +2724,67 @@ void smt2_convt::convert_expr(const exprt &expr)
     // use the lowering
     convert_expr(to_cond_expr(expr).lower());
   }
+  else if(expr.id() == ID_reduction_and)
+  {
+    // This is true iff all bits in the operand are true
+    auto &op = to_unary_expr(expr).op();
+    auto all_ones = to_bitvector_type(op.type()).all_ones_expr();
+    convert_expr(equal_exprt{op, all_ones});
+  }
+  else if(expr.id() == ID_reduction_nand)
+  {
+    // This is the negation of "reduction and"
+    auto &op = to_unary_expr(expr).op();
+    convert_expr(not_exprt{unary_predicate_exprt{ID_reduction_and, op}});
+  }
+  else if(expr.id() == ID_reduction_or)
+  {
+    // This is true iff the operand is not zero
+    auto &op = to_unary_expr(expr).op();
+    auto all_zeros = to_bitvector_type(op.type()).all_zeros_expr();
+    convert_expr(notequal_exprt{op, all_zeros});
+  }
+  else if(expr.id() == ID_reduction_nor)
+  {
+    // This is the negation of "reduction or"
+    auto &op = to_unary_expr(expr).op();
+    convert_expr(not_exprt{unary_predicate_exprt{ID_reduction_or, op}});
+  }
+  else if(expr.id() == ID_reduction_xor)
+  {
+    // This is the parity of the operand. No SMT-LIB 2 equivalent.
+    // Do bit-wise. SMT-LIB 3.0 could do this with "fold bvxor".
+    auto &op = to_unary_expr(expr).op();
+    auto width = to_bitvector_type(op.type()).get_width();
+    PRECONDITION(width >= 1);
+
+    if(width == 1)
+    {
+      out << "(= ";
+      flatten2bv(op);
+      out << " #b1)";
+    }
+    else
+    {
+      out << "(let ((?rop ";
+      flatten2bv(op);
+      out << ")) ";
+
+      // XOR all bits: extract each bit and use multi-ary bvxor
+      out << "(= (bvxor";
+      for(std::size_t i = 0; i < width; i++)
+        out << " ((_ extract " << i << " " << i << ") ?rop)";
+      out << ") #b1)";
+
+      out << ')'; // let
+    }
+  }
+  else if(expr.id() == ID_reduction_xnor)
+  {
+    // This is the negation of "reduction xor"
+    auto &op = to_unary_expr(expr).op();
+    convert_expr(not_exprt{unary_predicate_exprt{ID_reduction_xor, op}});
+  }
   else
     INVARIANT_WITH_DIAGNOSTICS(
       false,

unit/solvers/smt2/smt2_conv.cpp

@@ -1,8 +1,15 @@
 // Author: Diffblue Ltd.
 
-#include <testing-utils/use_catch.h>
+/// \file
+/// Unit tests for smt2_convt
+
+#include <util/bitvector_types.h>
+#include <util/namespace.h>
+#include <util/std_expr.h>
+#include <util/symbol_table.h>
 
 #include <solvers/smt2/smt2_conv.h>
+#include <testing-utils/use_catch.h>
 
 TEST_CASE(
   "smt2_convt::convert_identifier character escaping.",
@@ -17,3 +24,93 @@ TEST_CASE(
   CHECK(smt2_convt::convert_identifier("|") == "|&124;|");
   CHECK(smt2_convt::convert_identifier("&") == "&");
 }
+
+/// Helper: extract the "(assert ...)" line from SMT2 output of set_to
+static std::string get_assert(const exprt &red_expr)
+{
+  symbol_tablet symbol_table;
+  namespacet ns(symbol_table);
+  std::ostringstream out;
+  smt2_convt conv(ns, "test", "", "QF_BV", smt2_convt::solvert::GENERIC, out);
+  conv.set_to(red_expr, true);
+  std::string result = out.str();
+  auto pos = result.find("(assert ");
+  REQUIRE(pos != std::string::npos);
+  // strip trailing newline
+  auto end = result.find_last_not_of('\n');
+  return result.substr(pos, end - pos + 1);
+}
+
+TEST_CASE("smt2_convt reduction operators", "[core][solvers][smt2]")
+{
+  unsignedbv_typet u2(2);
+  symbol_exprt sym("x", u2);
+
+  SECTION("reduction_and")
+  {
+    REQUIRE(
+      get_assert(unary_predicate_exprt{ID_reduction_and, sym}) ==
+      "(assert (= x (_ bv3 2)))");
+  }
+
+  SECTION("reduction_nand")
+  {
+    REQUIRE(
+      get_assert(unary_predicate_exprt{ID_reduction_nand, sym}) ==
+      "(assert (not (= x (_ bv3 2))))");
+  }
+
+  SECTION("reduction_or")
+  {
+    REQUIRE(
+      get_assert(unary_predicate_exprt{ID_reduction_or, sym}) ==
+      "(assert (not (= x (_ bv0 2))))");
+  }
+
+  SECTION("reduction_nor")
+  {
+    REQUIRE(
+      get_assert(unary_predicate_exprt{ID_reduction_nor, sym}) ==
+      "(assert (not (not (= x (_ bv0 2)))))");
+  }
+
+  SECTION("reduction_xor")
+  {
+    REQUIRE(
+      get_assert(unary_predicate_exprt{ID_reduction_xor, sym}) ==
+      "(assert (let ((?rop x)) "
+      "(= (bvxor ((_ extract 0 0) ?rop) ((_ extract 1 1) ?rop)) #b1)))");
+  }
+
+  SECTION("reduction_xnor")
+  {
+    REQUIRE(
+      get_assert(unary_predicate_exprt{ID_reduction_xnor, sym}) ==
+      "(assert (not (let ((?rop x)) "
+      "(= (bvxor ((_ extract 0 0) ?rop) ((_ extract 1 1) ?rop)) #b1))))");
+  }
+
+  SECTION("reduction_xor 1-bit")
+  {
+    symbol_exprt sym1("y", unsignedbv_typet(1));
+    REQUIRE(
+      get_assert(unary_predicate_exprt{ID_reduction_xor, sym1}) ==
+      "(assert (= y #b1))");
+  }
+
+  SECTION("reduction_and 1-bit")
+  {
+    symbol_exprt sym1("y", unsignedbv_typet(1));
+    REQUIRE(
+      get_assert(unary_predicate_exprt{ID_reduction_and, sym1}) ==
+      "(assert (= y (_ bv1 1)))");
+  }
+
+  SECTION("reduction_or 1-bit")
+  {
+    symbol_exprt sym1("y", unsignedbv_typet(1));
+    REQUIRE(
+      get_assert(unary_predicate_exprt{ID_reduction_or, sym1}) ==
+      "(assert (not (= y (_ bv0 1))))");
+  }
+}