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

@@ -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