Add incremental smt2 solving to solver factory

Because the new smt2 incremental support is being initially introduced
in parallel to the existing support, we need the solver factory to make
the new separate solver when the new option is specified.

Author: thomasspriggs

src/goto-checker/solver_factory.cpp

@@ -32,6 +32,7 @@ Author: Daniel Kroening, Peter Schrammel
 #include <solvers/sat/dimacs_cnf.h>
 #include <solvers/sat/external_sat.h>
 #include <solvers/sat/satcheck.h>
+#include <solvers/smt2_incremental/smt2_incremental_decision_procedure.h>
 #include <solvers/strings/string_refinement.h>
 
 solver_factoryt::solver_factoryt(
@@ -140,6 +141,10 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_solver()
   }
   else if(options.get_bool_option("refine-strings"))
     return get_string_refinement();
+  const auto incremental_smt2_solver =
+    options.get_option("incremental-smt2-solver");
+  if(!incremental_smt2_solver.empty())
+    return get_incremental_smt2(incremental_smt2_solver);
   if(options.get_bool_option("smt2"))
     return get_smt2(get_smt2_solver_type());
   return get_default();
@@ -321,6 +326,16 @@ solver_factoryt::get_string_refinement()
     std::move(decision_procedure), std::move(prop));
 }
 
+std::unique_ptr<solver_factoryt::solvert>
+solver_factoryt::get_incremental_smt2(std::string solver_command)
+{
+  no_beautification();
+
+  return util_make_unique<solvert>(
+    util_make_unique<smt2_incremental_decision_proceduret>(
+      std::move(solver_command)));
+}
+
 std::unique_ptr<solver_factoryt::solvert>
 solver_factoryt::get_smt2(smt2_dect::solvert solver)
 {

src/goto-checker/solver_factory.h

@@ -75,6 +75,7 @@ class solver_factoryt final
   std::unique_ptr<solvert> get_external_sat();
   std::unique_ptr<solvert> get_bv_refinement();
   std::unique_ptr<solvert> get_string_refinement();
+  std::unique_ptr<solvert> get_incremental_smt2(std::string solver_command);
   std::unique_ptr<solvert> get_smt2(smt2_dect::solvert solver);
 
   smt2_dect::solvert get_smt2_solver_type() const;

src/solvers/Makefile

@@ -192,6 +192,7 @@ SRC = $(BOOLEFORCE_SRC) \
       smt2/smt2_parser.cpp \
       smt2/smt2_tokenizer.cpp \
       smt2/smt2irep.cpp \
+      smt2_incremental/smt2_incremental_decision_procedure.cpp \
       # Empty last line
 
 include ../common

src/solvers/smt2_incremental/module_dependencies.txt

@@ -0,0 +1,2 @@
+solvers
+util

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -0,0 +1,69 @@
+// Author: Diffblue Ltd.
+
+#include "smt2_incremental_decision_procedure.h"
+
+#include <util/expr.h>
+
+smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret(
+  std::string solver_command)
+  : solver_command{std::move(solver_command)}
+{
+}
+
+exprt smt2_incremental_decision_proceduret::handle(const exprt &expr)
+{
+  UNIMPLEMENTED;
+  return exprt();
+}
+
+exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const
+{
+  UNIMPLEMENTED;
+  return exprt();
+}
+
+void smt2_incremental_decision_proceduret::print_assignment(
+  std::ostream &out) const
+{
+  UNIMPLEMENTED;
+}
+
+std::string
+smt2_incremental_decision_proceduret::decision_procedure_text() const
+{
+  return "incremental SMT2 solving via \"" + solver_command + "\"";
+}
+
+std::size_t
+smt2_incremental_decision_proceduret::get_number_of_solver_calls() const
+{
+  UNIMPLEMENTED;
+  return 0;
+}
+
+void smt2_incremental_decision_proceduret::set_to(const exprt &expr, bool value)
+{
+  UNIMPLEMENTED;
+}
+
+void smt2_incremental_decision_proceduret::push(
+  const std::vector<exprt> &assumptions)
+{
+  UNIMPLEMENTED;
+}
+
+void smt2_incremental_decision_proceduret::push()
+{
+  UNIMPLEMENTED;
+}
+
+void smt2_incremental_decision_proceduret::pop()
+{
+  UNIMPLEMENTED;
+}
+
+decision_proceduret::resultt smt2_incremental_decision_proceduret::dec_solve()
+{
+  UNIMPLEMENTED;
+  return decision_proceduret::resultt::D_SATISFIABLE;
+}

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

@@ -0,0 +1,40 @@
+// Author: Diffblue Ltd.
+
+/// \file
+/// Decision procedure with incremental SMT2 solving.
+
+#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H
+#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H
+
+#include <solvers/stack_decision_procedure.h>
+
+class smt2_incremental_decision_proceduret final
+  : public stack_decision_proceduret
+{
+public:
+  /// \param solver_command: The command and arguments for invoking the smt2
+  ///                        solver.
+  explicit smt2_incremental_decision_proceduret(std::string solver_command);
+
+  // Implementation of public decision_proceduret member functions.
+  exprt handle(const exprt &expr) override;
+  exprt get(const exprt &expr) const override;
+  void print_assignment(std::ostream &out) const override;
+  std::string decision_procedure_text() const override;
+  std::size_t get_number_of_solver_calls() const override;
+  void set_to(const exprt &expr, bool value) override;
+
+  // Implementation of public stack_decision_proceduret member functions.
+  void push(const std::vector<exprt> &assumptions) override;
+  void push() override;
+  void pop() override;
+
+protected:
+  // Implementation of protected decision_proceduret member function.
+  resultt dec_solve() override;
+
+  /// This is where we store the solver command for reporting the solver used.
+  std::string solver_command;
+};
+
+#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H