From b1029dccbf6689ab8dd166ad6255a75d92ec4988 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Fri, 14 Dec 2012 20:16:52 +0100
Subject: [PATCH] Complete the previously added justify testcase
The testcase is now complete in the sense that the specification for
the justify function explicitly describe the final output list of columns,
while the previous one could be implicitly computed from the synthesized
parameters. It also features a simpler synthesis problem, that should be
the first target to solver.
---
testcases/synthesis/Justify.scala | 33 ++++++++++++++++++++++++-------
1 file changed, 26 insertions(+), 7 deletions(-)
diff --git a/testcases/synthesis/Justify.scala b/testcases/synthesis/Justify.scala
index fcb927be9..2c3ff9a32 100644
--- a/testcases/synthesis/Justify.scala
+++ b/testcases/synthesis/Justify.scala
@@ -40,20 +40,39 @@ object Justify {
* justifying lines by
* inserting extra blanks is
* one task of a text editor.
-
- *
- * This version is a simpler one, in which we are just trying to determine parameters that can then
- * be mecanically used to build the justified text. Also we do not distinguish on even/odd line number.
- *
*/
- def justify(n: Int, z: Int, s: Int, words: IntList): (Int, Int, Int) = {
+ def justify(n: Int, z: Int, s: Int, words: IntList): IntList = {
require(n >= 0 && s >= 0 && z >= 1)
//here p and q are as defined above. t is used to find the index of the word where
//we switch from p spaces to q spaces.
val (res, p, q, t) = choose((justifiedWords: IntList, p: Int, q: Int, t: Int) =>
p >= 0 && q >= 0 && p == q+1 && t >= 1 && t <= n &&
- p*(t - 1) + q*(n-t) == s //this constraint is probably going to be an issue since it is non linear
+ p*(t-1) + q*(n-t) == s && //this constraint is probably going to be an issue since it is non linear
+ ((z % 2 == 1 && q == p + 1) || (z % 2 == 0 && p == q + 1)) &&
+ justifiedWords == addSpaces(words, p, q, t, n, 0) //this is likely to be problematic as well
+ )
+
+ res
+ }
+
+ def addSpaces(words: IntList, p: Int, q: Int, t: Int, n: Int, i: Int): IntList = words match {
+ case IntNil() => IntNil()
+ case IntCons(head, tail) =>
+ if(i <= t) IntCons(head + p*(i-1), addSpaces(tail, p, q, t, n, i+1))
+ else if(i > t && i <= n) IntCons(head + p*(t-1) + q*(i-t), addSpaces(tail, p, q, t, n, i+1))
+ else IntNil() //this should never happen
+ }
+
+ /*
+ * This version is a simpler one, in which we are just trying to determine parameters that can then
+ * be mecanically used to build the justified text. Also we do not distinguish on even/odd line number.
+ */
+ def simpleJustify(n: Int, z: Int, s: Int, words: IntList): (Int, Int, Int) = {
+ require(n >= 0 && s >= 0 && z >= 1)
+
+ val (p, q, t) = choose((p: Int, q: Int, t: Int) =>
+ p >= 0 && q >= 0 && p == q+1 && t >= 1 && t <= n && p*(t - 1) + q*(n-t) == s
)
//actually, we could simply use the parameter to program the ocnstruction of the List, rather than explicitly synthesizing it
--
GitLab