diff options
| author | Clifford Wolf <clifford@clifford.at> | 2013-06-20 12:49:10 +0200 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2013-06-20 12:49:10 +0200 |
| commit | 8fbb5b62400edf82f6719eda90a75730d467db83 (patch) | |
| tree | 5f11874a9ffcb1553cca9a1de0d2a2234aa01ea5 /libs/ezsat/ezminisat.cc | |
| parent | 21e38bed98d3d6bc4ae5833f6f609ac8f12d6361 (diff) | |
Added timout functionality to SAT solver
Diffstat (limited to 'libs/ezsat/ezminisat.cc')
| -rw-r--r-- | libs/ezsat/ezminisat.cc | 38 |
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(); |