Add unit test of the get function

Author: thomasspriggs

unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -386,3 +386,70 @@ TEST_CASE(
         "SMT solver does not support given command."});
   }
 }
+
+TEST_CASE(
+  "smt2_incremental_decision_proceduret getting values back from solver.",
+  "[core][smt2_incremental]")
+{
+  decision_procedure_test_environmentt test{};
+  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});
+  const smt_bit_vector_constant_termt term_42{42, 16};
+  SECTION("Set \"foo\" identifier and solve.")
+  {
+    test.sent_commands.clear();
+    const exprt equal_42 = equal_exprt{foo.symbol_expr(), expr_42};
+    test.procedure.set_to(equal_42, true);
+    test.mock_responses.push_back(smt_check_sat_responset{smt_sat_responset{}});
+    test.procedure();
+    REQUIRE(
+      test.sent_commands ==
+      std::vector<smt_commandt>{
+        smt_declare_function_commandt{foo_term, {}},
+        smt_assert_commandt{smt_core_theoryt::equal(foo_term, term_42)},
+        smt_check_sat_commandt{}});
+    SECTION("Get \"foo\" value back")
+    {
+      test.sent_commands.clear();
+      test.mock_responses.push_back(
+        smt_get_value_responset{{{foo_term, term_42}}});
+      REQUIRE(test.procedure.get(foo.symbol_expr()) == expr_42);
+      REQUIRE(
+        test.sent_commands ==
+        std::vector<smt_commandt>{smt_get_value_commandt{foo_term}});
+    }
+    SECTION("Get value of non-set symbol")
+    {
+      // smt2_incremental_decision_proceduret is used this way when cbmc is
+      // invoked with the combination of `--trace` and `--slice-formula`.
+      test.sent_commands.clear();
+      const exprt bar =
+        make_test_symbol("bar", signedbv_typet{16}).symbol_expr();
+      REQUIRE(test.procedure.get(bar) == bar);
+      REQUIRE(test.sent_commands.empty());
+    }
+    SECTION("Get value of type less symbol back")
+    {
+      // smt2_incremental_decision_proceduret is used this way as part of
+      // building the goto trace, to get the partial order concurrency clock
+      // values.
+      test.sent_commands.clear();
+      const symbol_exprt baz = symbol_exprt::typeless("baz");
+      REQUIRE(test.procedure.get(baz) == baz);
+      REQUIRE(test.sent_commands.empty());
+    }
+    SECTION("Get value of trivially solved expression")
+    {
+      test.sent_commands.clear();
+      const smt_termt not_true_term =
+        smt_core_theoryt::make_not(smt_bool_literal_termt{true});
+      test.mock_responses.push_back(smt_get_value_responset{
+        {{not_true_term, smt_bool_literal_termt{false}}}});
+      REQUIRE(test.procedure.get(not_exprt{true_exprt{}}) == false_exprt{});
+      REQUIRE(
+        test.sent_commands ==
+        std::vector<smt_commandt>{smt_get_value_commandt{not_true_term}});
+    }
+  }
+}