Here, we list all benchmarks from Complexity_ITS_Size_Non_Linear and provide sources and context for all 15 programs. The benchmarks can be downloaded here. To test our benchmarks, we suggest to use our web interface for integer programs.
size01.koat
This benchmark is a simple linear loop which has linear size bounds. It corresponds to the loop from our paper.
(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR A B C D)
(RULES
l0(A,B,C,D) -> l1(A,B,C,D)
l1(A,B,C,D) -> l1(A - 1,3*B + 2*C,-5*B - 3*C,A^2 + D) :|: A > 0
)
size02.koat
This benchmark consists of the benchmark size01.koat and a consecutive loop.
(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR A B C D)
(RULES
l0(A,B,C,D) -> l1(A,B,C,D)
l1(A,B,C,D) -> l1(A - 1,3*B + 2*C,-5*B - 3*C,A^2 + D) :|: A > 0
l1(A,B,C,D) -> l2(A,B,C,D)
l2(A,B,C,D) -> l2(A,B - 1,C - 1,D) :|: B + C > 0
)
size03.koat
This benchmark consists of the benchmark size01.koat and a consecutive loop.
(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR A B C D)
(RULES
l0(A,B,C,D) -> l1(A,B,C,D)
l1(A,B,C,D) -> l1(A - 1,3*B + 2*C,-5*B - 3*C,A^2 + D) :|: A > 0
l1(A,B,C,D) -> l2(A,B,C,D)
l2(A,B,C,D) -> l2(A,B,C,D - 1) :|: D > 0
)
size04.koat
This benchmark is a combination of size02.koat and size03.koat.
(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR A B C D)
(RULES
l0(A,B,C,D) -> l1(A,B,C,D)
l1(A,B,C,D) -> l1(A - 1,3*B + 2*C,-5*B - 3*C,A^2 + D) :|: A > 0
l1(A,B,C,D) -> l2(A,B,C,D)
l2(A,B,C,D) -> l2(A,B - 1,C - 1,D - 1) :|: B + C + D > 0
)
size05.koat
The first loop needs our twn-technique to prove termination.
(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR A B C)
(RULES
l0(A,B,C) -> l1(A,B,C)
l1(A,B,C) -> l1(A - B^2,B + C^2,C) :|: A > 0 && C != 0
l1(A,B,C) -> l2(A,B,C) :|: A <= 0
l2(A,B,C) -> l2(A,B - 1,C) :|: B > 0
)
size06.koat
This program consists of three consecutive loops.
The first loop can be solved by MΦRFs of depth 2 (see Ben-Amram & Genaim here, Table 1 - Loop 20) or our twn-technique.
The second loop is a twn-loop which terminates as A eventually outgrows B^2.
The last loop decreases A until A becomes non-positive.
(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR A B C)
(RULES
l0(A,B,C) -> l1(A,B,C) :|: A > 0
l1(A,B,C) -> l1(A + C,B,C - 1) :|: C > 0
l1(A,B,C) -> l2(A,B,C) :|: C <= 0
l2(A,B,C) -> l2(A + C^2,B + 1,C + 1) :|: A < B^2
l2(A,B,C) -> l3(A,B,C) :|: A >= B^2
l3(A,B,C) -> l3(A - 1,B,C) :|: A > 0
)
size07.koat
The first loop has the eigenvalues 0 and 1. The second loop only has the eigenvalue 1. Hence, both loops are unit prs loops and thus both have polynomial size bounds. This benchmark also contains non-linear arithmetic.
(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR A B C D)
(RULES
l0(A,B,C,D) -> l1(A,B,C,D)
l1(A,B,C,D) -> l1(A - 1,3*B + 1*C,-6*B + -2*C,D + 2*A^2) :|: A > 0
l1(A,B,C,D) -> l2(A,B,C,D) :|: A <= 0
l2(A,B,C,D) -> l2(A,B - 1,C,D - 1) :|: B + D > 0
)
size08.koat
This benchmark is a terminating version of the twn-loop Frohn et al., Ex. 24) with a consecutive second loop.
To ensure termination, we have added the precondition and invariant C < 0.
Thus, the value of A always decreases, and at some point is less than -B^2.
Additionally, we have added a consecutive loop to decrease B.
(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR A B C)
(RULES
l0(A,B,C) -> l1(A,B,C) :|: C < 0
l1(A,B,C) -> l1(A + B^2*C,B - 2*C^2,C) :|: A + B^2 > 0
l1(A,B,C) -> l2(A,B^2,C) :|: A <= 0
l2(A,B,C) -> l2(A,B - 1,C) :|: B > 0
)
size09.koat
This benchmark corresponds to the running example of our paper.
(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR A B C D E)
(RULES
l0(A,B,C,D,E) -> l1(A,B,C,D,E) :|: A > 0 && E > 0
l1(A,B,C,D,E) -> l1(A - 1,3*B + 2*C,-5*B - 3*C,A^2 + D,E) :|: A > 0
l1(A,B,C,D,E) -> l2(A,B,C,D,E)
l2(A,B,C,D,E) -> l2(A,B - 1,C,D,E) :|: B > 0
l2(A,B,C,D,E) -> l1(E,2*E,3*E,A,E - 1) :|: E > 0
)
size10.koat
This benchmark is an advanced version of our running example size09.koat.
(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR A B C D E)
(RULES
l0(A,B,C,D,E) -> l1(A,B,C,D,E) :|: A > 0 && E > 0
l1(A,B,C,D,E) -> l1(A - 1,3*B + 2*C,-5*B - 3*C,A^2 + D,E) :|: A > 0
l1(A,B,C,D,E) -> l2(A,B,C,D,E)
l2(A,B,C,D,E) -> l2(A,B - 1,C,D - 1,E) :|: B + D > 0
l2(A,B,C,D,E) -> l1(E,2*E,3*E,A,E - 1) :|: E > 0
)
size11.koat
This program is similar the example of Ben-Amram et al. but we have added a consecutive loop which decreases A until it is negative.
Note that all variables have polynomial size bounds in this program.
However, KoAT2 currently only infers polynomial bounds for B and E.
(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR A B C D E)
(RULES
l0(A,B,C,D,E) -> l1(A,B,C,D,E)
l1(A,B,C,D,E) -> l2(A,B,C,D,E - 1) :|: E > 0
l2(A,B,C,D,E) -> l3(A,B,A + B,B,E)
l2(A,B,C,D,E) -> l3(A,B,B,A + B,E)
l3(A,B,C,D,E) -> l1(C + D,B,C,D,E)
l1(A,B,C,D,E) -> l4(A,B,C,D,E) :|: E <= 0
l4(A,B,C,D,E) -> l4(A - 1,B,C,D,E) :|: A >= 0
)
size12.koat
This program is the motivating example of Ben-Amram and Hamilton. Again, all variables have polynomial size bounds in this program.
(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR A B C D T1 T2)
(RULES
l0(A,B,C,D,T1,T2) -> l1(A,B,C,D,A,0)
l1(A,B,C,D,T1,T2) -> l2(A,B,C,D,T1 - 1,B + C) :|: T1 > 0
l2(A,B,C,D,T1,T2) -> l3(A,B,C,D,T1,T2 - 1) :|: T2 > 0
l3(A,B,C,D,T1,T2) -> l4(A,D,A,D,T1,T2)
l3(A,B,C,D,T1,T2) -> l4(A,A,D,D,T1,T2)
l4(A,B,C,D,T1,T2) -> l2(A,B,C,D,T1,T2)
l2(A,B,C,D,T1,T2) -> l1(A,B,C,B + C,T1,T2)
l2(A,B,C,D,T1,T2) -> l5(A,B,C,D,T1,T2)
l5(A,B,C,D,T1,T2) -> l6(A,B,C,D - 1,T1,T2) :|: D > 0
l6(A,B,C,D,T1,T2) -> l5(A,B,A + B + C,D,T1,T2)
l6(A,B,C,D,T1,T2) -> l5(A,A,B,D,T1,T2)
)
size13.koat
A simplified variant of size13.koat where we additionally added non-linear arithmetic.
(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR A B C D T1 T2 T3)
(RULES
l0(A,B,C,D,T1,T2,T3) -> l1(A,B,C,D,A,0,0)
l1(A,B,C,D,T1,T2,T3) -> l2(A,B,C,D,T1 - 1,B + C,T3 + T1^2) :|: T1 > 0
l2(A,B,C,D,T1,T2,T3) -> l3(A,B,C,D,T1,T2 - 1,T3) :|: T2 > 0
l3(A,B,C,D,T1,T2,T3) -> l2(A,D,A,D,T1,T2,T3)
l2(A,B,C,D,T1,T2,T3) -> l1(A,B,C,B,T1,T2,T3)
l2(A,B,C,D,T1,T2,T3) -> l5(A,B,C,D,T1,T2,T3)
l5(A,B,C,D,T1,T2,T3) -> l5(A,B,C,D,T1,T2,T3 - 1) :|: T3 > 0
)
size14.koat
The first loop is not a solvable loop.
However, the update still admits a closed form for B.
Currently, KoAT cannot handle this example and thus does not infer a (super-exponential) runtime bound.
(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR A B)
(RULES
l0(A,B) -> l1(A,2)
l1(A,B) -> l1(A - 1,B^2) :|: A > 0
l1(A,B) -> l2(A,B) :|: A <= 0
l2(A,B) -> l2(A,B - 1) :|: B > 0
)
size15.koat
This example combines an integer program which needs control-flow refinement (see Giesl et al. here, Fig.7) to be solved, a twn-loop, and a consecutive loop counting down B.
(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR X Y U V A B C)
(RULES
l0(X,Y,A,B,C) -> l1(U,Y,A,B,C)
l1(X,Y,A,B,C) -> l1(X+1,Y,A,B,C) :|: 1 <= X && X <= 3 && V = 0
l2(X,Y,A,B,C) -> l1(X,Y-1,A,B,C)
l1(X,Y,A,B,C) -> l2(X,Y,A,B,C) :|: Y > 0 && V = 1
l2(X,Y,A,B,C) -> l3(X,Y,A,B,C)
l3(X,Y,A,B,C) -> l3(X,Y,A + C^3,B + C^2,C + 1) :|: A < B && C != 0
l3(X,Y,A,B,C) -> l4(X,Y,A,B,C)
l4(X,Y,A,B,C) -> l4(X,Y,A,B - 1,C) :|: B > 0
)