Benchmarks ITS: non linear

Here, we list all benchmarks from Complexity_ITS_Non_Linear and provide sources and context for all 22 programs. The benchmarks can be downloaded here. To test our benchmarks, we suggest to use our web interface for integer programs. For more precise bounds, please refer to the “All Bounds” section at the end of the generated proof.

non_linear01.koat

This benchmark is the simple, non-linear prs-loop which has logarithmic runtime from the introduction of our paper.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR X1 X2 X3 X4 X5)
(RULES
  l0(X1, X2, X3, X4, X5) -> l1(X1, X2, X3, X4, X5)
  l1(X1, X2, X3, X4, X5) -> l1(3*X1 + 2*X2, -5*X1 -3*X2, X3, -2*X4, 3*X5 + X3^2) :|: X4^2 - X3^5 < X5 && X4 != 0
)

non_linear02.koat

This program corresponds to the chained version of the introductory loop from our paper, i.e., we chained the loop of non_linear01.koat once.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR X1 X2 X3 X4 X5)
(RULES
  l0(X1, X2, X3, X4, X5) -> l1(X1, X2, X3, X4, X5)
  l1(X1, X2, X3, X4, X5) -> l1(-X1, -X2, X3, 4*X4, 9*X5) :|: X4^2 - X3^5 < X5 && X4 != 0
)

non_linear03.koat

This benchmark is also a simple, non-linear prs-loop which has logarithmic runtime. In contrast to non_linear02.koat, we consider the product of two different variables X1 and X2.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR X1 X2 X3)
(RULES
  l0(X1, X2, X3) -> l1(X1, X2, X3)
  l1(X1, X2, X3) -> l1(2*X1, 3*X2, 4*X3) :|: X3^2 < X1 * X2 && X3 != 0
)

non_linear04.koat

This benchmark is prs-loop which has a disjunction in its guard.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR X1 X2 X3)
(RULES
  l0(X1, X2, X3) -> l1(X1, X2, X3)
  l1(X1, X2, X3) -> l1(2*X1, 3*X2, 4*X3) :|: X3 < X1 && X3 > 0
  l1(X1, X2, X3) -> l1(2*X1, 3*X2, 4*X3) :|: X3 < X2 && X3 > 0
)

non_linear05.koat

This benchmark is a prs-loop which can be transformed into the twn-loop while(X2 < X1 ∧ 0 < X2) do X1 = 2*X1; X2 = 3*X2; (which does not admit a linear ranking function over the reals (see Leike & Heizmann here, Thm. 4.5)) by the automorphism ϑ(X1) = X2 - X1 and ϑ(X2) = 2*X1 - X2, and its inverse ϑ⁻¹(X1) = X1 + X2 and ϑ⁻¹(X1) = 2*X1 + X2.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR X1 X2)
(RULES
  l0(X1, X2) -> l1(X1, X2)
  l1(X1, X2) -> l1(4*X1 - X2, 2*X1 + X2) :|: 3*X1 < 2*X2 && X2 < 2*X1
)

non_linear06.koat

This benchmark corresponds to the unsolvable loop (3) which is transformed into non_linear01.koat by using the polynomial 2*Y1 - Y2.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR X1 X2 X3 X4 Y1 Y2)
(RULES
  l0(X1, X2, X3, X4, Y1, Y2) -> l1(X1, X2, X3, X4, Y1, Y2)
  l1(X1, X2, X3, X4, Y1, Y2) -> l1(3*X1 + 2*X2, -5*X1 -3*X2, X3, -2*X4, Y1 + Y1^2 + X3^2, -4*Y1 + 2*Y1^2 + 3*Y2 + X3^2) :|: X4^2 - X3^5 < 2*Y1 - Y2 && X4 != 0
)

non_linear07.koat

This benchmark is an unsolvable loop which has a disjunction in its guard and which is transformed into non_linear03.koat by using the polynomial Y1 + 2*Y2.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR Y1 Y2 X2 X3)
(RULES
  l0(Y1, Y2, X2, X3) -> l1(Y1, Y2, X2, X3)
  l1(Y1, Y2, X2, X3) -> l1(2*Y1^2 + 2*Y1, -Y1^2 + 2*Y2, 3*X2, 4*X3) :|: X3 < Y1 + 2*Y2 && X3 > 0
  l1(Y1, Y2, X2, X3) -> l1(2*Y1^2 + 2*Y1, -Y1^2 + 2*Y2, 3*X2, 4*X3) :|: X3 < X2 && X3 > 0
)

non_linear08.koat

