Context 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

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

src/solvers/prop/context_prop_conv_solver.cpp

@@ -0,0 +1,55 @@
+/*******************************************************************\
+
+Module: Push/pop-context wrapper for propt-based refinement solvers
+
+Author: Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Push/pop-context wrapper for `propt`-based refinement solvers
+
+#include "context_prop_conv_solver.h"
+
+context_prop_conv_solvert::context_prop_conv_solvert(prop_convt &prop_conv)
+  : context_solvert(prop_conv)
+{
+}
+
+const std::string context_prop_conv_solvert::context_prefix =
+  "prop_conv::context$";
+
+void context_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 context_prop_conv_solvert::push_context()
+{
+  // We create a new context literal.
+  literalt context_literal = prop_conv.convert(symbol_exprt(
+    context_prefix + std::to_string(context_literal_counter++),
+    bool_typet()));
+
+  context_literals.push_back(context_literal);
+  prop_conv.set_assumptions(context_literals);
+}
+
+void context_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/context_prop_conv_solver.h

@@ -0,0 +1,39 @@
+/*******************************************************************\
+
+Module: Push/pop-context wrapper for propt-based refinement solvers
+
+Author: Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Push/pop-context wrapper for `propt`-based refinement solvers
+
+#ifndef CPROVER_SOLVERS_CONTEXT_PROP_CONV_SOLVER_H
+#define CPROVER_SOLVERS_CONTEXT_PROP_CONV_SOLVER_H
+
+#include "context_solver.h"
+
+/// Provides a push/pop-context interface for incremental solving
+/// to `propt`-based solvers such as `bv_refinementt`.
+class context_prop_conv_solvert : public context_solvert
+{
+public:
+  explicit context_prop_conv_solvert(prop_convt &prop_conv);
+
+  void set_to(const exprt &expr, bool value) override;
+
+  void push_context() override;
+
+  void pop_context() override;
+
+  static const std::string context_prefix;
+protected:
+  // context literals used as assumptions
+  bvt context_literals;
+
+  // unique context literal names
+  std::size_t context_literal_counter = 0;
+};
+
+#endif // CPROVER_SOLVERS_PROP_CONTEXT_PROP_CONV_SOLVER_H