From f0917eb5b0b79adec99f223989fcfcda3ce2054d Mon Sep 17 00:00:00 2001
From: Sebastian Krings <sebastian@krin.gs>
Date: Thu, 6 Oct 2016 11:20:05 +0200
Subject: [PATCH] throw exception if second solution of non-incremental solver
is requested
---
.../de/stups/probkodkod/ImmutableProblem.java | 2 +-
.../NonIncrementalSolverSolutionIterator.java | 29 ++++++++++
.../java/de/stups/probkodkod/Request.java | 56 +++++++++----------
3 files changed, 56 insertions(+), 31 deletions(-)
create mode 100644 src/main/java/de/stups/probkodkod/NonIncrementalSolverSolutionIterator.java
diff --git a/src/main/java/de/stups/probkodkod/ImmutableProblem.java b/src/main/java/de/stups/probkodkod/ImmutableProblem.java
index fc27cd8..6668dc0 100644
--- a/src/main/java/de/stups/probkodkod/ImmutableProblem.java
+++ b/src/main/java/de/stups/probkodkod/ImmutableProblem.java
@@ -198,7 +198,7 @@ public final class ImmutableProblem {
logger.info(bounds.toString());
}
- return new Request(variables, Arrays.asList(sol).iterator());
+ return new Request(variables, new NonIncrementalSolverSolutionIterator(sol));
}
}
diff --git a/src/main/java/de/stups/probkodkod/NonIncrementalSolverSolutionIterator.java b/src/main/java/de/stups/probkodkod/NonIncrementalSolverSolutionIterator.java
new file mode 100644
index 0000000..d5b606c
--- /dev/null
+++ b/src/main/java/de/stups/probkodkod/NonIncrementalSolverSolutionIterator.java
@@ -0,0 +1,29 @@
+package de.stups.probkodkod;
+
+import java.util.Iterator;
+
+import kodkod.engine.Solution;
+
+public class NonIncrementalSolverSolutionIterator implements Iterator<Solution> {
+
+ private Solution sol;
+ private boolean returned = false;
+
+ public NonIncrementalSolverSolutionIterator(Solution sol) {
+ this.sol = sol;
+ }
+
+ @Override
+ public boolean hasNext() {
+ return true;
+ }
+
+ @Override
+ public Solution next() {
+ if (!returned) {
+ return sol;
+ }
+ throw new RuntimeException("second solution of non-incremental solver requested");
+ }
+
+}
diff --git a/src/main/java/de/stups/probkodkod/Request.java b/src/main/java/de/stups/probkodkod/Request.java
index beb0012..6a2d17f 100644
--- a/src/main/java/de/stups/probkodkod/Request.java
+++ b/src/main/java/de/stups/probkodkod/Request.java
@@ -7,14 +7,13 @@ import java.util.Map;
import java.util.logging.Level;
import java.util.logging.Logger;
+import de.prob.prolog.output.IPrologTermOutput;
+import de.stups.probkodkod.types.TupleType;
import kodkod.ast.Relation;
import kodkod.engine.Solution;
-import kodkod.engine.Statistics;
import kodkod.instance.Instance;
import kodkod.instance.Tuple;
import kodkod.instance.TupleSet;
-import de.prob.prolog.output.IPrologTermOutput;
-import de.stups.probkodkod.types.TupleType;
/**
* A request stores the information about a ongoing query in the current
@@ -29,13 +28,11 @@ public final class Request {
private final RelationInfo[] variables;
private final Iterator<Solution> iterator;
- public Request(final RelationInfo[] variables,
- final Iterator<Solution> iterator) {
+ public Request(final RelationInfo[] variables, final Iterator<Solution> iterator) {
this.variables = variables;
this.iterator = iterator;
if (logger.isLoggable(Level.FINE)) {
- logger.fine("request created: return variables are: "
- + Arrays.asList(variables));
+ logger.fine("request created: return variables are: " + Arrays.asList(variables));
}
}
@@ -95,8 +92,7 @@ public final class Request {
pto.closeTerm();
pto.fullstop();
if (logger.isLoggable(Level.FINE)) {
- logger.fine("wrote " + num + " solutions, computed in "
- + duration + "ms");
+ logger.fine("wrote " + num + " solutions, computed in " + duration + "ms");
}
return solutionsPresent;
} catch (RuntimeException ex) {
@@ -106,6 +102,11 @@ public final class Request {
pto.fullstop();
return true;
}
+ if ("second solution of non-incremental solver requested".equals(ex.getMessage())) {
+ pto.printAtom("sat_non_incremental");
+ pto.fullstop();
+ return true;
+ }
throw (ex);
}
}
@@ -117,14 +118,12 @@ public final class Request {
pto.openList();
for (int i = 0; i < variables.length; i++) {
final RelationInfo relinfo = variables[i];
- final TupleSet tupleSet = instance.tuples(relinfo
- .getRelation());
+ final TupleSet tupleSet = instance.tuples(relinfo.getRelation());
final TupleType tupleType = relinfo.getTupleType();
pto.openTerm(tupleType.isSingleton() ? "b" : "s");
pto.printAtom(relinfo.getId());
if (tupleType.isSingleton()) {
- final Tuple tuple = tupleSet.isEmpty() ? null
- : tupleSet.iterator().next();
+ final Tuple tuple = tupleSet.isEmpty() ? null : tupleSet.iterator().next();
writeTuple(pto, tupleType, tupleSet, tuple);
} else {
pto.openList();
@@ -139,15 +138,13 @@ public final class Request {
pto.closeList();
}
- private void writeTupleSet(final IPrologTermOutput pto,
- final TupleType tupleType, final TupleSet tupleSet) {
+ private void writeTupleSet(final IPrologTermOutput pto, final TupleType tupleType, final TupleSet tupleSet) {
for (Tuple tuple : tupleSet) {
writeTuple(pto, tupleType, tupleSet, tuple);
}
}
- private void writeTuple(final IPrologTermOutput pto,
- final TupleType tupleType, final TupleSet tupleSet,
+ private void writeTuple(final IPrologTermOutput pto, final TupleType tupleType, final TupleSet tupleSet,
final Tuple tuple) {
final int[] intTuple = tupleType.decodeTuple(tuple, tupleSet);
pto.openList();
@@ -163,20 +160,19 @@ public final class Request {
Solution solution = iterator.next();
instance = solution.instance();
if (logger.isLoggable(Level.FINE)) {
- logger.fine("CNF translated in " + solution.stats().translationTime()
- + " ms and solved in " + solution.stats().solvingTime() + "ms ("
- + solution.stats().clauses() + " clauses, "
- + solution.stats().variables() + " variables, "
- + solution.stats().primaryVariables() + " primary variables)");
+ logger.fine("CNF translated in " + solution.stats().translationTime() + " ms and solved in "
+ + solution.stats().solvingTime() + "ms (" + solution.stats().clauses() + " clauses, "
+ + solution.stats().variables() + " variables, " + solution.stats().primaryVariables()
+ + " primary variables)");
}
- /* TO DO: maybe add a preference for this: */
- /* the information is printed on the output stream and then
- read by ProB in get_solutions_from_stream in kodkod_process.pl */
- System.out.println("stats(" + solution.stats().translationTime() +
- "," + solution.stats().solvingTime() +
- "," + solution.stats().clauses() +
- "," + solution.stats().variables() +
- "," + solution.stats().primaryVariables() + "). ");
+ /* TO DO: maybe add a preference for this: */
+ /*
+ * the information is printed on the output stream and then read by
+ * ProB in get_solutions_from_stream in kodkod_process.pl
+ */
+ System.out.println("stats(" + solution.stats().translationTime() + "," + solution.stats().solvingTime()
+ + "," + solution.stats().clauses() + "," + solution.stats().variables() + ","
+ + solution.stats().primaryVariables() + "). ");
} else {
instance = null;
}
--
GitLab