<jupyter_start><jupyter_text>Step 1: represent loop entry, AND backedge together as one map that can be accelerated / transitive closuredWe are interested in the program```cvoid loop_1d_const() {   for(int i = 0; i < 10; i += 2) {}}```<jupyter_code>def power1d():
    m0 = isl.Map("[k] -> { [i, count] -> [i+2, count + 1]}")
    # m = m.product(i)
    print("m x i: %s"  % m0)
    m = m0.transitive_closure()[0]
    print("m after trans: %s"% m)

    delta = m.deltas()
    print("delta: %s" % delta)
    # p0 = count
    c = Constraint.alloc_equality(isl.LocalSpace.from_space(delta.get_space()))
    c = c.set_coefficient_val(dim_type.param, 0, 1)
    c = c.set_coefficient_val(dim_type.set, 1, -1)
    print("c: %s" % c)
    delta = delta.add_constraint(c)
    print("delta after constraint: %s" % delta)
    delta = delta.project_out(dim_type.set, 1, 1)
    print("delta after projection: %s" % delta)
    return delta
    
    
m = power1d()
print("FINAL: %s" % m)<jupyter_output>m x i: [k] -> { [i, count] -> [2 + i, 1 + count] }
m after trans: [k] -> { [i, count] -> [o0, o1] : 2o1 = -i + 2count + o0 and o0 >= 2 + i }
delta: [k] -> { [i, count] : 2count = i and i >= 2 }
c: [k] -> { [i, count] : k - count = 0 }
delta after constraint: [k] -> { [i = 2k, count = k] : k > 0 }
delta after projection: [k] -> { [i = 2k] : k > 0 }
FINAL: [k] -> { [i = 2k] : k > 0 }<jupyter_text>Step 1.5: simple 2d loop with inner loop independent of outer loop```cvoid loop_1d_const() {   for(int i = 0; i < 10; i += 2) {       for(int j = 0; j < 10; j += 2) {        }   }}```<jupyter_code>def power2d_simple_1():
    # increment i once j has stopped incrementing
    deltai =  "[i, ci, j, cj] -> [i+2, ci+1, 0, 0] : ci >= 0 and cj >= 0 and i < 10 and j >= 10"
    # increment j as long as constraints are satisfied
    deltaj = "[i, ci, j, cj] -> [i, ci, j+2, cj+1] : ci >= 0 and cj >= 0 and j < 10"
    m0 = isl.Map("[k, l] -> {" + deltai + ";" + deltaj +  "}")
    print("m0: %s" % m0)
    (m, exact) = m0.transitive_closure()
    print("m after trans: %s"% m)
    print("EXACT?: %s" % exact)
    assert(exact == 1)

    delta = m.deltas()
    print("delta: %s" % delta)
    # p0 = count
    c = Constraint.alloc_equality(isl.LocalSpace.from_space(delta.get_space()))
    # k - ci = 0
    c = c.set_coefficient_val(dim_type.param, 0, 1)
    c = c.set_coefficient_val(dim_type.set, 1, -1)
    # l - cj = 0
    c = c.set_coefficient_val(dim_type.param, 1, 1)
    c = c.set_coefficient_val(dim_type.set, 3, -1)

    print("\n\nc: %s" % c)
    delta = delta.add_constraint(c)
    print("delta after constraint: %s" % delta)
    # project out ci
    delta = delta.project_out(dim_type.set, 1, 1)
    # project out cj
    delta = delta.project_out(dim_type.set, 2, 1)

    print("delta after projection: %s" % delta)
    return delta
    
# alternative encoding
def power2d_simple_2():
    # increment i once j has stopped incrementing
    deltai =  "[i, ci, j, -1] -> [i+2, ci+1, j, 0] : ci >= 0 and i < 10"
    # increment j as long as constraints are satisfied
    deltaj = "[i, ci, j, cj] -> [i, ci, j+2, cj+1] : ci >= 0 and cj >= 0 and j < 10"
    # reset counter of j
    jcounter = "[i, ci, j, cj] -> [i, ci, 0, (-1)] : ci >= 0 and cj >= 0 and j >= 10"
    m0 = isl.Map("[k, l] -> {" + deltai + ";" + deltaj + ";" + jcounter + ";" +  "}")
    print("m0: %s" % m0)
    (m, exact) = m0.transitive_closure()
    print("m after trans: %s"% m)
    print("EXACT?: %s" % exact)
    assert(exact == 1)

    delta = m.deltas()
    print("delta: %s" % delta)
    # p0 = count
    c = Constraint.alloc_equality(isl.LocalSpace.from_space(delta.get_space()))
    # k - ci = 0
    c = c.set_coefficient_val(dim_type.param, 0, 1)
    c = c.set_coefficient_val(dim_type.set, 1, -1)
    # l - cj = 0
    c = c.set_coefficient_val(dim_type.param, 1, 1)
    c = c.set_coefficient_val(dim_type.set, 3, -1)

    print("\n\nc: %s" % c)
    delta = delta.add_constraint(c)
    print("delta after constraint: %s" % delta)
    # project out ci
    delta = delta.project_out(dim_type.set, 1, 1)
    # project out cj
    delta = delta.project_out(dim_type.set, 2, 1)

    print("delta after projection: %s" % delta)
    return delta
    
print("## Simple 1 ## ")    
m = power2d_simple_1()
print("FINAL: %s" % m)


