summaryrefslogtreecommitdiff
path: root/libs
diff options
context:
space:
mode:
Diffstat (limited to 'libs')
-rw-r--r--libs/ezsat/ezminisat.cc38
-rw-r--r--libs/ezsat/ezminisat.h5
-rw-r--r--libs/ezsat/ezsat.cc3
-rw-r--r--libs/ezsat/ezsat.h11
4 files changed, 56 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();
diff --git a/libs/ezsat/ezminisat.h b/libs/ezsat/ezminisat.h
index 4171985b..2919aa2e 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 e3703131..00918f62 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 2674d83d..2d0307d5 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();