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

src/solvers/smt2/smt2_conv.cpp

@@ -75,13 +75,6 @@ void smt2_convt::set_all_frozen()
   // not needed
 }
 
-bool smt2_convt::is_in_conflict(literalt l) const
-{
-  // we cannot do that
-  UNREACHABLE;
-  return false;
-}
-
 void smt2_convt::write_header()
 {
   out << "; SMT 2" << "\n";

src/solvers/smt2/smt2_conv.h

@@ -116,7 +116,6 @@ class smt2_convt : public decision_procedure_assumptionst
   literalt convert(const exprt &expr) override;
   void set_frozen(literalt) override;
   void set_all_frozen() override;
-  bool is_in_conflict(literalt l) const override;
   void set_to(const exprt &expr, bool value) override;
   exprt get(const exprt &expr) const override;
   std::string decision_procedure_text() const override