Merge pull request #8536 from diffblue/fix-boolbv-onehot

Fix `onehot0` flattening

src/solvers/flattening/boolbv_onehot.cpp

@@ -15,6 +15,10 @@ literalt boolbvt::convert_onehot(const unary_exprt &expr)
 
   bvt op=convert_bv(expr.op());
 
+  // onehot0 is the same as onehot with the input bits flipped
+  if(expr.id() == ID_onehot0)
+    op = bv_utils.inverted(op);
+
   literalt one_seen=const_literal(false);
   literalt more_than_one_seen=const_literal(false);
 
@@ -25,14 +29,5 @@ literalt boolbvt::convert_onehot(const unary_exprt &expr)
     one_seen=prop.lor(*it, one_seen);
   }
 
-  if(expr.id()==ID_onehot)
-    return prop.land(one_seen, !more_than_one_seen);
-  else
-  {
-    INVARIANT(
-      expr.id() == ID_onehot0,
-      "should be a onehot0 expression as other onehot expression kind has been "
-      "handled in other branch");
-    return !more_than_one_seen;
-  }
+  return prop.land(one_seen, !more_than_one_seen);
 }

unit/Makefile

@@ -96,6 +96,7 @@ SRC += analyses/ai/ai.cpp \
        pointer-analysis/value_set.cpp \
        solvers/bdd/miniBDD/miniBDD.cpp \
        solvers/flattening/boolbv.cpp \
+       solvers/flattening/boolbv_onehot.cpp \
        solvers/flattening/boolbv_update_bit.cpp \
        solvers/floatbv/float_utils.cpp \
        solvers/prop/bdd_expr.cpp \

unit/solvers/flattening/boolbv_onehot.cpp

@@ -0,0 +1,92 @@
+/*******************************************************************\
+
+Module: Unit tests for solvers/flattening/boolbv_onehot
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+/// \file
+
+#include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
+#include <util/bitvector_types.h>
+#include <util/cout_message.h>
+#include <util/namespace.h>
+#include <util/std_expr.h>
+#include <util/symbol_table.h>
+
+#include <solvers/flattening/boolbv.h>
+#include <solvers/sat/satcheck.h>
+#include <testing-utils/use_catch.h>
+
+TEST_CASE("onehot flattening", "[core][solvers][flattening][boolbvt][onehot]")
+{
+  console_message_handlert message_handler;
+  message_handler.set_verbosity(0);
+  satcheckt satcheck{message_handler};
+  symbol_tablet symbol_table;
+  namespacet ns{symbol_table};
+  boolbvt boolbv{ns, satcheck, message_handler};
+  unsignedbv_typet u8{8};
+
+  GIVEN("A bit-vector that is one-hot")
+  {
+    boolbv << onehot_exprt{from_integer(64, u8)};
+
+    THEN("the lowering of onehot is true")
+    {
+      REQUIRE(boolbv() == decision_proceduret::resultt::D_SATISFIABLE);
+    }
+  }
+
+  GIVEN("A bit-vector that is not one-hot")
+  {
+    boolbv << onehot_exprt{from_integer(5, u8)};
+
+    THEN("the lowering of onehot is false")
+    {
+      REQUIRE(boolbv() == decision_proceduret::resultt::D_UNSATISFIABLE);
+    }
+  }
+
+  GIVEN("A bit-vector that is not one-hot")
+  {
+    boolbv << onehot_exprt{from_integer(0, u8)};
+
+    THEN("the lowering of onehot is false")
+    {
+      REQUIRE(boolbv() == decision_proceduret::resultt::D_UNSATISFIABLE);
+    }
+  }
+
+  GIVEN("A bit-vector that is one-hot 0")
+  {
+    boolbv << onehot0_exprt{from_integer(0xfe, u8)};
+
+    THEN("the lowering of onehot0 is true")
+    {
+      REQUIRE(boolbv() == decision_proceduret::resultt::D_SATISFIABLE);
+    }
+  }
+
+  GIVEN("A bit-vector that is not one-hot 0")
+  {
+    boolbv << onehot0_exprt{from_integer(0x7e, u8)};
+
+    THEN("the lowering of onehot0 is false")
+    {
+      REQUIRE(boolbv() == decision_proceduret::resultt::D_UNSATISFIABLE);
+    }
+  }
+
+  GIVEN("A bit-vector that is not one-hot 0")
+  {
+    boolbv << onehot0_exprt{from_integer(0xff, u8)};
+
+    THEN("the lowering of onehot0 is false")
+    {
+      REQUIRE(boolbv() == decision_proceduret::resultt::D_UNSATISFIABLE);
+    }
+  }
+}