SMT2 Incremental: Implement push/pop interface

regression/cbmc/fault_localization-stop_on_fail1/test.desc

@@ -1,4 +1,4 @@
-CORE paths-lifo-expected-failure broken-smt-backend no-new-smt
+CORE paths-lifo-expected-failure broken-smt-backend
 main.c
 --localize-faults --stop-on-fail --no-standard-checks
 ^EXIT=10$

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -635,22 +635,22 @@ void smt2_incremental_decision_proceduret::set_to(
 void smt2_incremental_decision_proceduret::push(
   const std::vector<exprt> &assumptions)
 {
+  push();
   for(const auto &assumption : assumptions)
-  {
-    UNIMPLEMENTED_FEATURE(
-      "pushing of assumption:\n  " + assumption.pretty(2, 0));
-  }
-  UNIMPLEMENTED_FEATURE("`push` of empty assumptions.");
+    set_to(assumption, true);
 }
 
 void smt2_incremental_decision_proceduret::push()
 {
-  UNIMPLEMENTED_FEATURE("`push`.");
+  solver_process->send(smt_push_commandt{1});
+  ++number_of_pushed_contexts;
 }
 
 void smt2_incremental_decision_proceduret::pop()
 {
-  UNIMPLEMENTED_FEATURE("`pop`.");
+  PRECONDITION(number_of_pushed_contexts > 0);
+  solver_process->send(smt_pop_commandt{1});
+  --number_of_pushed_contexts;
 }
 
 [[nodiscard]] static decision_proceduret::resultt

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

@@ -126,6 +126,9 @@ class smt2_incremental_decision_proceduret final
   const namespacet &ns;
   /// The number of times `dec_solve()` has been called.
   size_t number_of_solver_calls;
+  /// The number of currently active pushed solver contexts. Used to
+  /// validate that pop() is not called on an empty stack.
+  std::size_t number_of_pushed_contexts = 0;
   /// \brief For handling the lifetime of and communication with the separate
   ///   SMT solver process.
   /// \note This may be mocked for unit testing purposes.

unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -1197,3 +1197,35 @@ TEST_CASE(
 
   CHECK(test.sent_commands == expected_commands);
 }
+
+TEST_CASE(
+  "smt2_incremental_decision_proceduret push pop.",
+  "[core][smt2_incremental]")
+{
+  auto test = decision_procedure_test_environmentt::make();
+  test.sent_commands.clear();
+  SECTION("push sends push command")
+  {
+    test.procedure.push();
+    REQUIRE(
+      test.sent_commands == std::vector<smt_commandt>{smt_push_commandt{1}});
+    test.sent_commands.clear();
+    SECTION("pop sends pop command")
+    {
+      test.procedure.pop();
+      REQUIRE(
+        test.sent_commands == std::vector<smt_commandt>{smt_pop_commandt{1}});
+    }
+    SECTION("push with assumptions")
+    {
+      const symbolt foo = make_test_symbol("foo", bool_typet{});
+      const smt_identifier_termt foo_term{"foo", smt_bool_sortt{}};
+      test.procedure.push({foo.symbol_expr()});
+      REQUIRE(
+        test.sent_commands == std::vector<smt_commandt>{
+                                smt_push_commandt{1},
+                                smt_declare_function_commandt{foo_term, {}},
+                                smt_assert_commandt{foo_term}});
+    }
+  }
+}