Merge pull request #8589 from diffblue/enumeration_bv_get

implement boolbvt::get for enumeration types

Author: kroening

src/solvers/flattening/boolbv_get.cpp

@@ -199,7 +199,9 @@ exprt boolbvt::bv_get_rec(const exprt &expr, const bvt &bv, std::size_t offset)
   switch(bvtype)
   {
   case bvtypet::IS_UNKNOWN:
-    PRECONDITION(type.id() == ID_string || type.id() == ID_empty);
+    PRECONDITION(
+      type.id() == ID_string || type.id() == ID_empty ||
+      type.id() == ID_enumeration);
     if(type.id()==ID_string)
     {
       mp_integer int_value=binary2integer(value, false);
@@ -215,6 +217,16 @@ exprt boolbvt::bv_get_rec(const exprt &expr, const bvt &bv, std::size_t offset)
     {
       return constant_exprt{irep_idt(), type};
     }
+    else if(type.id() == ID_enumeration)
+    {
+      auto &elements = to_enumeration_type(type).elements();
+      mp_integer int_value = binary2integer(value, false);
+      if(int_value >= elements.size())
+        return nil_exprt{};
+      else
+        return constant_exprt{
+          elements[numeric_cast_v<std::size_t>(int_value)].id(), type};
+    }
     break;
 
   case bvtypet::IS_RANGE:

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_enumeration.cpp \
        solvers/flattening/boolbv_onehot.cpp \
        solvers/flattening/boolbv_update_bit.cpp \
        solvers/floatbv/float_utils.cpp \

unit/solvers/flattening/boolbv_enumeration.cpp

@@ -0,0 +1,57 @@
+/*******************************************************************\
+
+Module: Unit tests for solvers/flattening
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+/// \file
+
+#include <util/cout_message.h>
+#include <util/namespace.h>
+#include <util/symbol_table.h>
+
+#include <solvers/flattening/boolbv.h>
+#include <solvers/sat/satcheck.h>
+#include <testing-utils/use_catch.h>
+
+TEST_CASE(
+  "enumeration flattening",
+  "[core][solvers][flattening][boolbvt][enumeration]")
+{
+  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};
+  enumeration_typet enumeration;
+  enumeration.elements().push_back(irept{"A"});
+  enumeration.elements().push_back(irept{"B"});
+
+  constant_exprt A("A", enumeration);
+  constant_exprt B("B", enumeration);
+
+  GIVEN("an inconsistent equality over an enumeration type")
+  {
+    boolbv << equal_exprt{A, B};
+
+    THEN("the formula is unsat")
+    {
+      REQUIRE(boolbv() == decision_proceduret::resultt::D_UNSATISFIABLE);
+    }
+  }
+
+  GIVEN("an equality over an enumeration type")
+  {
+    symbol_exprt symbol("s", enumeration);
+    boolbv << equal_exprt{symbol, A};
+
+    THEN("the value of the variable in the model is correct")
+    {
+      REQUIRE(boolbv() == decision_proceduret::resultt::D_SATISFIABLE);
+      REQUIRE(boolbv.get(symbol) == A);
+    }
+  }
+}