From 0ee493340580e61b045fe7a1d0f228607fe1379f Mon Sep 17 00:00:00 2001
From: Chris Smowton <chris@smowton.net>
Date: Thu, 8 Jun 2017 15:42:43 +0100
Subject: [PATCH] Add simple time limiting to prop_conv and propt

Currently only minisat2 supports this.
---
 src/solvers/prop/prop.h               |  6 ++++
 src/solvers/prop/prop_conv.h          |  8 +++++
 src/solvers/sat/satcheck_minisat2.cpp | 45 +++++++++++++++++++++++++--
 src/solvers/sat/satcheck_minisat2.h   |  6 ++++
 4 files changed, 62 insertions(+), 3 deletions(-)

diff --git a/src/solvers/prop/prop.h b/src/solvers/prop/prop.h
index e48674d5c57..a6ee4371f2a 100644
--- a/src/solvers/prop/prop.h
+++ b/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;
diff --git a/src/solvers/prop/prop_conv.h b/src/solvers/prop/prop_conv.h
index 9d59fb06cf5..816b7481a0e 100644
--- a/src/solvers/prop/prop_conv.h
+++ b/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();
 
diff --git a/src/solvers/sat/satcheck_minisat2.cpp b/src/solvers/sat/satcheck_minisat2.cpp
index cab952930f6..6c8a6b45f3a 100644
--- a/src/solvers/sat/satcheck_minisat2.cpp
+++ b/src/solvers/sat/satcheck_minisat2.cpp
@@ -11,6 +11,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #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,7 +161,29 @@ 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;
@@ -159,11 +191,18 @@ propt::resultt satcheck_minisat2_baset<T>::prop_solve()
           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)
 {
 }
 
diff --git a/src/solvers/sat/satcheck_minisat2.h b/src/solvers/sat/satcheck_minisat2.h
index 22026e27d85..cda5ab21bac 100644
--- a/src/solvers/sat/satcheck_minisat2.h
+++ b/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;