print("## Simple 2 ## ")
m = power2d_simple_2()
print("FINAL: %s" % m)<jupyter_output>## Simple 1 ## 
m0: [k, l] -> { [i, ci, j, cj] -> [i, ci, 2 + j, 1 + cj] : ci >= 0 and j <= 9 and cj >= 0; [i, ci, j, cj] -> [2 + i, 1 + ci, 0, 0] : i <= 9 and ci >= 0 and j >= 10 and cj >= 0 }
m after trans: [k, l] -> { [i, ci, j, cj] -> [o0, o1, o2, o3] : 2o1 = -i + 2ci + o0 and 2o3 = o2 and ci >= 0 and cj >= 0 and 2 + i <= o0 <= 11 and o2 >= 0 and ((j >= 10 and o2 <= -5i + 2cj + 5o0 and o2 <= 11 and o2 <= j) or (j <= 9 and 2*floor((1 + j)/2) >= -10 + j + o2)); [i, ci, j, cj] -> [i, ci, o2, o3] : 2o3 = -j + 2cj + o2 and ci >= 0 and cj >= 0 and 2 + j <= o2 <= 11 }
EXACT?: 1
delta: [k, l] -> { [i, ci, j, cj] : 2ci = i and i >= 2 and cj <= 5 and (j <= 0 or (j >= -9 and 2cj <= 9 + j)); [i = 0, ci = 0, j, cj] : 2cj = j and j >= 2 }


c: [k, l] -> { [i, ci, j, cj] : k + l - ci - cj = 0 }
delta after constraint: [k, l] -> { [i, ci, j, cj] : 2ci = i and 2cj = 2k + 2l - i and i >= -10 + 2k + 2l and i >= 2 and (j <= 0 or (j >= -9 + 2k + 2l - i and j >= -9)); [i = 0, ci = 0, j = 2k + 2l, cj = k[...]<jupyter_text>Step 2: represent a nested loop as one map that can be poweredWe are interested in the program```cvoid loop_1d_const() {   for(int i = 0; i < 10; i += 2) {       for(int j = 0; j < i; j += 2) {        }   }}```<jupyter_code>def power2d_complex_1():
    # increment i once j has stopped incrementing
    deltai =  "[i, ci, j, cj] -> [i+2, ci+1, 0, 0] : ci >= 0 and cj >= 0 and i < 10 and j >= i"
    # increment j as long as constraints are satisfied
    deltaj = "[i, ci, j, cj] -> [i, ci, j+2, cj+1] : ci >= 0 and cj >= 0 and j < i"
    m0 = isl.Map("[k, l] -> {" + deltai + ";" + deltaj + "}")
    print("m0: %s" % m0)
    (m, exact) = m0.transitive_closure()
    print("m after trans: %s"% m)
    print("EXACT?: %s" % exact)
    assert(exact == 1)

    delta = m.deltas()
    print("delta: %s" % delta)
    # p0 = count
    c = Constraint.alloc_equality(isl.LocalSpace.from_space(delta.get_space()))
    # k - ci = 0
    c = c.set_coefficient_val(dim_type.param, 0, 1)
    c = c.set_coefficient_val(dim_type.set, 1, -1)
    # l - cj = 0
    c = c.set_coefficient_val(dim_type.param, 1, 1)
    c = c.set_coefficient_val(dim_type.set, 3, -1)

    print("\n\nc: %s" % c)
    delta = delta.add_constraint(c)
    print("delta after constraint: %s" % delta)
    # project out ci
    delta = delta.project_out(dim_type.set, 1, 1)
    # project out cj
    delta = delta.project_out(dim_type.set, 2, 1)

    print("delta after projection: %s" % delta)
    return delta
    
    
m = power2d_complex_1()
print("FINAL: %s" % m)<jupyter_output>m0: [k, l] -> { [i, ci, j, cj] -> [i, ci, 2 + j, 1 + cj] : ci >= 0 and j < i and cj >= 0; [i, ci, j, cj] -> [2 + i, 1 + ci, 0, 0] : i <= 9 and ci >= 0 and j >= i and cj >= 0 }
m after trans: [k, l] -> { [i, ci, j, cj] -> [o0, o1, o2, o3] : 2o1 = -i + 2ci + o0 and ci >= 0 and cj >= 0 and o0 >= 2 + i and o2 <= 1 + o0 and o3 > 0 and (j < i or (i <= 9 and j >= i)); [i, ci, j, cj] -> [o0, o1, 0, 0] : 2o1 = -i + 2ci + o0 and ci >= 0 and cj >= 0 and 2 + i <= o0 <= 11 and (j < i or j >= i); [i, ci, j, cj] -> [i, ci, o2, o3] : 2o3 = -j + 2cj + o2 and ci >= 0 and cj >= 0 and 2 + j <= o2 <= 1 + i }
EXACT?: 0
{'fraction_non_alphanumeric': 0.19691735317565773, 'fraction_numerical': 0.044246611745947385, 'mean_word_length': 2.538787023977433, 'pattern_counts': {'":': 0, '<': 45, '<?xml version=': 0, '>': 102, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'chain_length': '3', 'dir': 'jupyter-structured-clean-dedup', 'id': '297192', 'license': 'BSD-3-Clause', 'n_tokens_mistral': 3424, 'n_tokens_neox': 3186, 'n_words': 1028, 'path': 'notebooks/accel-many-loops.ipynb', 'repo_name': 'bollu/absint', 'size': '7526'}