# 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.