Allow getting context-based incremental solver

Puts the type check into a single place

Author: peterschrammel

src/goto-checker/solver_factory.cpp

@@ -25,6 +25,8 @@ Author: Daniel Kroening, Peter Schrammel
 #endif
 
 #include <solvers/flattening/bv_dimacs.h>
+#include <solvers/prop/decision_procedure_assumptions.h>
+#include <solvers/prop/decision_procedure_contexts.h>
 #include <solvers/prop/decision_procedure_incremental.h>
 #include <solvers/prop/prop.h>
 #include <solvers/prop/solver_resource_limits.h>
@@ -92,6 +94,17 @@ solver_factoryt::solvert::decision_procedure_assumptions() const
   return *solver;
 }
 
+decision_procedure_contextst &
+solver_factoryt::solvert::decision_procedure_contexts() const
+{
+  PRECONDITION(decision_procedure_ptr != nullptr);
+  decision_procedure_contextst *solver =
+    dynamic_cast<decision_procedure_contextst *>(&*decision_procedure_ptr);
+  INVARIANT(
+    solver != nullptr, "incremental decision procedure with contexts required");
+  return *solver;
+}
+
 propt &solver_factoryt::solvert::prop() const
 {
   PRECONDITION(prop_ptr != nullptr);

src/goto-checker/solver_factory.h

@@ -21,6 +21,7 @@ Author: Daniel Kroening, Peter Schrammel
 class message_handlert;
 class namespacet;
 class optionst;
+class decision_procedure_contextst;
 class decision_procedure_incrementalt;
 class decision_procedure_assumptionst;
 
@@ -49,6 +50,7 @@ class solver_factoryt
     decision_proceduret &decision_procedure() const;
     decision_procedure_incrementalt &decision_procedure_incremental() const;
     decision_procedure_assumptionst &decision_procedure_assumptions() const;
+    decision_procedure_contextst &decision_procedure_contexts() const;
     propt &prop() const;
 
     void set_decision_procedure(std::unique_ptr<decision_proceduret> p);