examples/template/modinv.lp @ d222461 has clause added to the precondition requiring N <= 10, even though the integer bounds are int_range(0, 20). (This clause also occurs in the loop invariant, as a temporary workaround for issue #2). If we remove these clauses and attempt to run the specification, the synthesiser starts to produce counterexamples like the following:
In the course of satisfying this example, a reasonable program might compute x*y = 19*18 = 342 or (x*y-x)%n + x = 3 + 19 = 22, both of which exceed the maximum integer bound and prevent such programs from being synthesised. In fact, it's probable that, with respect to reasonable limits on the number of lines, there is no program solving this problem that doesn't use intermediate values exceeding these integer bounds for this input.
The synthesis process would therefore continue until a program much longer than necessary is found, or perhaps even forever.
Cause:
The counterexample finder is able to compute inputs and expected outputs for this example that all lie within the integer bounds, so the tacit assumption is that a program therefore exists that performs the computation within these bounds, and the synthesised program is now required to satisfy this unsatisfiable example. The counterexample finder does not have enough information to know that the program will require intermediate values greater than either the input or output values.
Possible solutions:
The crude solution currently employed is to limit the sizes of the input variables below the integer bounds, so that the corresponding intermediate values are brought back within the bounds. However, this requires a judgement by the user, who does not necessarily know the right limits to set.
A better solution along the same theme might involve somehow observing the behaviour of candidate programs that cause integer overflow on some inputs but are correct on many others, to get an idea of what kind of intermediate values are involved, and then automatically increasing the integer bounds (or decreasing the bounds on the input) to accommodate. However, this also seems like it might be fragile.
The problem may more effectively be eliminated at its root by forbidding counterexamples based on integer overflow of the program for given inputs, when the program does satisfy other inputs without overflow. This would require that the program simulator provide more specific information about program failure. Care would need to be taken that this does not allow incorrect programs to be ultimately accepted.
Motivating example:
examples/template/modinv.lp @ d222461has clause added to the precondition requiringN <= 10, even though the integer bounds areint_range(0, 20). (This clause also occurs in the loop invariant, as a temporary workaround for issue #2). If we remove these clauses and attempt to run the specification, the synthesiser starts to produce counterexamples like the following:In the course of satisfying this example, a reasonable program might compute
x*y = 19*18 = 342or(x*y-x)%n + x = 3 + 19 = 22, both of which exceed the maximum integer bound and prevent such programs from being synthesised. In fact, it's probable that, with respect to reasonable limits on the number of lines, there is no program solving this problem that doesn't use intermediate values exceeding these integer bounds for this input.The synthesis process would therefore continue until a program much longer than necessary is found, or perhaps even forever.
Cause:
The counterexample finder is able to compute inputs and expected outputs for this example that all lie within the integer bounds, so the tacit assumption is that a program therefore exists that performs the computation within these bounds, and the synthesised program is now required to satisfy this unsatisfiable example. The counterexample finder does not have enough information to know that the program will require intermediate values greater than either the input or output values.
Possible solutions:
The crude solution currently employed is to limit the sizes of the input variables below the integer bounds, so that the corresponding intermediate values are brought back within the bounds. However, this requires a judgement by the user, who does not necessarily know the right limits to set.
A better solution along the same theme might involve somehow observing the behaviour of candidate programs that cause integer overflow on some inputs but are correct on many others, to get an idea of what kind of intermediate values are involved, and then automatically increasing the integer bounds (or decreasing the bounds on the input) to accommodate. However, this also seems like it might be fragile.
The problem may more effectively be eliminated at its root by forbidding counterexamples based on integer overflow of the program for given inputs, when the program does satisfy other inputs without overflow. This would require that the program simulator provide more specific information about program failure. Care would need to be taken that this does not allow incorrect programs to be ultimately accepted.