Benchmarks Complexity_ITS_Non_Linear

Here, we list all benchmarks from Complexity_ITS_Non_Linear and provide sources and context for all 20 programs. The benchmarks can be downloaded here. To test our benchmarks, we suggest to use our web interface for integer programs.

twn01.koat

This benchmark is a simple linear loop which does not have a ranking function over the reals (see Leike & Heizmann here, Thm. 4.5) but can be solved by our twn-technique.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR A B)
(RULES
  l0(A,B) -> l1(A,B) :|: A > 0
  l1(A,B) -> l1(3 * A,2 * B) :|: A < B
)

twn02.koat

This benchmark is an advanced, slightly changed version of twn01.koat by adding non-linear arithmetic.

(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(5 * A + C^2,2 * B,C) :|: A < B^2
)

twn03.koat

This program consists of two consecutive loops. The first loop at location l1 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 at the successor location l2 of l1 corresponds to the loop in twn02.koat.

(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(5 * A + C^2,2 * B,C) :|: A < B^2
)

twn04.koat

This example consists of two nested loops. The inner loop at location l2 corresponds to the loop in twn02.koat. The outer loop is evaluated at most C times and resets both variables A and B in every iteration.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR A B C D E)
(RULES
  l0(A,B,C,D,E) -> l1(D,E,C,D,E)
  l1(A,B,C,D,E) -> l2(A,B,C,D,E) :|: C > 0
  l2(A,B,C,D,E) -> l2(5 * A + C^2,2 * B,C,D,E) :|: A < B && A > 0
  l2(A,B,C,D,E) -> l1(D,E,C - 1,D,E)
)

twn05.koat

This benchmark is an advanced version of twn04.koat. While twn04.koat contains two loops, this program consists of three loops by adding the self-loop at location l3. This additional loop can be solved by MΦRFs of depth 2 (see Ben-Amram & Genaim here, Table 1 - Loop 20) or our twn-technique.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR A B C D E F)
(RULES
  l0(A,B,C,D,E,F) -> l1(D,E,C,D,E,F) :|: F > 0
  l1(A,B,C,D,E,F) -> l1(A + C,B,C - 1,D,E,F) :|: C > 0
  l1(A,B,C,D,E,F) -> l2(A,B,C,C,E,F) :|: C <= 0
  l2(A,B,C,D,E,F) -> l2(5 * A + C^2,2 * B,C,D,E,F) :|: A < B^2 && A >  0
  l2(A,B,C,D,E,F) -> l1(D,E,F,D,E,F - 1) :|: F > 0
)

twn06.koat

This benchmark is similar to twn05.koat. However, instead of using a twn-loop at location l2, this example uses a solvable loop (see Xu & Li here, Ex. 3.3 & 3.4).

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR A B C D E F)
(RULES
  l0(A,B,C,D,E,F) -> l1(D,E,F,D,E,F)
  l1(A,B,C,D,E,F) -> l1(A + C,B,C - 1,D,E,F) :|: C > 0
  l1(A,B,C,D,E,F) -> l2(A,B,F,D,E,F) :|: C <= 0
  l2(A,B,C,D,E,F) -> l2(A, 3 * B - 4 * C, 4 * B - 3 * C, 5 * D, 5 * E - A^2, F) :|: B^2 > 1 && A * C + 2 * A > 0
  l2(A,B,C,D,E,F) -> l1(D,E,F,D,E,F - 1) :|: F > 0
)

twn07.koat

This program consists of two consecutive loops such that one needs to compute size bounds for the self-loop at location l1 with non-linear arithmetic in order to handle the self-loop at location l2.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR A B C)
(RULES
  l0(A,B,C) -> l1(A,B,C)
  l1(A,B,C) -> l1(A - 1,B + C^3, C + 1) :|: A > 0
  l1(A,B,C) -> l2(A,B,C) :|: A <= 0
  l2(A,B,C) -> l2(A,B - 1,C) :|: B > 0
)

twn08.koat

This example combines an integer program which needs control-flow refinement (see Giesl et al. here, Fig.7) to be solved and the twn-loop twn02.koat.

(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,5 * A + C^2,2 * B,C) :|: A < B^2 && A >  0
)

twn09.koat

Our approach can not only handle twn-self-loops but simple cycles which correspond to twn-loops. To this end, we introduce the following benchmark. Note that the cycle consisting of locations l2, l3, and l4 corresponds to the twn-self-loop from twn02.koat.

(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) -> l3(A,B,C - 2 * B) :|: A < B^2
  l3(A,B,C) -> l4(5 * A,B,C + B)
  l4(A,B,C) -> l2(A + C^4,2 * B,C + B)
)

twn10.koat

This program is a twn-loop (see Frohn & Giesl here, Ex. 2).

(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(2,B + 1,-2*C - A, B) :|: C + D > 0
)

twn11.koat