This benchmark is an unsolvable loop which has a disjunction in its guard and which is transformed into non_linear03.koat by using the polynomials Y1 + 2*Y2 and Z1 - Z2.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR Y1 Y2 Z1 Z2 X3)
(RULES
  l0(Y1, Y2, Z1, Z2, X3) -> l1(Y1, Y2, Z1, Z2, X3)
  l1(Y1, Y2, Z1, Z2, X3) -> l1(2*Y1^2 + 2*Y1, -Y1^2 + 2*Y2, Z1^3 - 3*Z2, Z1^3 - 3*Z1, 4*X3) :|: X3 < Y1 + 2*Y2 && X3 > 0
  l1(Y1, Y2, Z1, Z2, X3) -> l1(2*Y1^2 + 2*Y1, -Y1^2 + 2*Y2, Z1^3 - 3*Z2, Z1^3 - 3*Z1, 4*X3) :|: X3 < Z1 - Z2 && X3 > 0
)

non_linear09.koat

This ITS is the leading example of our paper. Here, the loop at location l2 corresponds to the loop non_linear01.koat.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR X1 X2 X3 X4 X5 X6)
(RULES
  l0(X1, X2, X3, X4, X5, X6) -> l1(X1, X2, X3, X4, X5, X6)
  l1(X1, X2, X3, X4, X5, X6) -> l2(X6, X6, 2, X3, X6, X6 - Y) :|: 0 < Y && Y <= X6
  l2(X1, X2, X3, X4, X5, X6) -> l1(X1, X2, X3, X4, X5, X6)
  l2(X1, X2, X3, X4, X5, X6) -> l2(3*X1 + 2*X2, -5*X1 -3*X2, X3, -2*X4, 3*X5 + X3^2, X6) :|: X4^2 - X3^5 < X5 && X4 != 0
  l1(X1, X2, X3, X4, X5, X6) -> l3(X1, X2, X3, X4, X5, X1) :|: X6 <= 0
  l3(X1, X2, X3, X4, X5, X6) -> l3(X1, X2, X3, X4, X5, X6 - 1) :|: X6 > 0
)

non_linear10.koat

This benchmark is similar to non_linear09.koat. However, instead of using the loop non_linear01.koat at location l2, this example uses the unsolvable loop from non_linear06.koat.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR X1 X2 X3 X4 Y1 Y2 X6)
(RULES
  l0(X1, X2, X3, X4, Y1, Y2, X6) -> l1(X1, X2, X3, X4, Y1, Y2, X6)
  l1(X1, X2, X3, X4, Y1, Y2, X6) -> l2(X6, X6, 2, X3, X6, X6, X6 - Y) :|: 0 < Y && Y <= X6
  l2(X1, X2, X3, X4, Y1, Y2, X6) -> l1(X1, X2, X3, X4, Y1, Y2, X6)
  l2(X1, X2, X3, X4, Y1, Y2, X6) -> l2(3*X1 + 2*X2, -5*X1 -3*X2, X3, -2*X4, Y1 + Y1^2 + X3^2, -4*Y1 + 2*Y1^2 + 3*Y2 + X3^2,X6) :|: X4^2 - X3^5 < 2*Y1 - Y2 && X4 != 0
  l1(X1, X2, X3, X4, Y1, Y2, X6) -> l3(X1, X2, X3, X4, Y1, Y2, X1) :|: X6 <= 0
  l3(X1, X2, X3, X4, Y1, Y2, X6) -> l3(X1, X2, X3, X4, Y1, Y2, X6 - 1) :|: X6 > 0
)

non_linear11.koat

This benchmark corresponds to the commuting program of Fig. 5 in the paper.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR X1 X2 X3)
(RULES
  l0(X1, X2, X3) -> l1(X1, X2, X3)
  l1(X1, X2, X3) -> l1(X1 - 1, X2, X3 + X2^2) :|: X1 > 0
  l1(X1, X2, X3) -> l1(X1 - 1, X2, X3 + X2^2 + 1) :|: X1 > 0
  l1(X1, X2, X3) -> l2(X1, X2, X3)
  l2(X1, X2, X3) -> l2(X1, X2, X3 - 1) :|: X3 > 0
)

non_linear12.koat

This benchmark is an advanced version of the previous example. Here, the update of X1 and X2 is not twn.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR X1 X2 X3)
(RULES
  l0(X1, X2, X3, X4) -> l1(X1, X2, X3, X4)
  l1(X1, X2, X3, X4) -> l1(3*X1 + 2*X2 + X3^2, -5*X1 -3*X2, X3, X4 - 1) :|: X4 > 0
  l1(X1, X2, X3, X4) -> l1(3*X1 + 2*X2 + X3^2, -5*X1 -3*X2, X3, X4 - 2) :|: X4 > 0
  l1(X1, X2, X3, X4) -> l2(X1, X2, X3, X1) :|: X4 <= 0
  l2(X1, X2, X3, X4) -> l2(X1, X2, X3, X4 - 1) :|: X4 > 0
)

non_linear13.koat

