Changing line 2 of examples/template/gcd.lp @ 48dff02 to #const ceiling=20., and running this with main/TemplateLearn.hs, the correct while loop body is generated, but this candidate takes longer than a few minutes to verify the correctness:
[jjc311@pixel35:~/ws/main]$ ./TemplateLearn.hs --echo-asp ../examples/template/gcd.lp
[...]
Synthesising the program fragment between conditions:
Pre: gcd(X,Y,G1), gcd(X0,Y0,G1), Y > 0, Y1 = Y, X0+Y0 > 0, X+Y > 0.
Post: gcd(X,Y,G1), gcd(X0,Y0,G1), Y < Y1, X0+Y0 > 0, X+Y > 0.
[...]
Found the following program:
1. g = y
2. y = x % g
3. x = g
Searching for a counterexample to falsify the postcondition...
<-- #const time_max=40.
<-- #const int_min=0.
<-- #const int_max=20.
<-- #include "counterexample.lp".
<-- input_var(x; x0; y; y0; y1).
<-- output_var(y; x).
<--
<-- line_instr(3,set(x,var(g))).
<-- line_instr(2,set(y,mod(var(x),var(g)))).
<-- line_instr(1,set(g,var(y))).
<--
<-- precon :- gcd(In_x,In_y,G1), gcd(In_x0,In_y0,G1), In_y > 0, In_y1 = In_y, In_x0+In_y0 > 0, In_x+In_y > 0, counter_in(x, In_x), counter_in(x0, In_x0), counter_in(y, In_y), counter_in(y0, In_y0), counter_in(y1, In_y1).
<-- :- not precon.
<--
<-- postcon(Out_y, Out_x) :- gcd(Out_x,Out_y,G1), gcd(In_x0,In_y0,G1), Out_y < In_y1, In_x0+In_y0 > 0, Out_x+Out_y > 0, counter_in(x0, In_x0), counter_in(y0, In_y0), counter_in(y1, In_y1), int(Out_y), int(Out_x).
<-- :- postcon(Out_y, Out_x), counter_out(y, Out_y), counter_out(x, Out_x).
<--
<-- counter_expected_out(y, Out_y) :- postcon(Out_y, _).
<-- counter_expected_out(x, Out_x) :- postcon(_, Out_x).
<-- #include "../examples/template/gcd.lp".
[LONG DELAY]
Cause:
This is apparently because of the large search space generated by the 5 input variables configured for this program fragment, even though it is not necessary in informal reasoning to consider separately the values of x0 and y0, but rather just gcd(x0,y0)
Possible Solutions:
Just reducing the domain of variable values does reduce the search time to a tolerable duration, but of course this might not scale to all problems.
Automatically propagating more information from previous preconditions, to strengthen the current precondition, might cut down the search space; on the other hand, it might also increase it by introducing more variables.
If this doesn't work, some stronger kind of reasoning about the relationships that can be established between input variables (and output variables) to remove spurious regions of the search space might ultimately be require to achieve tolerable performance in all cases.
Motivating Example:
Changing line 2 of
examples/template/gcd.lp @ 48dff02to#const ceiling=20., and running this withmain/TemplateLearn.hs, the correct while loop body is generated, but this candidate takes longer than a few minutes to verify the correctness:Cause:
This is apparently because of the large search space generated by the 5 input variables configured for this program fragment, even though it is not necessary in informal reasoning to consider separately the values of
x0andy0, but rather justgcd(x0,y0)Possible Solutions:
Just reducing the domain of variable values does reduce the search time to a tolerable duration, but of course this might not scale to all problems.
Automatically propagating more information from previous preconditions, to strengthen the current precondition, might cut down the search space; on the other hand, it might also increase it by introducing more variables.
If this doesn't work, some stronger kind of reasoning about the relationships that can be established between input variables (and output variables) to remove spurious regions of the search space might ultimately be require to achieve tolerable performance in all cases.