Project: extend the synthesis algorithm from last time to generate solution enumerators (that are as efficient as possible).

Exercise: Suppose we have a precondition of a function and we wish to test the function for values that satisfy a precondition. We can add some bounds to the precondition and then obtain precondition formula that has finitely many solutions.

As an example, write a compact and efficient enumerator for this constraint:

10x + 6y = a && x >= 0 && y >= 0

where a is a parameter.

A Kaplan program:

for ((p,q) <- ((x,y) => 10x + 6y = a && x >= 0 && y >= 0).findAll)
  println(p + ", " + q)

It would be good to compile it to something like this code, which is guaranteed top produce a constant amount of work to find each next solution. The question is also whether such compilation is always possible.

  if(a % 2 == 0) {
    val ap = a/2
    val lower = ...
    val upper = ...
    var k = lower
    while (k <= upper)
      val p = -5*ap + 3*k
      val q = 2*ap - 5*k
      println(p + ", " + q)
      k = k + 1
    }
  }

See also the work on UDITA for automated generation of tests the work on Regular Synthesis.