Lower enum_tags to its enum underlying type.

In order to support expressions with type `c_enum_tag_typet` in the
incremental SMT2 solver, a new `lower_enum` has been added.
Such function lowers the type of each expression node in the AST with
type `c_enum_tag_type` to the underlying type of the `c_enum_typet` that
the tag points to.

Author: Enrico Steffinlongo

src/solvers/Makefile

@@ -211,6 +211,7 @@ SRC = $(BOOLEFORCE_SRC) \
       smt2_incremental/smt_to_smt2_string.cpp \
       smt2_incremental/smt2_incremental_decision_procedure.cpp \
       smt2_incremental/encoding/struct_encoding.cpp \
+      smt2_incremental/encoding/enum_encoding.cpp \
       smt2_incremental/theories/smt_array_theory.cpp \
       smt2_incremental/theories/smt_bit_vector_theory.cpp \
       smt2_incremental/theories/smt_core_theory.cpp \

src/solvers/smt2_incremental/encoding/enum_encoding.cpp

@@ -0,0 +1,53 @@
+// Author: Diffblue Ltd.
+
+#include "enum_encoding.h"
+
+#include <util/c_types.h>
+#include <util/expr_cast.h>
+#include <util/namespace.h>
+
+#include <queue>
+
+// Internal function to lower inner types of compound types (at the moment only
+// arrays)
+static typet encode(typet type, const namespacet &ns)
+{
+  std::queue<typet *> work_queue;
+  work_queue.push(&type);
+  while(!work_queue.empty())
+  {
+    typet &current = *work_queue.front();
+    work_queue.pop();
+    if(const auto c_enum_tag = type_try_dynamic_cast<c_enum_tag_typet>(current))
+    {
+      // Replace the type of the c_enum_tag with the underlying type of the enum
+      // it points to
+      current = ns.follow_tag(*c_enum_tag).underlying_type();
+    }
+    if(const auto array = type_try_dynamic_cast<array_typet>(current))
+    {
+      // Add the type of the array's elements to the queue to be explored
+      work_queue.push(&array->element_type());
+    }
+  }
+  return type;
+}
+
+// Worklist algorithm to lower enum types of expr and its sub-expressions.
+exprt lower_enum(exprt expr, const namespacet &ns)
+{
+  std::queue<exprt *> work_queue;
+  work_queue.push(&expr);
+  while(!work_queue.empty())
+  {
+    exprt &current = *work_queue.front();
+    work_queue.pop();
+
+    // Replace the type of the expression node with the encoded one
+    current.type() = encode(current.type(), ns);
+
+    for(auto &operand : current.operands())
+      work_queue.push(&operand);
+  }
+  return expr;
+}

src/solvers/smt2_incremental/encoding/enum_encoding.h

@@ -0,0 +1,16 @@
+// Author: Diffblue Ltd.
+
+#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_ENCODING_ENUM_ENCODING_H
+#define CPROVER_SOLVERS_SMT2_INCREMENTAL_ENCODING_ENUM_ENCODING_H
+
+#include <util/expr.h>
+
+/// Function to lower `expr` and its sub-expressions containing enum types.
+/// Specifically it replaces the node `c_enum_tag_typet` type with the
+/// underlying type of the enum the tag points to.
+/// @param expr the expression to lower.
+/// @param ns the namespace where to lookup `c_enum_tag_type`s.
+/// @return the lowered expression.
+exprt lower_enum(exprt expr, const namespacet &ns);
+
+#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_ENCODING_ENUM_ENCODING_H

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -16,6 +16,7 @@
 #include <solvers/smt2_incremental/ast/smt_terms.h>
 #include <solvers/smt2_incremental/construct_value_expr_from_smt.h>
 #include <solvers/smt2_incremental/convert_expr_to_smt.h>
+#include <solvers/smt2_incremental/encoding/enum_encoding.h>
 #include <solvers/smt2_incremental/smt_solver_process.h>
 #include <solvers/smt2_incremental/theories/smt_array_theory.h>
 #include <solvers/smt2_incremental/theories/smt_core_theory.h>
@@ -590,8 +591,8 @@ void smt2_incremental_decision_proceduret::define_object_properties()
 
 exprt smt2_incremental_decision_proceduret::lower(exprt expression)
 {
-  const exprt lowered =
-    struct_encoding.encode(lower_byte_operators(expression, ns));
+  const exprt lowered = struct_encoding.encode(
+    lower_enum(lower_byte_operators(expression, ns), ns));
   log.conditional_output(log.debug(), [&](messaget::mstreamt &debug) {
     if(lowered != expression)
       debug << "lowered to -\n  " << lowered.pretty(2, 0) << messaget::eom;