Add utility and module to track array constraints and display in json format

This commit adds utilities to track array constraints and also the type of
constraint being added, eg: ackermann constraint, array_of etc. Added a new
enum class constraint_typet which is an extension of lazy_typet. This enum class
includes a separate value for constraints added for other indices array_with,
constraints added for the 'true' and 'false branches of if etc in addition to
those available in lazy_typet. Also define a new member of type std::map that
tracks mapping between type of constraint and the constraint itself.
Currently support json output.

clang format arrays.cpp

Author: Natasha Yogananda Jeppu

src/solvers/flattening/arrays.cpp

@@ -10,12 +10,13 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/arith_tools.h>
 #include <util/format_expr.h>
+#include <util/json_irep.h>
+#include <util/message.h>
 #include <util/namespace.h>
 #include <util/replace_expr.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
-#include <util/json_irep.h>
-#include <util/message.h>
+
 #include <util/ui_message.h>
 
 #include <solvers/prop/prop.h>
@@ -31,7 +32,9 @@ arrayst::arrayst(
   propt &_prop,
   message_handlert &_message_handler,
   bool _get_array_constraints)
-  : equalityt(_prop, _message_handler), ns(_ns), log(_message_handler),
+  : equalityt(_prop, _message_handler),
+    ns(_ns),
+    log(_message_handler),
     message_handler(_message_handler)
 {
   lazy_arrays = false;        // will be set to true when --refine is used
@@ -371,8 +374,8 @@ void arrayst::add_array_Ackermann_constraints()
             lazy_constraintt lazy(lazy_typet::ARRAY_ACKERMANN,
               implies_exprt(literal_exprt(indices_equal_lit), values_equal));
             add_array_constraint(lazy, true); // added lazily
-            array_constraints_map[
-              constraint_typet::ARRAY_ACKERMANN].push_back(lazy.lazy);
+            array_constraints_map[constraint_typet::ARRAY_ACKERMANN].push_back(
+              lazy.lazy);
 
 #if 0 // old code for adding, not significantly faster
             prop.lcnf(!indices_equal_lit, convert(values_equal));
@@ -459,8 +462,8 @@ void arrayst::add_array_constraints_equality(
     // equality constraints are not added lazily
     // convert must be done to guarantee correct update of the index_set
     prop.lcnf(!array_equality.l, convert(equality_expr));
-    array_constraints_map[
-      constraint_typet::ARRAY_EQUALITY].push_back(equality_expr);
+    array_constraints_map[constraint_typet::ARRAY_EQUALITY].push_back(
+      equality_expr);
   }
 }
 
@@ -521,8 +524,8 @@ void arrayst::add_array_constraints(
       lazy_constraintt lazy(lazy_typet::ARRAY_TYPECAST,
         equal_exprt(index_expr1, index_expr2));
       add_array_constraint(lazy, false); // added immediately
-      array_constraints_map[
-        constraint_typet::ARRAY_TYPECAST].push_back(lazy.lazy);
+      array_constraints_map[constraint_typet::ARRAY_TYPECAST].push_back(
+        lazy.lazy);
     }
   }
   else if(expr.id()==ID_index)
@@ -561,8 +564,7 @@ void arrayst::add_array_constraints_with(
     lazy_constraintt lazy(
       lazy_typet::ARRAY_WITH, equal_exprt(index_expr, value));
     add_array_constraint(lazy, false); // added immediately
-    array_constraints_map[
-      constraint_typet::ARRAY_WITH].push_back(lazy.lazy);
+    array_constraints_map[constraint_typet::ARRAY_WITH].push_back(lazy.lazy);
 
     updated_indices.insert(index);
   }
@@ -598,8 +600,8 @@ void arrayst::add_array_constraints_with(
                                 literal_exprt(guard_lit)));
 
         add_array_constraint(lazy, false); // added immediately
-        array_constraints_map[
-          constraint_typet::ARRAY_WITH_OTHER].push_back(lazy.lazy);
+        array_constraints_map[constraint_typet::ARRAY_WITH_OTHER].push_back(
+          lazy.lazy);
 
 #if 0 // old code for adding, not significantly faster
         {
@@ -695,8 +697,7 @@ void arrayst::add_array_constraints_array_of(
     lazy_constraintt lazy(
       lazy_typet::ARRAY_OF, equal_exprt(index_expr, expr.what()));
     add_array_constraint(lazy, false); // added immediately
-    array_constraints_map[
-      constraint_typet::ARRAY_OF].push_back(lazy.lazy);
+    array_constraints_map[constraint_typet::ARRAY_OF].push_back(lazy.lazy);
   }
 }
 
