From b389181eede995f3e7915302bb4043cec10f544d Mon Sep 17 00:00:00 2001 From: Yuka Ikarashi Date: Sat, 8 Feb 2025 13:23:13 -0500 Subject: [PATCH] simplify unsatisfiable branches --- src/exo/rewrite/dataflow.py | 33 +- .../test_dataflow/test_reverse_x_10.txt | 88 ++---- .../test_dataflow/test_reverse_x_10_lo.txt | 132 +++----- .../test_dataflow/test_reverse_x_11.txt | 90 ++---- .../test_dataflow/test_super_simple.txt | 83 +---- tests/golden/test_dataflow/test_two_loops.txt | 289 +++--------------- 6 files changed, 147 insertions(+), 568 deletions(-) diff --git a/src/exo/rewrite/dataflow.py b/src/exo/rewrite/dataflow.py index 6a8bac04..e45e1491 100644 --- a/src/exo/rewrite/dataflow.py +++ b/src/exo/rewrite/dataflow.py @@ -1071,6 +1071,10 @@ def map_tree(tree: D.node): return tree elif isinstance(tree, D.AffineSplit): + # When assumptions are unsatisfiable, this is a cell without integer points. We Bottom such cases. + if not slv.satisfy((A.Const(True, T.bool, null_srcinfo()))): + return D.Leaf(D.SubVal(V.Bot())) + # we can collapse the tree when all values are the same if ( isinstance(tree.ltz, D.Leaf) @@ -1082,15 +1086,32 @@ def map_tree(tree: D.node): return tree.ltz pred = lift_to_smt_a(tree.ae) + + # If ltz branch is unsatisfiable and the values for eqz and gtz branches are equivalent, we can collapse this node. + if ( + isinstance(tree.eqz, D.Leaf) + and isinstance(tree.gtz, D.Leaf) + and (type(tree.eqz) == type(tree.gtz)) + and (tree.eqz.v == tree.gtz.v) + ): + if not slv.satisfy(mk_aexpr("<", pred)): + return tree.eqz + + # If gtz branch is unsatisfiable and the values for eqz and ltz branches are equivalent, we can collapse this node. + if ( + isinstance(tree.eqz, D.Leaf) + and isinstance(tree.ltz, D.Leaf) + and (type(tree.eqz) == type(tree.ltz)) + and (tree.eqz.v == tree.ltz.v) + ): + if not slv.satisfy(mk_aexpr(">", pred)): + return tree.eqz + # check if anything is simplifiable ltz_eq = mk_aexpr("<", pred) eqz_eq = mk_aexpr("==", pred) gtz_eq = mk_aexpr(">", pred) - # When assumptions are unsatisfiable, this is a cell without integer points. We can Bottom such cases. - if not slv.satisfy((A.Const(True, T.bool, null_srcinfo()))): - return D.Leaf(D.SubVal(V.Bot())) - if slv.verify(eqz_eq): return map_tree(tree.eqz) elif slv.verify(gtz_eq): @@ -1781,7 +1802,9 @@ def widening(a1: D.abs, a2: D.abs) -> D.abs: reconstructed_tree = dict_tree_to_node(dict_tree) print("\nReconstructed Abstract Domain Tree:") - a = abs_simplify(abs_simplify(D.abs(a2.iterators, reconstructed_tree))) + a = abs_simplify( + abs_simplify(abs_simplify(D.abs(a2.iterators, reconstructed_tree))) + ) print(a) return a diff --git a/tests/golden/test_dataflow/test_reverse_x_10.txt b/tests/golden/test_dataflow/test_reverse_x_10.txt index 8334ee7d..52690970 100644 --- a/tests/golden/test_dataflow/test_reverse_x_10.txt +++ b/tests/golden/test_dataflow/test_reverse_x_10.txt @@ -17,10 +17,7 @@ def foo(x : R[11]): - 3.0 - x[d0] - 3.0 - - ((i-1)-0) - - ⊥ - - x[d0] - - x[d0] + - x[d0] - 1.0 - ((10-(i-1))-d0) - (2*d0-10) @@ -46,20 +43,14 @@ def foo(x : R[11]): - 3.0 - 3.0 - x[d0] - - (d0-10) - - 3.0 - - 3.0 - - ⊥ + - 3.0 - ⊥ - 1.0 - ((10-(i-1))-d0) - (2*d0-9) - 3.0 - 3.0 - - (2*d0-10) - - 3.0 - - 1.0 - - 1.0 + - 1.0 - 3.0 - ⊥ - 3.0 @@ -67,10 +58,7 @@ def foo(x : R[11]): - ⊥ - x[d0] - ((i-1)-d0) - - ((i-1)-0) - - ⊥ - - x[d0] - - x[d0] + - x[d0] - 1.0 - 1.0 x_2 : \i. \d0 @@ -90,19 +78,13 @@ def foo(x : R[11]): - 3.0 - 3.0 - x[d0] - - (d0-10) - - 3.0 - - 3.0 - - ⊥ + - 3.0 - ⊥ - 3.0 - (i-0) - ⊥ - x[d0] - - ((i-1)-0) - - ⊥ - - x[d0] - - x[d0] + - x[d0] - 1.0 - ((10-i)-d0) - ((i-1)-d0) @@ -112,17 +94,11 @@ def foo(x : R[11]): - (2*d0-9) - 3.0 - 3.0 - - (2*d0-10) - - 3.0 - - 1.0 - - 1.0 + - 1.0 - 3.0 - ⊥ - 3.0 - - ((i-1)-d0) - - ⊥ - - 1.0 - - 1.0 + - 1.0 x_4 =\d0 \phi(10 > 0 ? x_2[10 - 1, d0] : x[d0]) # LoopExit ------------------------ x_1 : \i. \d0 - (i-0) @@ -138,10 +114,7 @@ def foo(x : R[11]): - 3.0 - x[d0] - 3.0 - - ((i-1)-0) - - ⊥ - - x[d0] - - x[d0] + - x[d0] - 1.0 - ((10-(i-1))-d0) - (2*d0-10) @@ -167,20 +140,14 @@ def foo(x : R[11]): - 3.0 - 3.0 - x[d0] - - (d0-10) - - 3.0 - - 3.0 - - ⊥ + - 3.0 - ⊥ - 1.0 - ((10-(i-1))-d0) - (2*d0-9) - 3.0 - 3.0 - - (2*d0-10) - - 3.0 - - 1.0 - - 1.0 + - 1.0 - 3.0 - ⊥ - 3.0 @@ -188,10 +155,7 @@ def foo(x : R[11]): - ⊥ - x[d0] - ((i-1)-d0) - - ((i-1)-0) - - ⊥ - - x[d0] - - x[d0] + - x[d0] - 1.0 - 1.0 x_2 : \i. \d0 @@ -211,19 +175,10 @@ def foo(x : R[11]): - 3.0 - 3.0 - x[d0] - - (d0-10) - - 3.0 - - 3.0 - - ⊥ + - 3.0 - ⊥ - 3.0 - - (i-0) - - ⊥ - - x[d0] - - ((i-1)-0) - - ⊥ - - x[d0] - - x[d0] + - x[d0] - 1.0 - ((10-i)-d0) - ((i-1)-d0) @@ -233,17 +188,11 @@ def foo(x : R[11]): - (2*d0-9) - 3.0 - 3.0 - - (2*d0-10) - - 3.0 - - 1.0 - - 1.0 + - 1.0 - 3.0 - ⊥ - 3.0 - - ((i-1)-d0) - - ⊥ - - 1.0 - - 1.0 + - 1.0 x_4 : \d0 - ((10-1)-d0) - (d0-10) @@ -259,10 +208,7 @@ def foo(x : R[11]): - (2*d0-9) - 3.0 - 3.0 - - (2*d0-10) - - 3.0 - - 1.0 - - 1.0 + - 1.0 - 3.0 - ⊥ - 3.0 diff --git a/tests/golden/test_dataflow/test_reverse_x_10_lo.txt b/tests/golden/test_dataflow/test_reverse_x_10_lo.txt index 65c44053..2d189af2 100644 --- a/tests/golden/test_dataflow/test_reverse_x_10_lo.txt +++ b/tests/golden/test_dataflow/test_reverse_x_10_lo.txt @@ -9,27 +9,21 @@ def foo(x : R[11]): - ((10-(i-1))-d0) - 3.0 - 3.0 - - (d0-2) - - ⊥ - - ⊥ - - ⊥ + - ⊥ - 1.0 - 1.0 - x[d0] - ((i-1)-d0) - ((10-(i-1))-d0) - ((i-1)-3) - - ⊤ + - ⊥ - x[d0] - (d0-7) - 3.0 - 3.0 - x[d0] - 3.0 - - ((i-1)-3) - - ⊤ - - x[d0] - - x[d0] + - x[d0] - 1.0 - ((10-(i-1))-d0) - (d0-2) @@ -41,27 +35,21 @@ def foo(x : R[11]): - 1.0 - 3.0 - ((i-1)-3) - - x[d0] + - ⊥ - x[d0] - (d0-2) - x[d0] - x[d0] - - (d0-3) - - x[d0] - - 1.0 - - 1.0 + - 1.0 x_3 : \i. \d0 - ((10-i)-d0) - (i-3) - - ((10-(i-1))-d0) - - 3.0 - - 3.0 - - ⊤ + - 3.0 - x[d0] - ((i-1)-d0) - ((10-(i-1))-d0) - ((i-1)-3) - - ⊤ + - ⊥ - x[d0] - (d0-6) - 3.0 @@ -71,7 +59,7 @@ def foo(x : R[11]): - 3.0 - x[d0] - 3.0 - - ⊤ + - ⊥ - 1.0 - ((10-(i-1))-d0) - (d0-2) @@ -80,19 +68,13 @@ def foo(x : R[11]): - (2*d0-9) - 3.0 - 3.0 - - (2*d0-10) - - 3.0 - - 1.0 - - 1.0 - - 3.0 + - 1.0 - 3.0 + - ⊥ - 3.0 - (i-3) - ((i-1)-d0) - - (d0-2) - - ⊥ - - ⊥ - - ⊥ + - ⊥ - 1.0 - 1.0 - x[d0] @@ -100,7 +82,7 @@ def foo(x : R[11]): - x[d0] - 1.0 - ((i-1)-3) - - x[d0] + - ⊥ - x[d0] - (d0-2) - x[d0] @@ -110,53 +92,44 @@ def foo(x : R[11]): - (i-d0) - ((10-i)-d0) - (i-3) - - ((10-(i-1))-d0) - - 3.0 - - 3.0 - - ⊤ + - 3.0 - x[d0] - ((10-(i-1))-d0) - ((i-1)-3) - - ⊤ + - ⊥ - x[d0] - (d0-7) - 3.0 - 3.0 - x[d0] - 3.0 - - ⊤ + - ⊥ - 3.0 - (i-3) - - (d0-3) - - ⊥ - - ⊥ - - ⊥ + - ⊥ - x[d0] - x[d0] - 1.0 - ((10-i)-d0) - ((i-1)-d0) - - ⊤ + - ⊥ - 1.0 - ((10-(i-1))-d0) - (2*d0-9) - 3.0 - 3.0 - - (2*d0-10) - - 3.0 - - 1.0 - - 1.0 - - 3.0 + - 1.0 - 3.0 + - ⊥ - 3.0 - (i-3) - 1.0 - x[d0] - ((i-1)-d0) - - ⊤ + - ⊥ - 1.0 - ((i-1)-3) - - x[d0] + - ⊥ - x[d0] - (d0-2) - x[d0] @@ -176,17 +149,14 @@ def foo(x : R[11]): - ((i-1)-d0) - ((10-(i-1))-d0) - ((i-1)-3) - - ⊤ + - ⊥ - x[d0] - (d0-7) - 3.0 - 3.0 - x[d0] - 3.0 - - ((i-1)-3) - - ⊤ - - x[d0] - - x[d0] + - x[d0] - 1.0 - ((10-(i-1))-d0) - (d0-2) @@ -198,27 +168,21 @@ def foo(x : R[11]): - 1.0 - 3.0 - ((i-1)-3) - - x[d0] + - ⊥ - x[d0] - (d0-2) - x[d0] - x[d0] - - (d0-3) - - x[d0] - - 1.0 - - 1.0 + - 1.0 x_3 : \i. \d0 - ((10-i)-d0) - (i-3) - - ((10-(i-1))-d0) - - 3.0 - - 3.0 - - ⊤ + - 3.0 - x[d0] - ((i-1)-d0) - ((10-(i-1))-d0) - ((i-1)-3) - - ⊤ + - ⊥ - x[d0] - (d0-6) - 3.0 @@ -228,7 +192,7 @@ def foo(x : R[11]): - 3.0 - x[d0] - 3.0 - - ⊤ + - ⊥ - 1.0 - ((10-(i-1))-d0) - (d0-2) @@ -237,12 +201,9 @@ def foo(x : R[11]): - (2*d0-9) - 3.0 - 3.0 - - (2*d0-10) - - 3.0 - - 1.0 - - 1.0 - - 3.0 + - 1.0 - 3.0 + - ⊥ - 3.0 - (i-3) - ((i-1)-d0) @@ -254,7 +215,7 @@ def foo(x : R[11]): - x[d0] - 1.0 - ((i-1)-3) - - x[d0] + - ⊥ - x[d0] - (d0-2) - x[d0] @@ -264,21 +225,18 @@ def foo(x : R[11]): - (i-d0) - ((10-i)-d0) - (i-3) - - ((10-(i-1))-d0) - - 3.0 - - 3.0 - - ⊤ + - 3.0 - x[d0] - ((10-(i-1))-d0) - ((i-1)-3) - - ⊤ + - ⊥ - x[d0] - (d0-7) - 3.0 - 3.0 - x[d0] - 3.0 - - ⊤ + - ⊥ - 3.0 - (i-3) - ⊥ @@ -287,27 +245,24 @@ def foo(x : R[11]): - 1.0 - ((10-i)-d0) - ((i-1)-d0) - - ⊤ + - ⊥ - 1.0 - ((10-(i-1))-d0) - (2*d0-9) - 3.0 - 3.0 - - (2*d0-10) - - 3.0 - - 1.0 - - 1.0 - - 3.0 + - 1.0 - 3.0 + - ⊥ - 3.0 - (i-3) - 1.0 - x[d0] - ((i-1)-d0) - - ⊤ + - ⊥ - 1.0 - ((i-1)-3) - - x[d0] + - ⊥ - x[d0] - (d0-2) - x[d0] @@ -319,17 +274,14 @@ def foo(x : R[11]): - 1.0 - ((10-(9-1))-d0) - (((9-1)-1)-d0) - - ⊤ + - ⊥ - 1.0 - ((10-((9-1)-1))-d0) - (2*d0-9) - 3.0 - 3.0 - - (2*d0-10) - - 3.0 - - 1.0 - - 1.0 - - 3.0 + - 1.0 - 3.0 + - ⊥ - 3.0 - x[d0] \ No newline at end of file diff --git a/tests/golden/test_dataflow/test_reverse_x_11.txt b/tests/golden/test_dataflow/test_reverse_x_11.txt index dd5f8e68..e97b5dac 100644 --- a/tests/golden/test_dataflow/test_reverse_x_11.txt +++ b/tests/golden/test_dataflow/test_reverse_x_11.txt @@ -17,10 +17,7 @@ def foo(x : R[11]): - 3.0 - x[d0] - 3.0 - - ((i-1)-0) - - ⊥ - - x[d0] - - x[d0] + - x[d0] - 1.0 - ((10-(i-1))-d0) - (2*d0-10) @@ -46,20 +43,14 @@ def foo(x : R[11]): - 3.0 - 3.0 - x[d0] - - (d0-10) - - 3.0 - - 3.0 - - ⊥ + - 3.0 - ⊥ - 1.0 - ((10-(i-1))-d0) - (2*d0-9) - 3.0 - 3.0 - - (2*d0-10) - - 3.0 - - 1.0 - - 1.0 + - 1.0 - 3.0 - ⊥ - 3.0 @@ -67,10 +58,7 @@ def foo(x : R[11]): - ⊥ - x[d0] - ((i-1)-d0) - - ((i-1)-0) - - ⊥ - - x[d0] - - x[d0] + - x[d0] - 1.0 - 1.0 x_2 : \i. \d0 @@ -90,19 +78,13 @@ def foo(x : R[11]): - 3.0 - 3.0 - x[d0] - - (d0-10) - - 3.0 - - 3.0 - - ⊥ + - 3.0 - ⊥ - 3.0 - (i-0) - ⊥ - x[d0] - - ((i-1)-0) - - ⊥ - - x[d0] - - x[d0] + - x[d0] - 1.0 - ((10-i)-d0) - ((i-1)-d0) @@ -112,17 +94,11 @@ def foo(x : R[11]): - (2*d0-9) - 3.0 - 3.0 - - (2*d0-10) - - 3.0 - - 1.0 - - 1.0 + - 1.0 - 3.0 - ⊥ - 3.0 - - ((i-1)-d0) - - ⊥ - - 1.0 - - 1.0 + - 1.0 x_4 =\d0 \phi(11 > 0 ? x_2[11 - 1, d0] : x[d0]) # LoopExit ------------------------ x_1 : \i. \d0 - (i-0) @@ -138,10 +114,7 @@ def foo(x : R[11]): - 3.0 - x[d0] - 3.0 - - ((i-1)-0) - - ⊥ - - x[d0] - - x[d0] + - x[d0] - 1.0 - ((10-(i-1))-d0) - (2*d0-10) @@ -167,20 +140,14 @@ def foo(x : R[11]): - 3.0 - 3.0 - x[d0] - - (d0-10) - - 3.0 - - 3.0 - - ⊥ + - 3.0 - ⊥ - 1.0 - ((10-(i-1))-d0) - (2*d0-9) - 3.0 - 3.0 - - (2*d0-10) - - 3.0 - - 1.0 - - 1.0 + - 1.0 - 3.0 - ⊥ - 3.0 @@ -188,10 +155,7 @@ def foo(x : R[11]): - ⊥ - x[d0] - ((i-1)-d0) - - ((i-1)-0) - - ⊥ - - x[d0] - - x[d0] + - x[d0] - 1.0 - 1.0 x_2 : \i. \d0 @@ -211,19 +175,10 @@ def foo(x : R[11]): - 3.0 - 3.0 - x[d0] - - (d0-10) - - 3.0 - - 3.0 - - ⊥ + - 3.0 - ⊥ - 3.0 - - (i-0) - - ⊥ - - x[d0] - - ((i-1)-0) - - ⊥ - - x[d0] - - x[d0] + - x[d0] - 1.0 - ((10-i)-d0) - ((i-1)-d0) @@ -233,17 +188,11 @@ def foo(x : R[11]): - (2*d0-9) - 3.0 - 3.0 - - (2*d0-10) - - 3.0 - - 1.0 - - 1.0 + - 1.0 - 3.0 - ⊥ - 3.0 - - ((i-1)-d0) - - ⊥ - - 1.0 - - 1.0 + - 1.0 x_4 : \d0 - ((11-1)-d0) - x[d0] @@ -256,11 +205,8 @@ def foo(x : R[11]): - (2*d0-9) - 3.0 - 3.0 - - (2*d0-10) - - 3.0 - - 1.0 - - 1.0 + - 1.0 - 3.0 - ⊥ - 3.0 - - ⊥ \ No newline at end of file + - 1.0 \ No newline at end of file diff --git a/tests/golden/test_dataflow/test_super_simple.txt b/tests/golden/test_dataflow/test_super_simple.txt index 3f0b7c03..48f0c2eb 100644 --- a/tests/golden/test_dataflow/test_super_simple.txt +++ b/tests/golden/test_dataflow/test_super_simple.txt @@ -7,95 +7,26 @@ def foo(x : f32[5]): - ⊥ - x[d0] - ((i-1)-d0) - - ((i-1)-0) - - (d0+1) - - ⊤ - - ⊤ - - d0 - - x[d0] - - x[d0] - - x[d0] - - (d0+1) - - ⊤ - - ⊤ - - d0 - - ⊤ - - ⊤ - - x[d0] - - (d0+1) - - ⊤ - - ⊤ - - d0 - - ⊤ - - ⊤ - - x[d0] - - (d0+1) - - ⊤ - - ⊤ - - 0.0 - - (d0+1) - - x[d0] - - x[d0] - - 0.0 + - x[d0] + - 0.0 + - 0.0 x_2 : \i. \d0 - (i-d0) - - (i-0) - - d0 - - ⊥ - - ⊥ - - ⊥ - - d0 - - ⊤ - - ⊤ - - x[d0] - - ((i-1)-0) - - d0 - - ⊤ - - ⊤ - - (d0-1) - - x[d0] - - x[d0] - - x[d0] - - d0 - - ⊤ - - ⊤ - - (d0-1) - - ⊤ - - ⊤ - - x[d0] - - d0 - - ⊤ - - ⊤ - - (d0-1) - - ⊤ - - ⊤ - - x[d0] + - x[d0] + - 0.0 - 0.0 - - ((i-1)-d0) - - 0.0 - - 0.0 - - 0.0 x_3 =\d0 \phi(5 > 0 ? x_2[5 - 1, d0] : x[d0]) # LoopExit ------------------------ x_1 : \i. \d0 - (i-0) - ⊥ - x[d0] - ((i-1)-d0) - - ((i-1)-0) - - ⊥ - - x[d0] - - x[d0] + - x[d0] - 0.0 - 0.0 x_2 : \i. \d0 - (i-d0) - - (i-0) - - ⊥ - - x[d0] - - ((i-1)-0) - - ⊥ - - x[d0] - - x[d0] + - x[d0] - 0.0 - 0.0 x_3 : \d0 diff --git a/tests/golden/test_dataflow/test_two_loops.txt b/tests/golden/test_dataflow/test_two_loops.txt index bd64c328..69965f26 100644 --- a/tests/golden/test_dataflow/test_two_loops.txt +++ b/tests/golden/test_dataflow/test_two_loops.txt @@ -7,74 +7,14 @@ def foo(x : f32[10]): - ⊥ - x[d0] - ((i-1)-d0) - - ((i-1)-0) - - (d0+1) - - ⊤ - - ⊤ - - d0 - - x[d0] - - x[d0] - - x[d0] - - (d0+1) - - ⊤ - - ⊤ - - d0 - - ⊤ - - ⊤ - - x[d0] - - (d0+1) - - ⊤ - - ⊤ - - d0 - - ⊤ - - ⊤ - - x[d0] - - (d0+1) - - ⊤ - - ⊤ - - 0.0 - - (d0+1) - - x[d0] - - x[d0] - - 0.0 + - x[d0] + - 0.0 + - 0.0 x_2 : \i. \d0 - (i-d0) - - (i-0) - - d0 - - ⊥ - - ⊥ - - ⊥ - - d0 - - ⊤ - - ⊤ - - x[d0] - - ((i-1)-0) - - d0 - - ⊤ - - ⊤ - - (d0-1) - - x[d0] - - x[d0] - - x[d0] - - d0 - - ⊤ - - ⊤ - - (d0-1) - - ⊤ - - ⊤ - - x[d0] - - d0 - - ⊤ - - ⊤ - - (d0-1) - - ⊤ - - ⊤ - - x[d0] + - x[d0] + - 0.0 - 0.0 - - ((i-1)-d0) - - 0.0 - - 0.0 - - 0.0 x_3 =\d0 \phi(10 > 0 ? x_2[10 - 1, d0] : x[d0]) # LoopExit for i_1 in seq(0, 10): x_4 =\i_1 \d0 \phi(i_1 == 0 ? x_3[d0] : x_5[i_1 - 1, d0]) # LoopStart @@ -84,21 +24,12 @@ def foo(x : f32[10]): - ⊥ - x[d0] - ((i-1)-d0) - - ((i-1)-0) - - ⊥ - - x[d0] - - x[d0] + - x[d0] - 0.0 - 0.0 x_2 : \i. \d0 - (i-d0) - - (i-0) - - ⊥ - - x[d0] - - ((i-1)-0) - - ⊥ - - x[d0] - - x[d0] + - x[d0] - 0.0 - 0.0 x_3 : \d0 @@ -110,204 +41,54 @@ def foo(x : f32[10]): - (i_1-0) - ⊥ - ((10-1)-d0) - - (9-d0) - - x[d0] - - ⊤ - - ⊤ - - (9-d0) - - ⊤ - - 0.0 - - ⊤ - - (9-d0) - - ⊤ - - ⊤ - - 0.0 + - x[d0] + - 0.0 + - 0.0 - ((i_1-1)-d0) - ((i_1-1)-0) - - (d0+1) - - ⊤ - - ⊤ - - d0 - - ((10-1)-d0) - - x[d0] - - 0.0 - - 0.0 - - ((10-1)-d0) - - x[d0] - - 0.0 - - 0.0 - - ((10-1)-d0) - - x[d0] - - 0.0 - - 0.0 + - ⊥ - ((10-1)-d0) - - (d0+1) - - ⊤ - - ⊤ - - d0 - - ⊤ - - ⊤ - - (9-d0) - - x[d0] - - ⊤ - - ⊤ - - (d0+1) - - ⊤ - - ⊤ - - d0 - - ⊤ - - ⊤ - - (9-d0) - - ⊤ - - 0.0 - - ⊤ - - (d0+1) - - ⊤ - - ⊤ - - d0 - - ⊤ - - ⊤ - - (9-d0) - - ⊤ - - ⊤ - - 0.0 - - (d0+1) - - ⊤ - - ⊤ - - d0 - - ⊤ - - ⊤ - - ((10-1)-d0) - - x[d0] - - 0.0 - - 0.0 - - (d0+1) - - ⊤ - - ⊤ - - 0.0 - - (d0+1) - - ((10-1)-d0) - - x[d0] - - 0.0 - - 0.0 - - ((10-1)-d0) - - x[d0] - - 0.0 - - 0.0 - - 0.0 + - x[d0] + - 0.0 + - 0.0 + - ((10-1)-d0) + - x[d0] + - 0.0 + - 0.0 + - 0.0 + - 0.0 x_5 : \i_1. \d0 - (i_1-d0) - (i_1-0) - - d0 - - ⊥ - - ⊥ - - ⊥ + - ⊥ - ((10-1)-d0) - - d0 - - ⊤ - - ⊤ - - (9-d0) - - x[d0] - - ⊤ - - ⊤ - - d0 - - ⊤ - - ⊤ - - (9-d0) - - ⊤ - - 0.0 - - ⊤ - - d0 - - ⊤ - - ⊤ - - (9-d0) - - ⊤ - - ⊤ - - 0.0 + - x[d0] + - 0.0 + - 0.0 - ((i_1-1)-0) - - d0 - - ⊤ - - ⊤ - - (d0-1) - - ((10-1)-d0) - - x[d0] - - 0.0 - - 0.0 - - ((10-1)-d0) - - x[d0] - - 0.0 - - 0.0 - - ((10-1)-d0) - - x[d0] - - 0.0 - - 0.0 + - ⊥ + - ((10-1)-d0) + - x[d0] + - 0.0 + - 0.0 - ((10-1)-d0) - - d0 - - ⊤ - - ⊤ - - (d0-1) - - ⊤ - - ⊤ - - (9-d0) - - x[d0] - - ⊤ - - ⊤ - - d0 - - ⊤ - - ⊤ - - (d0-1) - - ⊤ - - ⊤ - - (9-d0) - - ⊤ - - 0.0 - - ⊤ - - d0 - - ⊤ - - ⊤ - - (d0-1) - - ⊤ - - ⊤ - - (9-d0) - - ⊤ - - ⊤ - - 0.0 - - d0 - - ⊤ - - ⊤ - - (d0-1) - - ⊤ - - ⊤ - - ((10-1)-d0) - - x[d0] - - 0.0 - - 0.0 + - x[d0] + - 0.0 + - 0.0 + - 0.0 - 0.0 - - ((i_1-1)-d0) - - 0.0 - - 0.0 - - 0.0 x_6 =\d0 \phi(10 > 0 ? x_5[10 - 1, d0] : x_3[d0]) # LoopExit ------------------------ x_1 : \i. \d0 - (i-0) - ⊥ - x[d0] - ((i-1)-d0) - - ((i-1)-0) - - ⊥ - - x[d0] - - x[d0] + - x[d0] - 0.0 - 0.0 x_2 : \i. \d0 - (i-d0) - - (i-0) - - ⊥ - - x[d0] - - ((i-1)-0) - - ⊥ - - x[d0] - - x[d0] + - x[d0] - 0.0 - 0.0 x_3 : \d0