From 8991e729a115d21d4398a9e746a5ea3d61650734 Mon Sep 17 00:00:00 2001 From: Sebastian Krings <sebastian@krin.gs> Date: Mon, 17 Aug 2015 14:39:38 +0200 Subject: [PATCH] catch timeout and report it to prolog --- .../java/de/stups/probkodkod/Request.java | 69 +++++++++++-------- 1 file changed, 39 insertions(+), 30 deletions(-) diff --git a/src/main/java/de/stups/probkodkod/Request.java b/src/main/java/de/stups/probkodkod/Request.java index 27a666c..0227678 100644 --- a/src/main/java/de/stups/probkodkod/Request.java +++ b/src/main/java/de/stups/probkodkod/Request.java @@ -63,40 +63,49 @@ public final class Request { * have been send to the stream */ public boolean writeNextSolutions(final IPrologTermOutput pto, final int max) { - boolean solutionsPresent = true; - int num; - int size = 0; - long durations[] = new long[max]; - Instance[] solutions = new Instance[max]; - for (num = 0; solutionsPresent & num < max; num++) { - final long start = System.currentTimeMillis(); - final Instance instance = nextInstance(); - durations[num] = System.currentTimeMillis() - start; - solutionsPresent = instance != null; - if (solutionsPresent) { - solutions[num] = instance; - size++; + try { + boolean solutionsPresent = true; + int num; + int size = 0; + long durations[] = new long[max]; + Instance[] solutions = new Instance[max]; + for (num = 0; solutionsPresent & num < max; num++) { + final long start = System.currentTimeMillis(); + final Instance instance = nextInstance(); + durations[num] = System.currentTimeMillis() - start; + solutionsPresent = instance != null; + if (solutionsPresent) { + solutions[num] = instance; + size++; + } } - } - pto.openTerm("solutions"); - printInstances(solutions, pto); + pto.openTerm("solutions"); + printInstances(solutions, pto); - pto.printAtom(solutionsPresent ? "more" : "all"); - pto.openList(); - long duration = 0; - for (int i = 0; i < size; i++) { - pto.printNumber(durations[i]); - duration += durations[i]; - } - pto.closeList(); - pto.closeTerm(); - pto.fullstop(); - if (logger.isLoggable(Level.FINE)) { - logger.fine("wrote " + num + " solutions, computed in " + duration - + "ms"); + pto.printAtom(solutionsPresent ? "more" : "all"); + pto.openList(); + long duration = 0; + for (int i = 0; i < size; i++) { + pto.printNumber(durations[i]); + duration += durations[i]; + } + pto.closeList(); + pto.closeTerm(); + pto.fullstop(); + if (logger.isLoggable(Level.FINE)) { + logger.fine("wrote " + num + " solutions, computed in " + + duration + "ms"); + } + return solutionsPresent; + } catch (RuntimeException ex) { + // timeout of the solver is wrapped in a runtime exception + if ("timed out".equals(ex.getMessage())) { + pto.printAtom("sat_timeout"); + return true; + } + throw (ex); } - return solutionsPresent; } private void printInstances(Instance[] solutions, IPrologTermOutput pto) { -- GitLab