From 8fbb5b62400edf82f6719eda90a75730d467db83 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 20 Jun 2013 12:49:10 +0200
Subject: Added timout functionality to SAT solver

---
 libs/ezsat/ezminisat.cc | 38 +++++++++++++++++++++++++++++++++++++-
 1 file changed, 37 insertions(+), 1 deletion(-)

(limited to 'libs/ezsat/ezminisat.cc')

diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc
index c34ad748..56f04fef 100644
--- a/libs/ezsat/ezminisat.cc
+++ b/libs/ezsat/ezminisat.cc
@@ -23,6 +23,7 @@
 
 #include <limits.h>
 #include <stdint.h>
+#include <signal.h>
 #include <cinttypes>
 
 #include "minisat/core/Solver.h"
@@ -50,8 +51,22 @@ void ezMiniSAT::clear()
 	ezSAT::clear();
 }
 
+ezMiniSAT *ezMiniSAT::alarmHandlerThis = NULL;
+clock_t ezMiniSAT::alarmHandlerTimeout = 0;
+
+void ezMiniSAT::alarmHandler(int)
+{
+	if (clock() > alarmHandlerTimeout) {
+		alarmHandlerThis->minisatSolver->interrupt();
+		alarmHandlerTimeout = 0;
+	} else
+		alarm(1);
+}
+
 bool ezMiniSAT::solver(const std::vector<int> &modelExpressions, std::vector<bool> &modelValues, const std::vector<int> &assumptions)
 {
+	solverTimoutStatus = false;
+
 	if (0) {
 contradiction:
 		delete minisatSolver;
@@ -104,7 +119,28 @@ contradiction:
 		else
 			assumps.push(Minisat::mkLit(minisatVars.at(-idx-1), true));
 
-	if (!minisatSolver->solve(assumps))
+	sighandler_t old_alarm_sighandler;
+	int old_alarm_timeout;
+
+	if (solverTimeout > 0) {
+		alarmHandlerThis = this;
+		alarmHandlerTimeout = clock() + solverTimeout*CLOCKS_PER_SEC;
+		old_alarm_timeout = alarm(0);
+		old_alarm_sighandler = signal(SIGALRM, alarmHandler);
+		alarm(1);
+	}
+
+	bool foundSolution = minisatSolver->solve(assumps);
+
+	if (solverTimeout > 0) {
+		if (alarmHandlerTimeout == 0)
+			solverTimoutStatus = true;
+		alarm(0);
+		signal(SIGALRM, old_alarm_sighandler);
+		alarm(old_alarm_timeout);
+	}
+
+	if (!foundSolution)
 		return false;
 
 	modelValues.clear();
-- 
cgit v1.2.3