Expose MiniSAT's interrupt()

Makes MiniSAT's `interrupt()` and `clearInterrupt()` available to direct
users. This allows aborting a running SAT query, e.g. in the context of
multiple queries on different threads.

Once this feature is required with other solvers as well, it may be
useful to create a `virtual` function in `cnf_solvert` or even
`prop_convt`, but for now this feature is uniquely required for our
experiments with MiniSAT.

Author: pkesseli

src/solvers/sat/satcheck_minisat2.cpp

@@ -81,6 +81,18 @@ void satcheck_minisat2_baset<T>::set_polarity(literalt a, bool value)
   }
 }
 
+template<typename T>
+void satcheck_minisat2_baset<T>::interrupt()
+{
+  solver->interrupt();
+}
+
+template<typename T>
+void satcheck_minisat2_baset<T>::clear_interrupt()
+{
+  solver->clearInterrupt();
+}
+
 const std::string satcheck_minisat_no_simplifiert::solver_text()
 {
   return "MiniSAT 2.2.1 without simplifier";

src/solvers/sat/satcheck_minisat2.h

@@ -42,6 +42,12 @@ class satcheck_minisat2_baset:public cnf_solvert
   // extra MiniSat feature: default branching decision
   void set_polarity(literalt a, bool value);
 
+  // extra MiniSat feature: interrupt running SAT query
+  void interrupt();
+
+  // extra MiniSat feature: permit previously interrupted SAT query to continue
+  void clear_interrupt();
+
   virtual bool is_in_conflict(literalt a) const override;
   virtual bool has_set_assumptions() const final { return true; }
   virtual bool has_is_in_conflict() const final { return true; }