- added test case "Send More Money"

- added runtime information in answers
- new Kodkod version 1.5

git-svn-id: https://cobra.cs.uni-duesseldorf.de/prob/trunk/experimental/plagge/probkodkod@10471 7aec93f6-bc54-0410-ac70-7d7c9efa889a

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

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,

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 =

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(

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) {
+
+		}
+	}
 }

test/de/stups/probkodkod/problems/sendmoremoney.kodkod

+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)))))
+