Add push and pop commands

Author: thomasspriggs

src/solvers/smt2_incremental/smt_commands.cpp

@@ -121,3 +121,25 @@ const smt_termt &smt_get_value_commandt::descriptor() const
 {
   return downcast(find(ID_value));
 }
+
+smt_push_commandt::smt_push_commandt(std::size_t levels)
+  : smt_commandt(ID_smt_push_command)
+{
+  set_size_t(ID_value, levels);
+}
+
+size_t smt_push_commandt::levels() const
+{
+  return get_size_t(ID_value);
+}
+
+smt_pop_commandt::smt_pop_commandt(std::size_t levels)
+  : smt_commandt(ID_smt_pop_command)
+{
+  set_size_t(ID_value, levels);
+}
+
+size_t smt_pop_commandt::levels() const
+{
+  return get_size_t(ID_value);
+}

src/solvers/smt2_incremental/smt_commands.def

@@ -10,5 +10,7 @@ COMMAND_ID(declare_function)
 COMMAND_ID(define_function)
 COMMAND_ID(exit)
 COMMAND_ID(get_value)
+COMMAND_ID(pop)
+COMMAND_ID(push)
 COMMAND_ID(set_logic)
 COMMAND_ID(set_option)

src/solvers/smt2_incremental/smt_commands.h

@@ -79,6 +79,20 @@ class smt_get_value_commandt : public smt_commandt,
   const smt_termt &descriptor() const;
 };
 
+class smt_push_commandt : public smt_commandt
+{
+public:
+  explicit smt_push_commandt(std::size_t levels);
+  size_t levels() const;
+};
+
+class smt_pop_commandt : public smt_commandt
+{
+public:
+  explicit smt_pop_commandt(std::size_t levels);
+  size_t levels() const;
+};
+
 class smt_set_logic_commandt : public smt_commandt
 {
 public:

unit/solvers/smt2_incremental/smt_commands.cpp

@@ -76,3 +76,15 @@ TEST_CASE("smt_commandt equality", "[core][smt2_incremental]")
   const smt_assert_commandt assert_false{smt_bool_literal_termt{false}};
   CHECK_FALSE(assert_true == assert_false);
 }
+
+TEST_CASE("smt_push_commandt level", "[core][smt2_incremental]")
+{
+  CHECK(smt_push_commandt(1).levels() == 1);
+  CHECK(smt_push_commandt(2).levels() == 2);
+}
+
+TEST_CASE("smt_pop_commandt level", "[core][smt2_incremental]")
+{
+  CHECK(smt_pop_commandt(1).levels() == 1);
+  CHECK(smt_pop_commandt(2).levels() == 2);
+}