From 06c6477c0144025d79b32c2472ff81ded335c1cb Mon Sep 17 00:00:00 2001
From: Daniel Plagge <plagge@cs.uni-duesseldorf.de>
Date: Thu, 17 Mar 2011 15:38:00 +0000
Subject: [PATCH] Kodkod bugfix: exception when returning a 0 for a POW2
 integer, added test case

git-svn-id: https://cobra.cs.uni-duesseldorf.de/prob/trunk/experimental/plagge/probkodkod@7396 7aec93f6-bc54-0410-ac70-7d7c9efa889a
---
 src/de/stups/probkodkod/Request.java       |  3 ++-
 test/de/stups/probkodkod/KodkodTest.java   | 30 ++++++++++++++++------
 test/de/stups/probkodkod/returnzero.kodkod |  6 +++++
 3 files changed, 30 insertions(+), 9 deletions(-)
 create mode 100644 test/de/stups/probkodkod/returnzero.kodkod

diff --git a/src/de/stups/probkodkod/Request.java b/src/de/stups/probkodkod/Request.java
index 53ea99c..32f4bca 100644
--- a/src/de/stups/probkodkod/Request.java
+++ b/src/de/stups/probkodkod/Request.java
@@ -80,7 +80,8 @@ public final class Request {
 					pto.openTerm(tupleType.isSingleton() ? "b" : "s");
 					pto.printAtom(relinfo.getId());
 					if (tupleType.isSingleton()) {
-						final Tuple tuple = tupleSet.iterator().next();
+						final Tuple tuple = tupleSet.isEmpty() ? null
+								: tupleSet.iterator().next();
 						writeTuple(pto, tupleType, tupleSet, tuple);
 					} else {
 						pto.openList();
diff --git a/test/de/stups/probkodkod/KodkodTest.java b/test/de/stups/probkodkod/KodkodTest.java
index 59048fc..1fa5a35 100644
--- a/test/de/stups/probkodkod/KodkodTest.java
+++ b/test/de/stups/probkodkod/KodkodTest.java
@@ -15,7 +15,7 @@ import de.stups.probkodkod.test.Result;
 import de.stups.probkodkod.test.ResultSetBuilder;
 
 public class KodkodTest extends InteractionTestBase {
-	// @Test
+	@Test
 	public void testLoop() throws ParserException, LexerException, IOException,
 			InterruptedException {
 		String problem = load("loop.kodkod");
@@ -68,7 +68,7 @@ public class KodkodTest extends InteractionTestBase {
 		checkSolutions(createExpResLoop(), loop2);
 	}
 
-	// @Test
+	@Test
 	public void testIntegers() throws IOException, ParserException,
 			LexerException, InterruptedException {
 		ResultSetBuilder b = new ResultSetBuilder();
@@ -76,7 +76,7 @@ public class KodkodTest extends InteractionTestBase {
 		testAll("integers", b.toCollection());
 	}
 
-	// @Test
+	@Test
 	public void testProjection() throws IOException, ParserException,
 			LexerException, InterruptedException {
 		ResultSetBuilder b = new ResultSetBuilder();
@@ -84,7 +84,7 @@ public class KodkodTest extends InteractionTestBase {
 		testAll("projection", b.toCollection());
 	}
 
-	// @Test
+	@Test
 	public void testFunctions() throws IOException, ParserException,
 			LexerException, InterruptedException {
 		ResultSetBuilder b = new ResultSetBuilder();
@@ -93,7 +93,7 @@ public class KodkodTest extends InteractionTestBase {
 		testAll("functions", b.toCollection());
 	}
 
-	// @Test
+	@Test
 	public void testIntegerCasts() throws IOException, ParserException,
 			LexerException, InterruptedException {
 		ResultSetBuilder b = new ResultSetBuilder();
@@ -101,7 +101,7 @@ public class KodkodTest extends InteractionTestBase {
 		testAll("integercast", b.toCollection());
 	}
 
-	// @Test
+	@Test
 	public void testIntegerVariable() throws IOException, ParserException,
 			LexerException, InterruptedException {
 		ResultSetBuilder b = new ResultSetBuilder();
@@ -109,7 +109,7 @@ public class KodkodTest extends InteractionTestBase {
 		testAll("intvar", b.toCollection());
 	}
 
-	// @Test
+	@Test
 	public void testIntegerRange() throws IOException, ParserException,
 			LexerException, InterruptedException {
 		ResultSetBuilder b = new ResultSetBuilder();
@@ -126,7 +126,7 @@ public class KodkodTest extends InteractionTestBase {
 		testAll("negative", b.toCollection());
 	}
 
-	// @Test
+	@Test
 	public void testEmptySetInRequest() throws IOException, ParserException,
 			LexerException {
 		final String problem = load("simpletwovars.kodkod");
@@ -145,4 +145,18 @@ public class KodkodTest extends InteractionTestBase {
 
 		checkSolutions(b.toCollection(), sol);
 	}
+
+	@Test
+	public void testBug1() throws ParserException, LexerException, IOException {
+		final String problem = load("returnzero.kodkod");
+		sendMessage(problem + ".");
+
+		sendMessage("request returnzero 10 pos ().");
+		List<SortedMap<String, Result>> sol = new LinkedList<SortedMap<String, Result>>();
+		getSolutions(false, sol);
+
+		ResultSetBuilder b = new ResultSetBuilder();
+		b.single("x", t(0)).store();
+		checkSolutions(b.toCollection(), sol);
+	}
 }
diff --git a/test/de/stups/probkodkod/returnzero.kodkod b/test/de/stups/probkodkod/returnzero.kodkod
new file mode 100644
index 0000000..8437c86
--- /dev/null
+++ b/test/de/stups/probkodkod/returnzero.kodkod
@@ -0,0 +1,6 @@
+problem returnzero 
+  ( (inttype(p2i 0 0)) )
+  
+  ( (x singleton subset p2i) )
+  
+  (equals(expr2int(relref x))(0))
-- 
GitLab