Fix onehot0 flattening

This fixes the flattening of onehot0 expressions.

Author: kroening

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 \