Decision procedure interface for solving with contexts/assumptions

Provides combined push/pop + assumptions interface

Author: peterschrammel

src/solvers/stack_decision_procedure.h

@@ -0,0 +1,43 @@
+/*******************************************************************\
+
+Module: Decision procedure with incremental solving with contexts
+        and assumptions
+
+Author: Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Decision procedure with incremental solving with contexts
+/// and assumptions
+
+#ifndef CPROVER_SOLVERS_STACK_DECISION_PROCEDURE_H
+#define CPROVER_SOLVERS_STACK_DECISION_PROCEDURE_H
+
+#include <vector>
+
+#include "decision_procedure.h"
+
+class stack_decision_proceduret : public decision_proceduret
+{
+public:
+  /// Pushes a new context on the stack that consists of the given
+  /// (possibly empty vector of) \p assumptions.
+  /// This context becomes a child context nested in the current context.
+  /// An assumption is usually obtained by calling
+  /// `decision_proceduret::handle`. Thus it can be a Boolean expression or
+  /// something more solver-specific such as `literal_exprt`.
+  /// An empty vector of assumptions counts as an element on the stack.
+  virtual void push(const std::vector<exprt> &assumptions) = 0;
+
+  /// Push a new context on the stack
+  /// This context becomes a child context nested in the current context.
+  virtual void push() = 0;
+
+  /// Pop whatever has been pushed in the last call to `push`
+  virtual void pop() = 0;
+
+  virtual ~stack_decision_proceduret() = default;
+};
+
+#endif // CPROVER_SOLVERS_STACK_DECISION_PROCEDURE_H