This benchmark consists of two consecutive loops. In the first loop, we double X2 in every iteration. Hence, the value of X2 is exponential after the first loop. However, the program still has linear runtime as the second loop is only executed a logarithmic number of times.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR X1 X2 X3)
(RULES
  l0(X1, X2, X3) -> l1(X1, X2, X3)
  l1(X1, X2, X3) -> l1(X1 - 1, 2 * X2, X3) :|: X1 > 0
  l1(X1, X2, X3) -> l2(X1, X2, X3)
  l2(X1, X2, X3) -> l2(X1, 2*X2, 3*X3) :|: X3 < X2 && X3 > 0
)

non_linear14.koat

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

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR X1 X2 X3 X4 Y1 Y2 U V)
(RULES
  l0(X1, X2, X3, X4, Y1, Y2) -> l1(U, X2, X3, X4, Y1, Y2)
  l1(X1, X2, X3, X4, Y1, Y2) -> l1(X1 + 1, X2, X3, X4, Y1, Y2) :|: 1 <= X1 && X1 <= 3 && V = 0
  l2(X1, X2, X3, X4, Y1, Y2) -> l1(X1, X2 - 1, X3, X4, Y1, Y2)
  l1(X1, X2, X3, X4, Y1, Y2) -> l2(X1, X2, X3, X4, Y1, Y2) :|: X2 > 0 && V = 1
  l2(X1, X2, X3, X4, Y1, Y2) -> l3(X1, X2, X3, X4, Y1, Y2)
  l3(X1, X2, X3, X4, Y1, Y2) -> l3(X1, X2, X3, -2*X4, Y1 + Y1^2 + X3^2, -4*Y1 + 2*Y1^2 + 3*Y2 + X3^2) :|: X4^2 - X3^5 < 2*Y1 - Y2 && X4 != 0
)

non_linear15.koat

This benchmark consists of two commuting twn-loops which both do not admit a linear ranking function over the reals (see Leike & Heizmann here, Thm. 4.5) but can be handled individually by our twn-technique. However, this combination of two twn-loops needs more advanced techniques.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR X1 X2)
(RULES
  l0(X1, X2) -> l1(X1, X2)
  l1(X1, X2) -> l1(2*X1, 3*X2) :|: X2 < X1 && X2 > 0
  l1(X1, X2) -> l1(2*X1, 4*X2) :|: X2 < X1 && X2 > 0
)

non_linear16.koat

This benchmark consists of a twn-loop and a second loop which cannot be handled by our techniques for loops as it contains temporary variables. Furthermore, this second loop needs a MPRF of depth at least two.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR X1 X2 Y1 Y2 T)
(RULES
  l0(X1, X2, Y1, Y2) -> l1(X1, X2, Y1, Y2)
  l1(X1, X2, Y1, Y2) -> l1(2*X1, 3*X2, Y1, Y2) :|: X2 < X1 && X2 > 0
  l1(X1, X2, Y1, Y2) -> l2(X1, X2, Y1, Y2)
  l2(X1, X2, Y1, Y2) -> l2(X1, X2, Y1 + Y2, Y2 - T) :|: Y1 > 0 && T > 0
)

non_linear17.koat

Here, we have extended the example from our earlier paper here, Fig.7 by a twn-loop which has a logarithmic runtime and thus yields linear size bounds. These linear size bounds are important for a third loop which decrements Y1 iteratively by one.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR X1 X2 X3 X4 Y1 Y2 U V)
(RULES
  l0(X1, X2, X3, X4, Y1, Y2) -> l1(U, X2, X3, X4, Y1, Y2)
  l1(X1, X2, X3, X4, Y1, Y2) -> l1(X1 + 1, X2, X3, X4, Y1, Y2) :|: 1 <= X1 && X1 <= 3 && V = 0
  l2(X1, X2, X3, X4, Y1, Y2) -> l1(X1, X2 - 1, X3, X4, Y1, Y2)
  l1(X1, X2, X3, X4, Y1, Y2) -> l2(X1, X2, X3, X4, Y1, Y2) :|: X2 > 0 && V = 1
  l2(X1, X2, X3, X4, Y1, Y2) -> l3(X1, X2, X3, X4, Y1, Y2)
  l3(X1, X2, X3, X4, Y1, Y2) -> l3(X1, X2, X3, X4, 2*Y1, 3*Y2):|: Y2 < Y1 && Y2 > 0
  l3(X1, X2, X3, X4, Y1, Y2) -> l4(X1, X2, X3, X4, Y1, Y2)
  l4(X1, X2, X3, X4, Y1, Y2) -> l4(X1, X2, X3, X4, Y1 - 1, Y2) :|: Y1 > 0
)

non_linear18.koat

