Add context-based incremental solver interface

Allows to use incremental solvers using
a push/pop interface.

Author: peterschrammel

src/solvers/Makefile

@@ -145,6 +145,7 @@ SRC = $(BOOLEFORCE_SRC) \
       lowering/popcount.cpp \
       bdd/miniBDD/miniBDD.cpp \
       prop/bdd_expr.cpp \
+      prop/context_solver.cpp \
       prop/cover_goals.cpp \
       prop/literal.cpp \
       prop/minimize.cpp \

src/solvers/prop/context_solver.cpp

@@ -0,0 +1,106 @@
+/*******************************************************************\
+
+Module: Context-based Incremental Solver Interface
+
+Author: Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Context-based interface for incremental solvers
+
+#include "context_solver.h"
+
+#include <util/invariant.h>
+
+context_solvert::context_solvert(prop_convt &prop_conv)
+  : prop_convt(), prop_conv(prop_conv)
+{
+}
+
+decision_proceduret::resultt context_solvert::dec_solve()
+{
+  return prop_conv.dec_solve();
+}
+
+literalt context_solvert::convert(const exprt &expr)
+{
+  return prop_conv.convert(expr);
+}
+
+exprt context_solvert::get(const exprt &expr) const
+{
+  return prop_conv.get(expr);
+}
+
+tvt context_solvert::l_get(literalt l) const
+{
+  return prop_conv.l_get(l);
+}
+
+std::string context_solvert::decision_procedure_text() const
+{
+  return prop_conv.decision_procedure_text();
+}
+
+void context_solvert::print_assignment(std::ostream &out) const
+{
+  prop_conv.print_assignment(out);
+}
+
+void context_solvert::set_frozen(literalt)
+{
+  // unsupported
+  UNREACHABLE;
+}
+
+void context_solvert::set_frozen(const bvt &)
+{
+  // unsupported
+  UNREACHABLE;
+}
+
+void context_solvert::set_assumptions(const bvt &_assumptions)
+{
+  // unsupported
+  UNREACHABLE;
+}
+
+bool context_solvert::has_set_assumptions() const
+{
+  // unsupported
+  return false;
+}
+
+void context_solvert::set_all_frozen()
+{
+  // unsupported
+  UNREACHABLE;
+}
+
+bool context_solvert::is_in_conflict(literalt l) const
+{
+  // unsupported
+  UNREACHABLE;
+}
+
+bool context_solvert::has_is_in_conflict() const
+{
+  // unsupported
+  return false;
+}
+
+void context_solvert::set_time_limit_seconds(uint32_t limit)
+{
+  prop_conv.set_time_limit_seconds(limit);
+}
+
+std::size_t context_solvert::get_number_of_solver_calls() const
+{
+  return prop_conv.get_number_of_solver_calls();
+}
+
+prop_convt &context_solvert::get_solver() const
+{
+  return prop_conv;
+}

src/solvers/prop/context_solver.h

@@ -0,0 +1,88 @@
+/*******************************************************************\
+
+Module: Context-based Incremental Solver Interface
+
+Author: Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Context-based interface for incremental solvers
+
+#ifndef CPROVER_SOLVERS_PROP_CONTEXT_SOLVER_H
+#define CPROVER_SOLVERS_PROP_CONTEXT_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 context_solvert : public prop_convt
+{
+public:
+  /// 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;
+
+  /// Not supported
+  void set_frozen(literalt) override;
+
+  /// Not supported
+  void set_frozen(const bvt &) override;
+
+  /// Not supported
+  void set_assumptions(const bvt &) override;
+
+  /// Not supported
+  bool has_set_assumptions() const override;
+
+  /// Not supported
+  void set_all_frozen() override;
+
+  /// Not supported
+  bool is_in_conflict(literalt) const override;
+
+  /// Not supported
+  bool has_is_in_conflict() const override;
+
+  // Set resource limits
+  void set_time_limit_seconds(uint32_t) override;
+
+  /// Returns the number of incremental solver calls
+  std::size_t get_number_of_solver_calls() const override;
+
+  /// Returns the underlying solver
+  prop_convt &get_solver() const;
+
+  virtual ~context_solvert() = default;
+
+protected:
+  explicit context_solvert(prop_convt &prop_conv);
+
+  prop_convt &prop_conv;
+};
+
+#endif // CPROVER_SOLVERS_PROP_CONTEXT_SOLVER_H