Rename define_object_sizes to define_object_properties

Because this now covers both the size and the definition of whether the
object is dynamic or not.

Author: thomasspriggs

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -549,16 +549,16 @@ static decision_proceduret::resultt lookup_decision_procedure_result(
   UNREACHABLE;
 }
 
-void smt2_incremental_decision_proceduret::define_object_sizes()
+void smt2_incremental_decision_proceduret::define_object_properties()
 {
-  object_size_defined.resize(object_map.size());
+  object_properties_defined.resize(object_map.size());
   for(const auto &key_value : object_map)
   {
     const decision_procedure_objectt &object = key_value.second;
-    if(object_size_defined[object.unique_id])
+    if(object_properties_defined[object.unique_id])
       continue;
     else
-      object_size_defined[object.unique_id] = true;
+      object_properties_defined[object.unique_id] = true;
     define_dependent_functions(object.size);
     solver_process->send(object_size_function.make_definition(
       object.unique_id, convert_expr_to_smt(object.size)));
@@ -570,7 +570,7 @@ void smt2_incremental_decision_proceduret::define_object_sizes()
 decision_proceduret::resultt smt2_incremental_decision_proceduret::dec_solve()
 {
   ++number_of_solver_calls;
-  define_object_sizes();
+  define_object_properties();
   const smt_responset result = get_response_to_command(
     *solver_process, smt_check_sat_commandt{}, identifier_table);
   if(const auto check_sat_response = result.cast<smt_check_sat_responset>())

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

@@ -93,8 +93,9 @@ class smt2_incremental_decision_proceduret final
   /// \note This function is non-const because it mutates the object_map.
   smt_termt convert_expr_to_smt(const exprt &expr);
   void define_index_identifiers(const exprt &expr);
-  /// Sends the solver the definitions of the object sizes.
-  void define_object_sizes();
+  /// Sends the solver the definitions of the object sizes and dynamic memory
+  /// statuses.
+  void define_object_properties();
 
   /// Namespace for looking up the expressions which symbol_exprts relate to.
   /// This includes the symbols defined outside of the decision procedure but
@@ -150,12 +151,12 @@ class smt2_incremental_decision_proceduret final
   /// This map is used to track object related state. See documentation in
   /// object_tracking.h for details.
   smt_object_mapt object_map;
-  /// The size of each object is separately defined as a pre-solving step.
-  /// `object_size_defined[object ID]` is set to true for objects where the size
-  /// has been defined. This is used to avoid defining the size of the same
-  /// object multiple times in the case where multiple rounds of solving are
-  /// carried out.
-  std::vector<bool> object_size_defined;
+  /// The size of each object and the dynamic object stus is separately defined
+  /// as a pre-solving step. `object_properties_defined[object ID]` is set to
+  /// true for objects where the size has been defined. This is used to avoid
+  /// defining the size of the same object multiple times in the case where
+  /// multiple rounds of solving are carried out.
+  std::vector<bool> object_properties_defined;
   /// Implementation of the SMT formula for the object size function. This is
   /// stateful because it depends on the configuration of the number of object
   /// bits and how many bits wide the size type is configured to be.