Added timout functionality to SAT solver

4 files changed, 56 insertions, 1 deletions

diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc
index c34ad7480..56f04fefd 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();
diff --git a/libs/ezsat/ezminisat.h b/libs/ezsat/ezminisat.h
index 4171985b6..2919aa2e3 100644
--- a/libs/ezsat/ezminisat.h
+++ b/libs/ezsat/ezminisat.h
@@ -21,6 +21,7 @@
 #define EZMINISAT_H
 
 #include "ezsat.h"
+#include <time.h>
 
 // minisat is using limit macros and format macros in their headers that
 // can be the source of some troubles when used from c++11. thefore we
@@ -36,6 +37,10 @@ private:
 	std::vector<int> minisatVars;
 	bool foundContradiction;
 
+	static ezMiniSAT *alarmHandlerThis;
+	static clock_t alarmHandlerTimeout;
+	static void alarmHandler(int);
+
 public:
 	ezMiniSAT();
 	virtual ~ezMiniSAT();
diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc
index e37031314..00918f62f 100644
--- a/libs/ezsat/ezsat.cc
+++ b/libs/ezsat/ezsat.cc
@@ -38,6 +38,9 @@ ezSAT::ezSAT()
 	cnfConsumed = false;
 	cnfVariableCount = 0;
 	cnfClausesCount = 0;
+
+	solverTimeout = 0;
+	solverTimoutStatus = false;
 }
 
 ezSAT::~ezSAT()
diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h
index 2674d83df..2d0307d51 100644
--- a/libs/ezsat/ezsat.h
+++ b/libs/ezsat/ezsat.h
@@ -69,6 +69,9 @@ private:
 	int bind_cnf_or(const std::vector<int> &args);
 
 public:
+	int solverTimeout;
+	bool solverTimoutStatus;
+
 	ezSAT();
 	virtual ~ezSAT();
 
@@ -130,6 +133,14 @@ public:
 		return solver(modelExpressions, modelValues, assumptions);
 	}
 
+	void setSolverTimeout(int newTimeoutSeconds) {
+		solverTimeout = newTimeoutSeconds;
+	}
+
+	bool getSolverTimoutStatus() {
+		return solverTimoutStatus;
+	}
+
 	// manage CNF (usually only accessed by SAT solvers)
 
 	virtual void clear();