Incremental solver implementation for propt-based solvers

Allows us to use, e.g. bv_refinementt, incrementally
with a push/pop 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_prop_conv_solver.cpp \
       prop/incremental_solver.cpp \
       prop/literal.cpp \
       prop/minimize.cpp \

src/solvers/prop/incremental_prop_conv_solver.cpp

@@ -0,0 +1,54 @@
+/*******************************************************************\
+
+Module: Incremental wrapper for propt based refinement solvers
+
+Author: Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Incremental wrapper for `propt`-based refinement solvers
+
+#include "incremental_prop_conv_solver.h"
+
+incremental_prop_conv_solvert::incremental_prop_conv_solvert(
+  const namespacet &ns,
+  prop_convt &prop_conv)
+  : incremental_solvert(ns, prop_conv)
+{
+}
+
+void incremental_prop_conv_solvert::set_to(const exprt &expr, bool value)
+{
+  if(context_literals.empty())
+  {
+    // We are in the root context.
+    prop_conv.set_to(expr, value);
+  }
+  else
+  {
+    // We have a child context. We add context_literal ==> expr to the formula.
+    prop_conv.set_to(
+      or_exprt(literal_exprt(!context_literals.back()), expr), value);
+  }
+}
+
+void incremental_prop_conv_solvert::push_context()
+{
+  // We create a new context literal.
+  literalt context_literal = prop_conv.convert(symbol_exprt(
+    "symex::context$" + std::to_string(context_literal_counter++),
+    bool_typet()));
+
+  context_literals.push_back(context_literal);
+  prop_conv.set_assumptions(context_literals);
+}
+
+void incremental_prop_conv_solvert::pop_context()
+{
+  PRECONDITION(!context_literals.empty());
+
+  // We remove the last context literal from the stack.
+  context_literals.pop_back();
+  prop_conv.set_assumptions(context_literals);
+}

src/solvers/prop/incremental_prop_conv_solver.h

@@ -0,0 +1,38 @@
+/*******************************************************************\
+
+Module: Incremental wrapper for propt based refinement solvers
+
+Author: Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Incremental wrapper for `propt`-based refinement solvers
+
+#ifndef CPROVER_SOLVERS_INCREMENTAL_PROP_CONV_SOLVER_H
+#define CPROVER_SOLVERS_INCREMENTAL_PROP_CONV_SOLVER_H
+
+#include "incremental_solver.h"
+
+/// Provides a push/pop-context interface for incremental solving
+/// to `propt`-based solvers such as `bv_refinementt`.
+class incremental_prop_conv_solvert : public incremental_solvert
+{
+public:
+  incremental_prop_conv_solvert(const namespacet &ns, prop_convt &prop_conv);
+
+  void set_to(const exprt &expr, bool value) override;
+
+  void push_context() override;
+
+  void pop_context() override;
+
+protected:
+  // context literals used as assumptions
+  bvt context_literals;
+
+  // unique context literal names
+  std::size_t context_literal_counter = 0;
+};
+
+#endif // CPROVER_SOLVERS_PROP_INCREMENTAL_PROP_CONV_SOLVER_H