summaryrefslogtreecommitdiff
path: root/libs/ezsat/ezminisat.cc
diff options
context:
space:
mode:
Diffstat (limited to 'libs/ezsat/ezminisat.cc')
-rw-r--r--libs/ezsat/ezminisat.cc38
1 files changed, 37 insertions, 1 deletions
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();