# Calculating Solutions of PA Formulas

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.