Send is_dynamic object declaration and defintion to solver

In preparation for calling the new function in the conversion of
is_dynamic_object expressions to SMT terms.

Author: thomasspriggs

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -255,6 +255,7 @@ smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret(
     smt_set_option_commandt{smt_option_produce_modelst{true}});
   solver_process->send(smt_set_logic_commandt{smt_logic_allt{}});
   solver_process->send(object_size_function.declaration);
+  solver_process->send(is_dynamic_object_function.declaration);
 }
 
 void smt2_incremental_decision_proceduret::ensure_handle_for_expr_defined(
@@ -561,6 +562,8 @@ void smt2_incremental_decision_proceduret::define_object_sizes()
     define_dependent_functions(object.size);
     solver_process->send(object_size_function.make_definition(
       object.unique_id, convert_expr_to_smt(object.size)));
+    solver_process->send(is_dynamic_object_function.make_definition(
+      object.unique_id, object.is_dynamic));
   }
 }
 

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

@@ -11,6 +11,7 @@
 
 #include <solvers/smt2_incremental/ast/smt_terms.h>
 #include <solvers/smt2_incremental/object_tracking.h>
+#include <solvers/smt2_incremental/smt_is_dynamic_object.h>
 #include <solvers/smt2_incremental/smt_object_size.h>
 #include <solvers/smt2_incremental/type_size_mapping.h>
 #include <solvers/stack_decision_procedure.h>
@@ -159,6 +160,11 @@ class smt2_incremental_decision_proceduret final
   /// 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.
   smt_object_sizet object_size_function;
+  /// Implementation of the SMT formula for the dynamic object status lookup
+  /// 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.
+  smt_is_dynamic_objectt is_dynamic_object_function;
   /// Precalculated type sizes used for pointer arithmetic.
   type_size_mapt pointer_sizes_map;
 };

unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -113,6 +113,7 @@ struct decision_procedure_test_environmentt final
   std::vector<smt_commandt> sent_commands;
   null_message_handlert message_handler;
   smt_object_sizet object_size_function;
+  smt_is_dynamic_objectt is_dynamic_object_function;
   smt2_incremental_decision_proceduret procedure{
     ns,
     util_make_unique<smt_mock_solver_processt>(
@@ -177,7 +178,8 @@ TEST_CASE(
       std::vector<smt_commandt>{
         smt_set_option_commandt{smt_option_produce_modelst{true}},
         smt_set_logic_commandt{smt_logic_allt{}},
-        test.object_size_function.declaration});
+        test.object_size_function.declaration,
+        test.is_dynamic_object_function.declaration});
     test.sent_commands.clear();
     SECTION("Set symbol to true.")
     {
@@ -464,6 +466,10 @@ TEST_CASE(
   const auto invalid_pointer_object_size_definition =
     test.object_size_function.make_definition(
       1, smt_bit_vector_constant_termt{0, 32});
+  const auto null_object_dynamic_definition =
+    test.is_dynamic_object_function.make_definition(0, false);
+  const auto invalid_pointer_object_dynamic_definition =
+    test.is_dynamic_object_function.make_definition(1, false);
   const symbolt foo = make_test_symbol("foo", signedbv_typet{16});
   const smt_identifier_termt foo_term{"foo", smt_bit_vector_sortt{16}};
   const exprt expr_42 = from_integer({42}, signedbv_typet{16});
@@ -480,6 +486,8 @@ TEST_CASE(
       smt_assert_commandt{smt_core_theoryt::equal(foo_term, term_42)},
       invalid_pointer_object_size_definition,
       null_object_size_definition,
+      null_object_dynamic_definition,
+      invalid_pointer_object_dynamic_definition,
       smt_check_sat_commandt{}};
     REQUIRE(
       (test.sent_commands.size() == expected_commands.size() &&