Merge pull request #1004 from smowton/smowton/feature/time_limit_minisat

Add simple time limiting to prop_conv and propt

Author: smowton

src/solvers/prop/prop.h

@@ -108,6 +108,12 @@ class propt:public messaget, public prop_assignmentt
   // an incremental solver may remove any variables that aren't frozen
   virtual void set_frozen(literalt a) { }
 
+  // Resource limits:
+  virtual void set_time_limit_seconds(uint32_t lim)
+  {
+    warning() << "CPU limit ignored (not implemented)" << eom;
+  }
+
 protected:
   // to avoid a temporary for lcnf(...)
   bvt lcnf_bv;

src/solvers/prop/prop_conv.h

@@ -55,6 +55,9 @@ class prop_convt:public decision_proceduret
   // returns true if an assumption is in the final conflict
   virtual bool is_in_conflict(literalt l) const;
   virtual bool has_is_in_conflict() const { return false; }
+
+  // Resource limits:
+  virtual void set_time_limit_seconds(uint32_t) {}
 };
 
 //
@@ -115,6 +118,11 @@ class prop_conv_solvert:public prop_convt
   const cachet &get_cache() const { return cache; }
   const symbolst &get_symbols() const { return symbols; }
 
+  void set_time_limit_seconds(uint32_t lim) override
+  {
+    prop.set_time_limit_seconds(lim);
+  }
+
 protected:
   virtual void post_process();
 

src/solvers/sat/satcheck_minisat2.cpp

@@ -11,6 +11,9 @@ Author: Daniel Kroening, [email protected]
 #include <inttypes.h>
 #endif
 
+#include <signal.h>
+#include <unistd.h>
+
 #include <cassert>
 #include <stack>
 
@@ -112,6 +115,13 @@ void satcheck_minisat2_baset<T>::lcnf(const bvt &bv)
   clause_counter++;
 }
 
+static Minisat::Solver *solver_to_interrupt=nullptr;
+
+static void interrupt_solver(int signum)
+{
+  solver_to_interrupt->interrupt();
+}
+
 template<typename T>
 propt::resultt satcheck_minisat2_baset<T>::prop_solve()
 {
@@ -151,19 +161,48 @@ propt::resultt satcheck_minisat2_baset<T>::prop_solve()
         Minisat::vec<Minisat::Lit> solver_assumptions;
         convert(assumptions, solver_assumptions);
 
-        if(solver->solve(solver_assumptions))
+        void (*old_handler)(int)=SIG_ERR;
+
+        if(time_limit_seconds!=0)
+        {
+          solver_to_interrupt=solver;
+          old_handler=signal(SIGALRM, interrupt_solver);
+          if(old_handler==SIG_ERR)
+            warning() << "Failed to set solver time limit" << eom;
+          else
+            alarm(time_limit_seconds);
+        }
+
+        using Minisat::lbool;
+        lbool solver_result=solver->solveLimited(solver_assumptions);
+
+        if(old_handler!=SIG_ERR)
+        {
+          alarm(0);
+          signal(SIGALRM, old_handler);
+          solver_to_interrupt=solver;
+        }
+
+        if(solver_result==l_True)
         {
           messaget::status() <<
             "SAT checker: instance is SATISFIABLE" << eom;
           assert(solver->model.size()!=0);
           status=statust::SAT;
           return resultt::P_SATISFIABLE;
         }
-        else
+        else if(solver_result==l_False)
         {
           messaget::status() <<
             "SAT checker: instance is UNSATISFIABLE" << eom;
         }
+        else
+        {
+          messaget::status() <<
+            "SAT checker: timed out or other error" << eom;
+          status=statust::ERROR;
+          return resultt::P_ERROR;
+        }
       }
     }
 
@@ -195,7 +234,7 @@ void satcheck_minisat2_baset<T>::set_assignment(literalt a, bool value)
 
 template<typename T>
 satcheck_minisat2_baset<T>::satcheck_minisat2_baset(T *_solver):
-  solver(_solver)
+  solver(_solver), time_limit_seconds(0)
 {
 }
 

src/solvers/sat/satcheck_minisat2.h

@@ -46,8 +46,14 @@ class satcheck_minisat2_baset:public cnf_solvert
   virtual bool has_set_assumptions() const final { return true; }
   virtual bool has_is_in_conflict() const final { return true; }
 
+  void set_time_limit_seconds(uint32_t lim) override
+  {
+    time_limit_seconds=lim;
+  }
+
 protected:
   T *solver;
+  uint32_t time_limit_seconds;
 
   void add_variables();
   bvt assumptions;