@@ -732,8 +733,8 @@ void arrayst::add_array_constraints_array_constant(
       lazy_constraintt lazy{lazy_typet::ARRAY_CONSTANT,
                             equal_exprt{index_expr, v}};
       add_array_constraint(lazy, false); // added immediately
-      array_constraints_map[
-        constraint_typet::ARRAY_CONSTANT].push_back(lazy.lazy);
+      array_constraints_map[constraint_typet::ARRAY_CONSTANT].push_back(
+        lazy.lazy);
     }
     else
     {
@@ -776,8 +777,8 @@ void arrayst::add_array_constraints_array_constant(
           implies_exprt{index_constraint,
                         equal_exprt{index_expr, operands[range.first]}}};
         add_array_constraint(lazy, true); // added lazily
-        array_constraints_map[
-          constraint_typet::ARRAY_NON_CONSTANT].push_back(lazy.lazy);
+        array_constraints_map[constraint_typet::ARRAY_NON_CONSTANT].push_back(
+          lazy.lazy);
       }
     }
   }
@@ -803,8 +804,8 @@ void arrayst::add_array_constraints_comprehension(
       equal_exprt(index_expr, comprehension_body));
 
     add_array_constraint(lazy, false); // added immediately
-    array_constraints_map[
-      constraint_typet::ARRAY_COMPREHENSION].push_back(lazy.lazy);
+    array_constraints_map[constraint_typet::ARRAY_COMPREHENSION].push_back(
+      lazy.lazy);
   }
 }
 
@@ -832,8 +833,7 @@ void arrayst::add_array_constraints_if(
                             or_exprt(literal_exprt(!cond_lit),
                               equal_exprt(index_expr1, index_expr2)));
     add_array_constraint(lazy, false); // added immediately
-    array_constraints_map[
-      constraint_typet::ARRAY_IF_TRUE].push_back(lazy.lazy);
+    array_constraints_map[constraint_typet::ARRAY_IF_TRUE].push_back(lazy.lazy);
 
 #if 0 // old code for adding, not significantly faster
     prop.lcnf(!cond_lit, convert(equal_exprt(index_expr1, index_expr2)));
@@ -853,8 +853,8 @@ void arrayst::add_array_constraints_if(
       or_exprt(literal_exprt(cond_lit),
       equal_exprt(index_expr1, index_expr2)));
     add_array_constraint(lazy, false); // added immediately
-    array_constraints_map[
-      constraint_typet::ARRAY_IF_FALSE].push_back(lazy.lazy);
+    array_constraints_map[constraint_typet::ARRAY_IF_FALSE].push_back(
+      lazy.lazy);
 
 #if 0 // old code for adding, not significantly faster
     prop.lcnf(cond_lit, convert(equal_exprt(index_expr1, index_expr2)));
@@ -866,30 +866,30 @@ std::string arrayst::enum_to_string(constraint_typet type)
 {
   switch(type)
   {
-    case constraint_typet::ARRAY_ACKERMANN:
-      return "arrayAckermann";
-    case constraint_typet::ARRAY_EQUALITY:
-      return "arrayEquality";
-    case constraint_typet::ARRAY_WITH:
-      return "arrayWith";
-    case constraint_typet::ARRAY_WITH_OTHER:
-      return "arrayWithOther";
-    case constraint_typet::ARRAY_IF_TRUE:
-      return "arrayIfTrue";
-    case constraint_typet::ARRAY_IF_FALSE:
-      return "arrayIfFalse";
-    case constraint_typet::ARRAY_OF:
-      return "arrayOf";
-    case constraint_typet::ARRAY_TYPECAST:
-      return "arrayTypecast";
-    case constraint_typet::ARRAY_CONSTANT:
-      return "arrayConstant";
-    case constraint_typet::ARRAY_NON_CONSTANT:
-      return "arrayNonConstant";
-    case constraint_typet::ARRAY_COMPREHENSION:
-      return "arrayComprehension";
-    default:
-      UNREACHABLE;
+  case constraint_typet::ARRAY_ACKERMANN:
+    return "arrayAckermann";
+  case constraint_typet::ARRAY_EQUALITY:
+    return "arrayEquality";
+  case constraint_typet::ARRAY_WITH:
+    return "arrayWith";
+  case constraint_typet::ARRAY_WITH_OTHER:
+    return "arrayWithOther";
+  case constraint_typet::ARRAY_IF_TRUE:
+    return "arrayIfTrue";
+  case constraint_typet::ARRAY_IF_FALSE:
+    return "arrayIfFalse";
+  case constraint_typet::ARRAY_OF:
+    return "arrayOf";
+  case constraint_typet::ARRAY_TYPECAST:
+    return "arrayTypecast";
+  case constraint_typet::ARRAY_CONSTANT:
+    return "arrayConstant";
+  case constraint_typet::ARRAY_NON_CONSTANT:
+    return "arrayNonConstant";
+  case constraint_typet::ARRAY_COMPREHENSION:
+    return "arrayComprehension";
+  default:
+    UNREACHABLE;
   }
 }