Merge pull request #8104 from thomasspriggs/tas/smt-no-implicit-symbol-values

Keep symbols as nondet rather than using their symbol table values in SMT decision procedure.

Author: thomasspriggs

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -5,12 +5,10 @@
 #include <util/arith_tools.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
-#include <util/namespace.h>
 #include <util/range.h>
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 #include <util/string_constant.h>
-#include <util/symbol.h>
 
 #include <solvers/smt2_incremental/ast/smt_commands.h>
 #include <solvers/smt2_incremental/ast/smt_responses.h>
@@ -210,28 +208,12 @@ void smt2_incremental_decision_proceduret::define_dependent_functions(
       continue;
     if(const auto symbol_expr = expr_try_dynamic_cast<symbol_exprt>(current))
     {
-      const irep_idt &identifier = symbol_expr->get_identifier();
-      const symbolt *symbol = nullptr;
-      if(ns.lookup(identifier, symbol) || symbol->value.is_nil())
-      {
-        send_function_definition(
-          *symbol_expr,
-          symbol_expr->get_identifier(),
-          solver_process,
-          expression_identifiers,
-          identifier_table);
-      }
-      else
-      {
-        const exprt lowered = lower(symbol->value);
-        if(push_dependencies_needed(lowered))
-          continue;
-        const smt_define_function_commandt function{
-          symbol->name, {}, convert_expr_to_smt(lowered)};
-        expression_identifiers.emplace(*symbol_expr, function.identifier());
-        identifier_table.emplace(identifier, function.identifier());
-        solver_process->send(function);
-      }
+      send_function_definition(
+        *symbol_expr,
+        symbol_expr->get_identifier(),
+        solver_process,
+        expression_identifiers,
+        identifier_table);
     }
     else if(const auto array_expr = expr_try_dynamic_cast<array_exprt>(current))
       define_array_function(*array_expr);

unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -242,31 +242,7 @@ TEST_CASE(
       REQUIRE(
         test.sent_commands ==
         std::vector<smt_commandt>{
-          smt_declare_function_commandt{nondet_int_a_term, {}},
-          smt_define_function_commandt{
-            "forty_two", {}, smt_bit_vector_constant_termt{42, 16}},
-          smt_define_function_commandt{
-            "first_comparison",
-            {},
-            smt_core_theoryt::equal(nondet_int_a_term, forty_two_term)},
-          smt_declare_function_commandt{nondet_int_b_term, {}},
-          smt_define_function_commandt{
-            "second_comparison",
-            {},
-            smt_core_theoryt::make_not(
-              smt_core_theoryt::equal(nondet_int_b_term, forty_two_term))},
-          smt_define_function_commandt{
-            "third_comparison",
-            {},
-            smt_core_theoryt::equal(nondet_int_a_term, nondet_int_b_term)},
-          smt_define_function_commandt{
-            "comparison_conjunction",
-            {},
-            smt_core_theoryt::make_and(
-              smt_core_theoryt::make_and(
-                smt_identifier_termt{"first_comparison", smt_bool_sortt{}},
-                smt_identifier_termt{"second_comparison", smt_bool_sortt{}}),
-              smt_identifier_termt{"third_comparison", smt_bool_sortt{}})},
+          smt_declare_function_commandt{comparison_conjunction_term, {}},
           smt_assert_commandt{comparison_conjunction_term}});
     }
     SECTION("Set with nondet_padding")
@@ -326,8 +302,8 @@ TEST_CASE(
       REQUIRE(
         test.sent_commands ==
         std::vector<smt_commandt>{
-          smt_define_function_commandt{
-            "bar", {}, smt_bit_vector_constant_termt{42, 8}},
+          smt_declare_function_commandt{
+            smt_identifier_termt{"bar", smt_bit_vector_sortt{8}}, {}},
           smt_define_function_commandt{
             "B0", {}, smt_identifier_termt{"bar", smt_bit_vector_sortt{8}}}});
     }
@@ -1210,19 +1186,9 @@ TEST_CASE(
   test.procedure.set_to(equal_expr, true);
 
   std::vector<smt_commandt> expected_commands{
-    smt_define_function_commandt(
-      inner_symbol_with_value.name,
-      {},
-      smt_bit_vector_theoryt::concat(
-        smt_bit_vector_constant_termt{10, 32},
-        smt_bit_vector_constant_termt{23, 16})),
-    smt_define_function_commandt(
-      symbol_with_value.name,
-      {},
-      smt_bit_vector_theoryt::concat(
-        smt_bit_vector_constant_termt{1, config.ansi_c.bool_width},
-        smt_identifier_termt{
-          inner_symbol_with_value.name, smt_bit_vector_sortt{48}})),
+    smt_declare_function_commandt{
+      smt_identifier_termt{symbol_with_value.name, smt_bit_vector_sortt{56}},
+      {}},
     smt_assert_commandt{smt_core_theoryt::equal(
       smt_identifier_termt{symbol_with_value.name, smt_bit_vector_sortt{56}},
       smt_identifier_termt{symbol_with_value.name, smt_bit_vector_sortt{56}})}};