This benchmark corresponds to a loop which can be transformed into a twn-loop by automorphisms (see Frohn et al. here, Ex. 24).

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR A B C)
(RULES
  l0(A,B,C) -> l1(A,B,C)
  l1(A,B,C) -> l1(A + 8*A*B^2 + 16*B^3 + 16*B^2*C,B - A^2 - 4*A*B - 4*A*C - 4*B^2 - 8*B*C - 4*C^2,C - 4*A*B^2 - 8*B^3 - 8*B^2*C + A^2 + 4*A*B + 4*A*C + 4*B^2 + 8*B*C + 4*C^2) :|: 4*B^2+A+B+C > 0
)

twn12.koat

This program is a non-terminating twn-loop (see Frohn et al. here, Ex. 24).

(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*C, B - 2 * C^2, C) :|: A + B^2 > 0
)

twn13.koat

This benchmark is a terminating version of twn12.koat. We have added the precondition and invariant C < 0. So, the value of A always decreases, and at some point is less than -B^2.

(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
)

twn14.koat

This benchmark is an implementation of our running example (see Fig. 1). This example differs from the benchmark twn14.c.

(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) -> l3(A,A,E,D,E) :|: A > 0 && D > 0
  l1(A,B,C,D,E) -> l2(A,A,E,D,E) :|: -5 <= D && D <= 5
  l2(A,B,C,D,E) -> l3(A,A,E,D,E) :|: A > 0
  l3(A,B,C,D,E) -> l3(A,-2 * B, 3 * C - 2 * D^3, D,E) :|: B^2 + D^5 < C && B != 0
  l3(A,B,C,D,E) -> l1(A - 1,B,C,D,E)
)

twn15.koat

This benchmark is an implementation of our second running example (see Fig. 2). This example differs from the benchmark twn15.c.

(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) -> l3(A,A,E,D,E) :|: A > 0 && D > 0
  l1(A,B,C,D,E) -> l2(A,A,E,D,E) :|: -5 <= D && D <= 5
  l2(A,B,C,D,E) -> l3(A,A,E,D,E) :|: A > 0
  l3(A,B,C,D,E) -> l4(A,-2 * B, C, D,E) :|: B^2 + D^5 < C && B != 0
  l4(A,B,C,D,E) -> l3(A,B, 3 * C - 2 * D^3, D,E)
  l3(A,B,C,D,E) -> l1(A - 1,B,C,D,E)
)

twn16.koat

This benchmark has constant runtime and our twn-approach indeed infers a constant runtime bound. In contrast, linear ranking functions only infer a linear bound for this example. Therefore, both configurations KoAT2 + TWN + RF or KoAT2 + TWN + MΦRF5 infer a non-constant linear runtime bound here, since they always search for linear ranking functions first and only if they do not succeed in inferring a finite runtime bound, then these configurations apply our twn-technique.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR A)
(RULES
  l0(A) -> l1(A)
  l1(A) -> l1(17 * A) :|: A > 0 && 42 > A
)

twn17.koat

This benchmark is an advanced version of twn14.koat. Here, we add a location l4 and self-loop which decreases the value of B by 1 until it is non-positive. However, as the value of B can have exponential size w.r.t. the initial values (since the self-loop doubles the absolute value of B iteratively), this benchmark has exponential runtime.

(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) -> l3(A,A,E,D,E) :|: A > 0 && D > 0
  l1(A,B,C,D,E) -> l2(A,A,E,D,E) :|: -5 <= D && D <= 5
  l2(A,B,C,D,E) -> l3(A,A,E,D,E) :|: A > 0
  l3(A,B,C,D,E) -> l3(A,-2 * B, 3 * C - 2 * D^3, D,E) :|: B^2 + D^5 < C && B != 0
  l3(A,B,C,D,E) -> l1(A - 1,B,C,D,E)
  l1(A,B,C,D,E) -> l4(A,B,C,D,E)
  l4(A,B,C,D,E) -> l4(A,B - 1,C,D,E) :|: B > 0
)

twn18.koat

This benchmark is a solvable loop (see Xu & Li here, Ex. 3.3 & 3.4).

(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) -> l1(A, 3 * B - 4 * C, 4 * B - 3 * C, 5 * D, 5 * E - A^2) :|: B^2 > 1 && A * C + 2 * A > 0
)

twn19.koat

This benchmark corresponds to the isolated transition t₅ as in Fig. 1. Note that only our tool with our twn-technique is able to solve this example, i.e., tools based on ranking functions already fail on t₅ alone.

(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(-2 * A, 3 * B - 2 * C^3, C) :|: A^2 + C^5 < B && A != 0
)

twn20.koat

This program corresponds to the chained version of the isolated transition t₅, i.e., it corresponds to t₅ * t₅, as in Fig. 1. Again, only our tool with our twn-technique is able to solve this example.

(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(4 * A, 9 * B - 8 * C^3, C) :|: A^2 + C^5 < B && A != 0
)