Add incremental solver interface

Author: peterschrammel

src/solvers/Makefile

@@ -146,6 +146,7 @@ SRC = $(BOOLEFORCE_SRC) \
       bdd/miniBDD/miniBDD.cpp \
       prop/bdd_expr.cpp \
       prop/cover_goals.cpp \
+      prop/incremental_solver.cpp \
       prop/literal.cpp \
       prop/minimize.cpp \
       prop/prop.cpp \

src/solvers/prop/incremental_solver.cpp

@@ -0,0 +1,60 @@
+/*******************************************************************\
+
+Module: Incremental Solver Interface
+
+Author: Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Interface for incremental solvers
+
+#include "incremental_solver.h"
+
+incremental_solvert::incremental_solvert(
+  const namespacet &ns,
+  prop_convt &prop_conv)
+  : prop_convt(ns), prop_conv(prop_conv)
+{
+}
+
+decision_proceduret::resultt incremental_solvert::dec_solve()
+{
+  solver_calls++;
+  return prop_conv.dec_solve();
+}
+
+literalt incremental_solvert::convert(const exprt& expr)
+{
+  return prop_conv.convert(expr);
+}
+
+exprt incremental_solvert::get(const exprt& expr) const
+{
+  return prop_conv.get(expr);
+}
+
+tvt incremental_solvert::l_get(literalt l) const
+{
+  return prop_conv.l_get(l);
+}
+
+std::string incremental_solvert::decision_procedure_text() const
+{
+  return prop_conv.decision_procedure_text();
+}
+
+void incremental_solvert::print_assignment(std::ostream &out) const
+{
+  prop_conv.print_assignment(out);
+}
+
+std::size_t incremental_solvert::get_number_of_solver_calls() const
+{
+  return solver_calls;
+}
+
+prop_convt &incremental_solvert::get_solver() const
+{
+  return prop_conv;
+}

src/solvers/prop/incremental_solver.h

@@ -0,0 +1,64 @@
+/*******************************************************************\
+
+Module: Incremental Solver Interface
+
+Author: Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Interface for incremental solvers
+
+#ifndef CPROVER_SOLVERS_INCREMENTAL_SOLVER_H
+#define CPROVER_SOLVERS_INCREMENTAL_SOLVER_H
+
+#include "prop_conv.h"
+
+/// A `prop_convt` that wraps another `prop_convt` and provides
+/// a push/pop-context interface for incremental solving
+class incremental_solvert : public prop_convt
+{
+public:
+  virtual ~incremental_solvert() = default;
+
+  /// Push a new context on the stack
+  /// This context becomes a child context nested in the current context.
+  virtual void push_context() = 0;
+
+  /// Pop the current context
+  virtual void pop_context() = 0;
+
+  /// Add \p expr to the formula within the current context
+  void set_to(const exprt &expr, bool value) override = 0;
+
+  /// Solve the current formula
+  decision_proceduret::resultt dec_solve() override;
+
+  /// Convert a boolean expression \p expr
+  literalt convert(const exprt &expr) override;
+
+  /// Replace the variables in \p expr by values from the model
+  exprt get(const exprt &expr) const override;
+
+  /// Return the value of the given literal in the model
+  tvt l_get(literalt) const override;
+
+  // return a textual description of the decision procedure
+  std::string decision_procedure_text() const override;
+
+  // print satisfying assignment
+  void print_assignment(std::ostream &out) const override;
+
+  std::size_t get_number_of_solver_calls() const;
+
+  /// Returns the underlying solver
+  prop_convt &get_solver() const;
+
+protected:
+  incremental_solvert(const namespacet &ns, prop_convt &prop_conv);
+
+  prop_convt &prop_conv;
+  std::size_t solver_calls = 0;
+};
+
+#endif // CPROVER_SOLVERS_PROP_INCREMENTAL_SOLVER_H