This benchmarks contains a non-unit, solvable loop at location l1. The eigenvalues of this loop have absolute value 1/2 * (5 + sqrt(33)). Hence, the value of X1 is exponential before the second loop and thus also the runtime of the complete program is exponential.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR X1 X2 X3)
(RULES
  l0(X1, X2, X3) -> l1(X1, X2, X3)
  l1(X1, X2, X3) -> l1(X1 + 2*X2, 3*X1 + 4*X2, X3 - 1) :|: X3 > 0
  l1(X1, X2, X3) -> l2(X1, X2, X3)
  l2(X1, X2, X3) -> l2(X1 - 1, X2, X3) :|: X1 > 0
)

non_linear19.koat

This benchmark is a more advanced version of the twn-loop while(X2 < X1 ∧ 0 < X2) do X1 = 2*X1; X2 = 3*X2; (which does not admit a linear ranking function over the reals (see Leike & Heizmann here, Thm. 4.5)). Here, we extended this loop by the update of X3. The first loop is not a solvable loop. However, the update still admits a (super-exponential) closed form for X3. As the first loop has a logarithmic runtime complexity, the overall size of X3 is still polynomial and thus the runtime of the complete program is also polynomial.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR X1 X2 X3)
(RULES
  l0(X1,X2,X3) -> l1(X1,X2,X3)
  l1(X1,X2,X3) -> l1(2*X1,3*X2,X3^2) :|: X2 < X1 && 0 < X2
  l1(X1,X2,X3) -> l2(X1,X2,X3)
  l2(X1,X2,X3) -> l2(X1,X2,X3 - 1) :|: X3 > 0
)

non_linear20.koat

This benchmark is a more advanced version of the twn-loop while(X2 < X1 ∧ 0 < X2) do X1 = 2*X1; X2 = 3*X2; (which does not admit a linear ranking function over the reals (see Leike & Heizmann here, Thm. 4.5)). Here, we introduced a temporary variable and consider the following loop while(X2 < X1 ∧ 0 < X2) do X1 = 2*X1; X2 >= 3*X2;. Our current technique is not able to succeed on this benchmark.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR X1 X2)
(RULES
  l0(X1, X2) -> l1(X1, X2)
  l1(X1, X2) -> l1(2*X1, T*X2) :|: X2 < X1 && 0 < X2 && T >= 3
)

non_linear21.koat

This benchmark corresponds to the more advanced version of our leading example non_linear09.koat in which we replaced the simple loop at location l2 by a simple cycle of length two. Note that an update of an integer program is performed simultaneously on all variables, whereas in a C program each variable is updated individually. Hence, we excluded this benchmark from the other collection Complexity_C_Non_Linear.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR X1 X2 X3 X4 X5 X6)
(RULES
  l0(X1, X2, X3, X4, X5, X6) -> l1(X1, X2, X3, X4, X5, X6)
  l1(X1, X2, X3, X4, X5, X6) -> l2(X6, X6, 2, X3, X6, X6 - Y) :|: 0 < Y && Y <= X6
  l2(X1, X2, X3, X4, X5, X6) -> l1(X1, X2, X3, X4, X5, X6)
  l2(X1, X2, X3, X4, X5, X6) -> l2a(3*X1 + 2*X2, -5*X1 -3*X2, X3, X4, X5, X6) :|: X4^2 - X3^5 < X5 && X4 != 0
  l2a(X1, X2, X3, X4, X5, X6) -> l2(X1, X2, X3, -2*X4, 3*X5 + X3^2, X6)
  l1(X1, X2, X3, X4, X5, X6) -> l3(X1, X2, X3, X4, X5, X1) :|: X6 <= 0
  l3(X1, X2, X3, X4, X5, X6) -> l3(X1, X2, X3, X4, X5, X6 - 1) :|: X6 > 0
)

non_linear22.koat

This benchmark corresponds to a more advanced version of our example non_linear11.koat in which we replaced the simple loop at location l1 by a simple cycle of length three. Note that an update of an integer program is performed simultaneously on all variables, whereas in a C program each variable is updated individually. Hence, we also excluded this benchmark from the other collection Complexity_C_Non_Linear.

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR X1 X2 X3)
(RULES
  l0(X1, X2, X3) -> l1(X1, X2, X3)
  l1(X1, X2, X3) -> l1a(X1 - 1, X2, X3) :|: X1 > 0
  l1b(X1, X2, X3) -> l1c(X1, X2, X3)
  l1c(X1, X2, X3) -> l1(X1, X2, X3 + X2^2)
  l1(X1, X2, X3) -> l1(X1 - 1, X2, X3 + X2^2 + 1) :|: X1 > 0
  l1(X1, X2, X3) -> l2(X1, X2, X3)
  l2(X1, X2, X3) -> l2(X1, X2, X3 - 1) :|: X3 > 0
)