Split out is_in_conflict solver capability

This is only provided by the prop_conv_solvert-based hierarchy
at the moment and is quite specific to MiniSAT-based solvers.
The functionality itself is used out-of-tree only (2LS).

Author: peterschrammel

src/solvers/prop/decision_procedure_assumptions.h

@@ -20,9 +20,6 @@ class decision_procedure_assumptionst : public decision_procedure_incrementalt
   /// Set assumptions for the next call to operator() to solve the problem
   virtual void set_assumptions(const bvt &) = 0;
 
-  /// Returns true if an assumption is in the final conflict
-  virtual bool is_in_conflict(literalt l) const = 0;
-
   virtual ~decision_procedure_assumptionst() = default;
 };
 

src/solvers/prop/prop_conv_solver.h

@@ -20,9 +20,11 @@ Author: Daniel Kroening, [email protected]
 #include "literal.h"
 #include "literal_expr.h"
 #include "prop.h"
+#include "solver_conflicts.h"
 #include "solver_resource_limits.h"
 
 class prop_conv_solvert : public decision_procedure_assumptionst,
+                          public solver_conflictst,
                           public solver_resource_limitst
 {
 public:

src/solvers/prop/solver_conflicts.h

@@ -0,0 +1,28 @@
+/*******************************************************************\
+
+Module: Capability to return assumptions that are in a conflict
+        when solving under assumptions
+
+Author: Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Capability to return assumptions that are in a conflict
+//  when solving under assumptions
+
+#ifndef CPROVER_SOLVERS_PROP_SOLVER_CONFLICTS_H
+#define CPROVER_SOLVERS_PROP_SOLVER_CONFLICTS_H
+
+class literalt;
+
+class solver_conflictst
+{
+public:
+  /// Returns true if an assumption is in the final conflict
+  virtual bool is_in_conflict(literalt) const = 0;
+
+  virtual ~solver_conflictst() = default;
+};
+
+#endif // CPROVER_SOLVERS_PROP_SOLVER_CONFLICTS_H