track number of constraints of different types rather than the actual constraints

Author: Natasha Yogananda Jeppu

src/solvers/flattening/arrays.cpp

@@ -16,7 +16,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/replace_expr.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
-
 #include <util/ui_message.h>
 
 #include <solvers/prop/prop.h>
@@ -39,6 +38,7 @@ arrayst::arrayst(
 {
   lazy_arrays = false;        // will be set to true when --refine is used
   incremental_cache = false;  // for incremental solving
+  // get_array_constraints is true when --show-array-constraints is used
   get_array_constraints = _get_array_constraints;
 }
 
@@ -374,8 +374,7 @@ 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_constraint_count[constraint_typet::ARRAY_ACKERMANN]++;
 
 #if 0 // old code for adding, not significantly faster
             prop.lcnf(!indices_equal_lit, convert(values_equal));
@@ -462,8 +461,7 @@ 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_constraint_count[constraint_typet::ARRAY_EQUALITY]++;
   }
 }
 
@@ -524,8 +522,7 @@ 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_constraint_count[constraint_typet::ARRAY_TYPECAST]++;
     }
   }
   else if(expr.id()==ID_index)
@@ -564,7 +561,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_constraint_count[constraint_typet::ARRAY_WITH]++;
 
     updated_indices.insert(index);
   }
@@ -600,8 +597,7 @@ 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_constraint_count[constraint_typet::ARRAY_WITH]++;
 
 #if 0 // old code for adding, not significantly faster
         {
@@ -697,7 +693,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_constraint_count[constraint_typet::ARRAY_OF]++;
   }
 }
 
@@ -733,8 +729,7 @@ 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_constraint_count[constraint_typet::ARRAY_CONSTANT]++;
     }
     else
     {
@@ -777,8 +772,7 @@ 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_constraint_count[constraint_typet::ARRAY_CONSTANT]++;
       }
     }
   }
@@ -804,8 +798,7 @@ 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_constraint_count[constraint_typet::ARRAY_COMPREHENSION]++;
   }
 }
 
@@ -833,7 +826,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_constraint_count[constraint_typet::ARRAY_IF]++;
 
 #if 0 // old code for adding, not significantly faster
     prop.lcnf(!cond_lit, convert(equal_exprt(index_expr1, index_expr2)));
@@ -853,8 +846,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_FALSE].push_back(
-      lazy.lazy);
+    array_constraint_count[constraint_typet::ARRAY_IF]++;
 
 #if 0 // old code for adding, not significantly faster
     prop.lcnf(cond_lit, convert(equal_exprt(index_expr1, index_expr2)));
@@ -868,56 +860,41 @@ std::string arrayst::enum_to_string(constraint_typet 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_IF:
+    return "arrayIf";
   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";
+  case constraint_typet::ARRAY_EQUALITY:
+    return "arrayEquality";
   default:
     UNREACHABLE;
   }
 }
 
-void arrayst::display_constraints()
+void arrayst::display_array_constraint_count()
 {
   json_objectt json_result;
   json_objectt &json_array_theory =
     json_result["arrayConstraints"].make_object();
 
   size_t num_constraints = 0;
 
-  array_constraints_mapt::iterator it = array_constraints_map.begin();
-  while(it != array_constraints_map.end())
+  array_constraint_countt::iterator it = array_constraint_count.begin();
+  while(it != array_constraint_count.end())
   {
     std::string contraint_type_string = enum_to_string(it->first);
-    json_arrayt &json_constraint_list =
-      json_array_theory[contraint_type_string].make_array();
-
-    array_constraintst::iterator constraint_it = it->second.begin();
-    while(constraint_it != it->second.end())
-    {
-      std::stringstream ss;
-      ss << format(*constraint_it);
-      json_constraint_list.push_back(json_stringt(ss.str()));
+    json_array_theory[contraint_type_string] =
+      json_numbert(std::to_string(it->second));
 
-      constraint_it++;
-      num_constraints++;
-    }
+    num_constraints += it->second;
     it++;
   }
 

src/solvers/flattening/arrays.h

@@ -41,7 +41,7 @@ class arrayst:public equalityt
     post_process_arrays();
     SUB::post_process();
     if(get_array_constraints)
-      display_constraints();
+      display_array_constraint_count();
   }
 
   // NOLINTNEXTLINE(readability/identifiers)
@@ -82,27 +82,6 @@ class arrayst:public equalityt
   typedef std::map<std::size_t, index_sett> index_mapt;
   index_mapt index_map;
 
-  enum class constraint_typet
-  {
-    ARRAY_ACKERMANN,
-    ARRAY_EQUALITY,
-    ARRAY_WITH,
-    ARRAY_WITH_OTHER,
-    ARRAY_IF_TRUE,
-    ARRAY_IF_FALSE,
-    ARRAY_OF,
-    ARRAY_TYPECAST,
-    ARRAY_CONSTANT,
-    ARRAY_NON_CONSTANT,
-    ARRAY_COMPREHENSION
-  };
-
-  typedef std::list<exprt> array_constraintst;
-  typedef std::map<constraint_typet, array_constraintst> array_constraints_mapt;
-  array_constraints_mapt array_constraints_map;
-  void display_constraints();
-  std::string enum_to_string(constraint_typet);
-
   // adds array constraints lazily
   enum class lazy_typet
   {
@@ -134,6 +113,23 @@ class arrayst:public equalityt
   void add_array_constraint(const lazy_constraintt &lazy, bool refine = true);
   std::map<exprt, bool> expr_map;
 
+  enum class constraint_typet
+  {
+    ARRAY_ACKERMANN,
+    ARRAY_WITH,
+    ARRAY_IF,
+    ARRAY_OF,
+    ARRAY_TYPECAST,
+    ARRAY_CONSTANT,
+    ARRAY_COMPREHENSION,
+    ARRAY_EQUALITY
+  };
+
+  typedef std::map<constraint_typet, size_t> array_constraint_countt;
+  array_constraint_countt array_constraint_count;
+  void display_array_constraint_count();
+  std::string enum_to_string(constraint_typet);
+
   // adds all the constraints eagerly
   void add_array_constraints();
   void add_array_Ackermann_constraints();