Fix semantics of onehot0: at most one bit set

src/solvers/flattening/boolbv_onehot.cpp

@@ -15,10 +15,6 @@ 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);
 
@@ -29,5 +25,14 @@ literalt boolbvt::convert_onehot(const unary_exprt &expr)
     one_seen=prop.lor(*it, one_seen);
   }
 
-  return prop.land(one_seen, !more_than_one_seen);
+  if(expr.id() == ID_onehot)
+  {
+    // exactly one bit is set
+    return prop.land(one_seen, !more_than_one_seen);
+  }
+  else
+  {
+    // onehot0: at most one bit is set
+    return !more_than_one_seen;
+  }
 }

src/util/bitvector_expr.cpp

@@ -307,7 +307,9 @@ exprt zero_extend_exprt::lower() const
   }
 }
 
-static exprt onehot_lowering(const exprt &expr)
+/// Returns a pair of expressions: the first is true iff at least one bit
+/// of \p expr is set, the second is true iff more than one bit is set.
+static std::pair<exprt, exprt> onehot_lowering_helper(const exprt &expr)
 {
   exprt one_seen = false_exprt{};
   const auto width = to_bitvector_type(expr.type()).get_width();
@@ -321,22 +323,24 @@ static exprt onehot_lowering(const exprt &expr)
     one_seen = or_exprt{one_seen, bit};
   }
 
-  auto more_than_one_seen = disjunction(more_than_one_seen_disjuncts);
-
-  return and_exprt{one_seen, not_exprt{more_than_one_seen}};
+  return {one_seen, disjunction(more_than_one_seen_disjuncts)};
 }
 
 exprt onehot_exprt::lower() const
 {
   auto symbol = symbol_exprt{"onehot-op", op().type()};
+  auto [one_seen, more_than_one_seen] = onehot_lowering_helper(symbol);
 
-  return let_exprt{symbol, op(), onehot_lowering(symbol)};
+  // exactly one bit is set
+  return let_exprt{
+    symbol, op(), and_exprt{one_seen, not_exprt{more_than_one_seen}}};
 }
 
 exprt onehot0_exprt::lower() const
 {
   auto symbol = symbol_exprt{"onehot-op", op().type()};
+  auto [one_seen, more_than_one_seen] = onehot_lowering_helper(symbol);
 
-  // same as onehot, but on flipped operand bits
-  return let_exprt{symbol, bitnot_exprt{op()}, onehot_lowering(symbol)};
+  // at most one bit is set
+  return let_exprt{symbol, op(), not_exprt{more_than_one_seen}};
 }

src/util/bitvector_expr.h

@@ -1936,7 +1936,9 @@ inline onehot_exprt &to_onehot_expr(exprt &expr)
 }
 
 /// \brief A Boolean expression returning true iff the given
-/// operand consists of exactly one '0' and '1' otherwise.
+/// operand contains at most one '1', i.e., the operand is either
+/// one-hot or zero. This matches the semantics of SystemVerilog's
+/// $onehot0.
 class onehot0_exprt : public unary_predicate_exprt
 {
 public:

unit/solvers/flattening/boolbv_onehot.cpp

@@ -58,29 +58,39 @@ TEST_CASE("onehot flattening", "[core][solvers][flattening][boolbvt][onehot]")
     }
   }
 
-  GIVEN("A bit-vector that is one-hot 0")
+  GIVEN("A bit-vector that is one-hot")
   {
-    boolbv << onehot0_exprt{from_integer(0xfe, u8)};
+    boolbv << onehot0_exprt{from_integer(64, 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")
+  GIVEN("A bit-vector that is zero")
   {
-    boolbv << onehot0_exprt{from_integer(0x7e, u8)};
+    boolbv << onehot0_exprt{from_integer(0, u8)};
+
+    THEN("the lowering of onehot0 is true")
+    {
+      REQUIRE(boolbv() == decision_proceduret::resultt::D_SATISFIABLE);
+    }
+  }
+
+  GIVEN("A bit-vector with two bits set")
+  {
+    boolbv << onehot0_exprt{from_integer(5, 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")
+  GIVEN("A bit-vector with all bits but one set")
   {
-    boolbv << onehot0_exprt{from_integer(0xff, u8)};
+    boolbv << onehot0_exprt{from_integer(0xfe, u8)};
 
     THEN("the lowering of onehot0 is false")
     {

unit/util/bitvector_expr.cpp

@@ -110,29 +110,39 @@ TEST_CASE("onehot expression lowering", "[core][util][expr]")
     }
   }
 
-  GIVEN("A bit-vector that is one-hot 0")
+  GIVEN("A bit-vector that is one-hot")
   {
-    boolbv << onehot0_exprt{from_integer(0xfe, u8)}.lower();
+    boolbv << onehot0_exprt{from_integer(64, u8)}.lower();
 
     THEN("the lowering of onehot0 is true")
     {
       REQUIRE(boolbv() == decision_proceduret::resultt::D_SATISFIABLE);
     }
   }
 
-  GIVEN("A bit-vector that is not one-hot 0")
+  GIVEN("A bit-vector that is zero")
   {
-    boolbv << onehot0_exprt{from_integer(0x7e, u8)}.lower();
+    boolbv << onehot0_exprt{from_integer(0, u8)}.lower();
+
+    THEN("the lowering of onehot0 is true")
+    {
+      REQUIRE(boolbv() == decision_proceduret::resultt::D_SATISFIABLE);
+    }
+  }
+
+  GIVEN("A bit-vector with two bits set")
+  {
+    boolbv << onehot0_exprt{from_integer(5, u8)}.lower();
 
     THEN("the lowering of onehot0 is false")
     {
       REQUIRE(boolbv() == decision_proceduret::resultt::D_UNSATISFIABLE);
     }
   }
 
-  GIVEN("A bit-vector that is not one-hot 0")
+  GIVEN("A bit-vector with all bits but one set")
   {
-    boolbv << onehot0_exprt{from_integer(0xff, u8)}.lower();
+    boolbv << onehot0_exprt{from_integer(0xfe, u8)}.lower();
 
     THEN("the lowering of onehot0 is false")
     {