Merge pull request #1750 from pkesseli/feature/sat-interrupt

Expose MiniSAT's `interrupt()`

Author: tautschnig

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; }