diff --git a/lib/kodkod.jar b/lib/kodkod.jar
index bc62d19b83389d58c5efb96c760b5333577be78f..80a4756f6d00f8bdfcb4da62936b1ed84772303d 100644
Binary files a/lib/kodkod.jar and b/lib/kodkod.jar differ
diff --git a/src/de/stups/probkodkod/KodkodAnalysis.java b/src/de/stups/probkodkod/KodkodAnalysis.java
index ae124657026e13a7a1f87fbfc919441df39443da..11f3793293e18e8ed6b5bebb4b603600c5ef7d6d 100644
--- a/src/de/stups/probkodkod/KodkodAnalysis.java
+++ b/src/de/stups/probkodkod/KodkodAnalysis.java
@@ -89,7 +89,6 @@ import de.stups.probkodkod.parser.node.APrjInnerexpression;
import de.stups.probkodkod.parser.node.AProblem;
import de.stups.probkodkod.parser.node.AProductExprMultop;
import de.stups.probkodkod.parser.node.AQuantInnerformula;
-import de.stups.probkodkod.parser.node.AReflclsExprUnop;
import de.stups.probkodkod.parser.node.ARelInnerformula;
import de.stups.probkodkod.parser.node.ARelation;
import de.stups.probkodkod.parser.node.ARelrefInnerexpression;
@@ -178,8 +177,6 @@ public class KodkodAnalysis extends DepthFirstAdapter {
BINEXPROPS.put(AOverwriteExprBinop.class.getName(),
ExprOperator.OVERRIDE);
UNEXPROPS.put(AClosureExprUnop.class.getName(), ExprOperator.CLOSURE);
- UNEXPROPS.put(AReflclsExprUnop.class.getName(),
- ExprOperator.REFLEXIVE_CLOSURE);
UNEXPROPS.put(ATransposeExprUnop.class.getName(),
ExprOperator.TRANSPOSE);
MULTIPLICITIES
diff --git a/src/de/stups/probkodkod/Request.java b/src/de/stups/probkodkod/Request.java
index 32f4bca4dedc95581790980cf9b81f6a0d9d9802..27a666c160a81b72f4c32df31d0308700d1c63c0 100644
--- a/src/de/stups/probkodkod/Request.java
+++ b/src/de/stups/probkodkod/Request.java
@@ -63,14 +63,46 @@ public final class Request {
* have been send to the stream
*/
public boolean writeNextSolutions(final IPrologTermOutput pto, final int max) {
- pto.openTerm("solutions");
- pto.openList();
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++) {
- Instance instance = nextInstance();
+ 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.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;
+ }
+
+ private void printInstances(Instance[] solutions, IPrologTermOutput pto) {
+ pto.openList();
+ for (final Instance instance : solutions) {
+ if (instance != null) {
pto.openList();
for (int i = 0; i < variables.length; i++) {
final RelationInfo relinfo = variables[i];
@@ -94,13 +126,6 @@ public final class Request {
}
}
pto.closeList();
- pto.printAtom(solutionsPresent ? "more" : "all");
- if (logger.isLoggable(Level.FINE)) {
- logger.fine("wrote " + num + " solutions");
- }
- pto.closeTerm();
- pto.fullstop();
- return solutionsPresent;
}
private void writeTupleSet(final IPrologTermOutput pto,
diff --git a/src/problem.grammar b/src/problem.grammar
index a0fd3ee5f1a6e9b8331330ad09a005ee49a3974d..d32d2959a6867009fcc49249f4752162ac42597b 100644
--- a/src/problem.grammar
+++ b/src/problem.grammar
@@ -49,7 +49,6 @@ Tokens
keyword_overwrite = 'overwrite';
keyword_transpose = 'transpose';
keyword_closure = 'closure';
- keyword_reflexive_closure = 'reflexive_closure';
keyword_comprehension = 'comp';
keyword_empty = 'empty';
keyword_iden = 'iden';
@@ -186,8 +185,7 @@ Productions
expr_unop =
{transpose} keyword_transpose
- | {closure} keyword_closure
- | {reflcls} keyword_reflexive_closure;
+ | {closure} keyword_closure;
intexpression = parenl innerintexpression parenr;
innerintexpression =
diff --git a/test/de/stups/probkodkod/InteractionTestBase.java b/test/de/stups/probkodkod/InteractionTestBase.java
index 1d7ec5ed006753d0f70dc9f7ba51f7716e10a604..561ef428dfe15709c4f1decc25101ed7bd23b251 100644
--- a/test/de/stups/probkodkod/InteractionTestBase.java
+++ b/test/de/stups/probkodkod/InteractionTestBase.java
@@ -116,7 +116,7 @@ public class InteractionTestBase {
throws IOException, ParserException, LexerException {
CompoundPrologTerm solsterm = (CompoundPrologTerm) answer;
assertEquals("solutions", solsterm.getFunctor());
- assertEquals(2, solsterm.getArity());
+ assertEquals(3, solsterm.getArity());
ListPrologTerm listterm = (ListPrologTerm) solsterm.getArgument(1);
for (PrologTerm bindings : listterm) {
ListPrologTerm solterm = (ListPrologTerm) bindings;
@@ -129,6 +129,8 @@ public class InteractionTestBase {
} else {
assertEquals(new CompoundPrologTerm("all"), moreTerm);
}
+ ListPrologTerm durterm = (ListPrologTerm) solsterm.getArgument(3);
+ assertEquals("number of durations", listterm.size(), durterm.size());
}
private SortedMap<String, Result> extractSolution(
diff --git a/test/de/stups/probkodkod/KodkodTest.java b/test/de/stups/probkodkod/KodkodTest.java
index 95d2521f2f4f4db9c87f6ac6d31188a36df7129c..87b12f0f58cce3a7af49287d4c454c0007895a16 100644
--- a/test/de/stups/probkodkod/KodkodTest.java
+++ b/test/de/stups/probkodkod/KodkodTest.java
@@ -5,6 +5,7 @@ import static org.junit.Assert.assertTrue;
import java.io.IOException;
import java.util.LinkedList;
import java.util.List;
+import java.util.Map;
import java.util.SortedMap;
import org.junit.Test;
@@ -175,4 +176,29 @@ public class KodkodTest extends InteractionTestBase {
checkSolutions(b.toCollection(), sol);
}
+ @Test
+ public void testSendMoreMoney() throws ParserException, LexerException,
+ IOException {
+ final String problem = load("sendmoremoney.kodkod");
+ sendMessage(problem + ".");
+ sendMessage("request sendmoremoney 100 pos ().");
+ List<SortedMap<String, Result>> sol = new LinkedList<SortedMap<String, Result>>();
+ getSolutions(false, sol);
+
+ ResultSetBuilder b = new ResultSetBuilder();
+ b.single("s", t(9));
+ b.single("e", t(5));
+ b.single("n", t(6));
+ b.single("d", t(7));
+ b.single("m", t(1));
+ b.single("o", t(0));
+ b.single("r", t(8));
+ b.single("y", t(2));
+ b.store();
+ checkSolutions(b.toCollection(), sol);
+
+ for (final Map<String, Result> entry : sol) {
+
+ }
+ }
}
diff --git a/test/de/stups/probkodkod/problems/sendmoremoney.kodkod b/test/de/stups/probkodkod/problems/sendmoremoney.kodkod
new file mode 100644
index 0000000000000000000000000000000000000000..775f4fdc7b9eb1183883ac16f62ddecbc9e41c47
--- /dev/null
+++ b/test/de/stups/probkodkod/problems/sendmoremoney.kodkod
@@ -0,0 +1,63 @@
+problem sendmoremoney ((inttype(p2i 0 199980)))
+
+( (s singleton subset p2i)
+ (e singleton subset p2i)
+ (n singleton subset p2i)
+ (d singleton subset p2i)
+ (m singleton subset p2i)
+ (o singleton subset p2i)
+ (r singleton subset p2i)
+ (y singleton subset p2i))
+
+(and (gt(expr2int(relref s))(0))
+ (gt(expr2int(relref m))(0))
+ (not(equals(relref s)(relref e)))
+ (not(equals(relref s)(relref n)))
+ (not(equals(relref s)(relref d)))
+ (not(equals(relref s)(relref m)))
+ (not(equals(relref s)(relref o)))
+ (not(equals(relref s)(relref r)))
+ (not(equals(relref s)(relref y)))
+ (not(equals(relref e)(relref n)))
+ (not(equals(relref e)(relref d)))
+ (not(equals(relref e)(relref m)))
+ (not(equals(relref e)(relref o)))
+ (not(equals(relref e)(relref r)))
+ (not(equals(relref e)(relref y)))
+ (not(equals(relref n)(relref d)))
+ (not(equals(relref n)(relref m)))
+ (not(equals(relref n)(relref o)))
+ (not(equals(relref n)(relref r)))
+ (not(equals(relref n)(relref y)))
+ (not(equals(relref d)(relref m)))
+ (not(equals(relref d)(relref o)))
+ (not(equals(relref d)(relref r)))
+ (not(equals(relref d)(relref y)))
+ (not(equals(relref m)(relref o)))
+ (not(equals(relref m)(relref r)))
+ (not(equals(relref m)(relref y)))
+ (not(equals(relref o)(relref r)))
+ (not(equals(relref o)(relref y)))
+ (not(equals(relref r)(relref y)))
+ (lte(1)(expr2int(relref s))) (lte(expr2int(relref s))(9))
+ (lte(0)(expr2int(relref e))) (lte(expr2int(relref e))(9))
+ (lte(0)(expr2int(relref n))) (lte(expr2int(relref n))(9))
+ (lte(0)(expr2int(relref d))) (lte(expr2int(relref d))(9))
+ (lte(1)(expr2int(relref m))) (lte(expr2int(relref m))(9))
+ (lte(0)(expr2int(relref o))) (lte(expr2int(relref o))(9))
+ (lte(0)(expr2int(relref r))) (lte(expr2int(relref r))(9))
+ (lte(0)(expr2int(relref y))) (lte(expr2int(relref y))(9))
+ (equals(add(add(add(add(add(add(add(mul(expr2int(relref s))(1000))
+ (mul(expr2int(relref e))(100)))
+ (mul(expr2int(relref n))(10)))
+ (expr2int(relref d)))
+ (mul(expr2int(relref m))(1000)))
+ (mul(expr2int(relref o))(100)))
+ (mul(expr2int(relref r))(10)))
+ (expr2int(relref e)))
+ (add(add(add(add(mul(expr2int(relref m))(10000))
+ (mul(expr2int(relref o))(1000)))
+ (mul(expr2int(relref n))(100)))
+ (mul(expr2int(relref e))(10)))
+ (expr2int(relref y)))))
+