Extract map_theoryt base class from arrayst

regression/cbmc/array-constraint/test_json.desc

@@ -1,10 +1,10 @@
-KNOWNBUG
+CORE broken-cprover-smt-backend no-new-smt
 main.c
 --show-array-constraints --json-ui
 activate-multi-line-match
-^EXIT=0$
+^EXIT=10$
 ^SIGNAL=0$
-\{\n\s*"arrayConstraints": \{\n\s*"arrayEquality": \[.*\],\n\s*"arrayWith": \[.*\]\n\s*\},\n\s*"numOfConstraints": 4\n\s*\}
+\{\n\s*"arrayConstraints": \{\n\s*"arrayEquality": \d+,\n\s*"arrayWith": \d+\n\s*\},\n\s*"numOfConstraints": 4\n\s*\}
 --
 --
 To test output for --show-array-constraints option that displays the count and list of all array constraints added during post processing in json format.

src/cprover/bv_pointers_wide.cpp

@@ -155,8 +155,8 @@ bv_pointers_widet::bv_pointers_widet(
   const namespacet &_ns,
   propt &_prop,
   message_handlert &message_handler,
-  bool get_array_constraints)
-  : boolbvt(_ns, _prop, message_handler, get_array_constraints),
+  bool collect_constraint_stats)
+  : boolbvt(_ns, _prop, message_handler, collect_constraint_stats),
     pointer_logic(_ns)
 {
 }

src/cprover/bv_pointers_wide.h

@@ -23,7 +23,7 @@ class bv_pointers_widet : public boolbvt
     const namespacet &,
     propt &,
     message_handlert &,
-    bool get_array_constraints = false);
+    bool collect_constraint_stats = false);
 
   void finish_eager_conversion() override;
 

src/goto-checker/solver_factory.cpp

@@ -356,10 +356,10 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_default()
 {
   auto sat_solver = get_sat_solver(message_handler, options);
 
-  bool get_array_constraints =
+  bool collect_constraint_stats =
     options.get_bool_option("show-array-constraints");
   auto bv_pointers = std::make_unique<bv_pointerst>(
-    ns, *sat_solver, message_handler, get_array_constraints);
+    ns, *sat_solver, message_handler, collect_constraint_stats);
 
   if(options.get_option("arrays-uf") == "never")
     bv_pointers->unbounded_array = bv_pointerst::unbounded_arrayt::U_NONE;

src/solvers/Makefile

@@ -140,6 +140,7 @@ SRC = $(BOOLEFORCE_SRC) \
       flattening/bv_utils.cpp \
       flattening/c_bit_field_replacement_type.cpp \
       flattening/equality.cpp \
+      flattening/map_theory.cpp \
       flattening/pointer_logic.cpp \
       floatbv/float_bv.cpp \
       floatbv/float_utils.cpp \