lib/algo/legacy/tests/heaps.viv

# Generated by tools/algo/check.py from lib/algo/algo.spec: do not edit.
# Each case prints its input (= X), its results, and the verdict of each postcondition
# (? ...) as lib/algo/props.viv computes it; check.py checks them again in Python.
from algo.cases import algo_case, CASE_NAMES
from algo.props import (
    algo_is_max_heap, algo_is_permutation, algo_is_sorted, algo_is_sorted_desc,
    algo_is_stable_values,
)
from algo.legacy.heaps import (
    build_max_heap, extract_max, heap_insert, heap_items, heap_new, heap_sort_in_place, heappop,
    heappush,
)

#| ta_build_max_heap: TheAlgorithms heap.py: build_max_heap
def algo_t_ta_build_max_heap(kind, n, inside, skip: Arr) -> Bool {
    X = algo_case(kind, n, 1 + 97 * kind + n)
    print("@ ta_build_max_heap", CASE_NAMES[kind], n)
    H = heap_new(len(X))
    build_max_heap(H, X)
    R = heap_items(H)
    print("= X", fmt(X))
    print("= R", fmt(R))
    p0 = algo_is_max_heap(R)
    p1 = algo_is_permutation(R, X)
    print("?", p0, p1)
    return inside == 0 or ((p0 or skip[0] == 1) and (p1 or skip[1] == 1))
}

#| ta_heap_insert: TheAlgorithms heap.py: insert one by one
def algo_t_ta_heap_insert(kind, n, inside, skip: Arr) -> Bool {
    X = algo_case(kind, n, 1 + 97 * kind + n)
    print("@ ta_heap_insert", CASE_NAMES[kind], n)
    H = heap_new(len(X))
    for i to len(X) {
        heap_insert(H, X[i])
    }
    R = heap_items(H)
    print("= X", fmt(X))
    print("= R", fmt(R))
    p0 = algo_is_max_heap(R)
    p1 = algo_is_permutation(R, X)
    print("?", p0, p1)
    return inside == 0 or ((p0 or skip[0] == 1) and (p1 or skip[1] == 1))
}

#| ta_extract_max: TheAlgorithms heap.py: build, then extract_max until empty
def algo_t_ta_extract_max(kind, n, inside, skip: Arr) -> Bool {
    X = algo_case(kind, n, 1 + 97 * kind + n)
    print("@ ta_extract_max", CASE_NAMES[kind], n)
    H = heap_new(len(X))
    build_max_heap(H, X)
    R = zeros(len(X))
    for i to len(X) {
        R[i] = extract_max(H)
    }
    print("= X", fmt(X))
    print("= R", fmt(R))
    p0 = algo_is_sorted_desc(R)
    p1 = algo_is_permutation(R, X)
    print("?", p0, p1)
    return inside == 0 or ((p0 or skip[0] == 1) and (p1 or skip[1] == 1))
}

#| ta_heap_sort_in_place: TheAlgorithms heap.py: heap_sort_in_place
def algo_t_ta_heap_sort_in_place(kind, n, inside, skip: Arr) -> Bool {
    X = algo_case(kind, n, 1 + 97 * kind + n)
    print("@ ta_heap_sort_in_place", CASE_NAMES[kind], n)
    H = heap_new(len(X))
    build_max_heap(H, X)
    heap_sort_in_place(H)
    R = heap_items(H)
    print("= X", fmt(X))
    print("= R", fmt(R))
    p0 = algo_is_permutation(R, X)
    p1 = algo_is_sorted(R)
    p2 = algo_is_stable_values(R, X)
    print("?", p0, p1, p2)
    return inside == 0 or ((p0 or skip[0] == 1) and (p1 or skip[1] == 1))
}

#| dijkstra_heap: the (cost, vertex) min-heap of TheAlgorithms' Dijkstra port
def algo_t_dijkstra_heap(kind, n, inside, skip: Arr) -> Bool {
    X = algo_case(kind, n, 1 + 97 * kind + n)
    print("@ dijkstra_heap", CASE_NAMES[kind], n)
    H = zeros(len(X) + 1, 2)
    size = 0
    for i to len(X) {
        size = heappush(H, size, X[i], i)
    }
    R = zeros(len(X))
    for i to len(X) {
        size = heappop(H, size)
        R[i] = H[size, 0]
    }
    print("= X", fmt(X))
    print("= R", fmt(R))
    p0 = algo_is_sorted(R)
    print("?", p0)
    return inside == 0 or ((p0 or skip[0] == 1))
}

algo_t_ok_ta_build_max_heap = true
algo_t_kinds_ta_build_max_heap = [0.0, 1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0, 9.0]
algo_t_inside_ta_build_max_heap = [1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 0.0]
algo_t_sizes_ta_build_max_heap = [0.0, 1.0, 2.0, 3.0, 4.0, 5.0, 7.0, 8.0, 9.0, 15.0, 16.0, 17.0, 31.0, 32.0, 33.0, 63.0, 64.0, 65.0, 129.0, 257.0]
algo_t_skip_ta_build_max_heap = [0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0]
for algo_t_k to len(algo_t_kinds_ta_build_max_heap) {
    for algo_t_s to len(algo_t_sizes_ta_build_max_heap) {
        algo_t_r = algo_t_ta_build_max_heap(algo_t_kinds_ta_build_max_heap[algo_t_k], algo_t_sizes_ta_build_max_heap[algo_t_s], algo_t_inside_ta_build_max_heap[algo_t_k], algo_t_skip_ta_build_max_heap[algo_t_k * 2:(algo_t_k + 1) * 2])
        algo_t_ok_ta_build_max_heap = algo_t_ok_ta_build_max_heap and algo_t_r
    }
}

algo_t_ok_ta_heap_insert = true
algo_t_kinds_ta_heap_insert = [0.0, 1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0, 9.0]
algo_t_inside_ta_heap_insert = [1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 0.0]
algo_t_sizes_ta_heap_insert = [0.0, 1.0, 2.0, 3.0, 4.0, 5.0, 7.0, 8.0, 9.0, 15.0, 16.0, 17.0, 31.0, 32.0, 33.0, 63.0, 64.0, 65.0, 129.0, 257.0]
algo_t_skip_ta_heap_insert = [0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0]
for algo_t_k to len(algo_t_kinds_ta_heap_insert) {
    for algo_t_s to len(algo_t_sizes_ta_heap_insert) {
        algo_t_r = algo_t_ta_heap_insert(algo_t_kinds_ta_heap_insert[algo_t_k], algo_t_sizes_ta_heap_insert[algo_t_s], algo_t_inside_ta_heap_insert[algo_t_k], algo_t_skip_ta_heap_insert[algo_t_k * 2:(algo_t_k + 1) * 2])
        algo_t_ok_ta_heap_insert = algo_t_ok_ta_heap_insert and algo_t_r
    }
}

algo_t_ok_ta_extract_max = true
algo_t_kinds_ta_extract_max = [0.0, 1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0, 9.0]
algo_t_inside_ta_extract_max = [1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 0.0]
algo_t_sizes_ta_extract_max = [0.0, 1.0, 2.0, 3.0, 4.0, 5.0, 7.0, 8.0, 9.0, 15.0, 16.0, 17.0, 31.0, 32.0, 33.0, 63.0, 64.0, 65.0, 129.0, 257.0]
algo_t_skip_ta_extract_max = [0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0]
for algo_t_k to len(algo_t_kinds_ta_extract_max) {
    for algo_t_s to len(algo_t_sizes_ta_extract_max) {
        algo_t_r = algo_t_ta_extract_max(algo_t_kinds_ta_extract_max[algo_t_k], algo_t_sizes_ta_extract_max[algo_t_s], algo_t_inside_ta_extract_max[algo_t_k], algo_t_skip_ta_extract_max[algo_t_k * 2:(algo_t_k + 1) * 2])
        algo_t_ok_ta_extract_max = algo_t_ok_ta_extract_max and algo_t_r
    }
}

algo_t_ok_ta_heap_sort_in_place = true
algo_t_kinds_ta_heap_sort_in_place = [0.0, 1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0, 9.0]
algo_t_inside_ta_heap_sort_in_place = [1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 0.0]
algo_t_sizes_ta_heap_sort_in_place = [0.0, 1.0, 2.0, 3.0, 4.0, 5.0, 7.0, 8.0, 9.0, 15.0, 16.0, 17.0, 31.0, 32.0, 33.0, 63.0, 64.0, 65.0, 129.0, 257.0]
algo_t_skip_ta_heap_sort_in_place = [0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0]
for algo_t_k to len(algo_t_kinds_ta_heap_sort_in_place) {
    for algo_t_s to len(algo_t_sizes_ta_heap_sort_in_place) {
        algo_t_r = algo_t_ta_heap_sort_in_place(algo_t_kinds_ta_heap_sort_in_place[algo_t_k], algo_t_sizes_ta_heap_sort_in_place[algo_t_s], algo_t_inside_ta_heap_sort_in_place[algo_t_k], algo_t_skip_ta_heap_sort_in_place[algo_t_k * 2:(algo_t_k + 1) * 2])
        algo_t_ok_ta_heap_sort_in_place = algo_t_ok_ta_heap_sort_in_place and algo_t_r
    }
}

algo_t_ok_dijkstra_heap = true
algo_t_kinds_dijkstra_heap = [0.0, 1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0, 9.0]
algo_t_inside_dijkstra_heap = [1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 0.0]
algo_t_sizes_dijkstra_heap = [0.0, 1.0, 2.0, 3.0, 4.0, 5.0, 7.0, 8.0, 9.0, 15.0, 16.0, 17.0, 31.0, 32.0, 33.0, 63.0, 64.0, 65.0, 129.0, 257.0]
algo_t_skip_dijkstra_heap = [0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0]
for algo_t_k to len(algo_t_kinds_dijkstra_heap) {
    for algo_t_s to len(algo_t_sizes_dijkstra_heap) {
        algo_t_r = algo_t_dijkstra_heap(algo_t_kinds_dijkstra_heap[algo_t_k], algo_t_sizes_dijkstra_heap[algo_t_s], algo_t_inside_dijkstra_heap[algo_t_k], algo_t_skip_dijkstra_heap[algo_t_k * 1:(algo_t_k + 1) * 1])
        algo_t_ok_dijkstra_heap = algo_t_ok_dijkstra_heap and algo_t_r
    }
}

test "ta_build_max_heap: max-heap R, permutation R X (kinds random dups sorted reversed equal organ sawtooth nearly zeros)" {
    assert_true(algo_t_ok_ta_build_max_heap)
}

test "ta_heap_insert: max-heap R, permutation R X (kinds random dups sorted reversed equal organ sawtooth nearly zeros)" {
    assert_true(algo_t_ok_ta_heap_insert)
}

test "ta_extract_max: ordered-desc R, permutation R X (kinds random dups sorted reversed equal organ sawtooth nearly zeros)" {
    assert_true(algo_t_ok_ta_extract_max)
}

test "ta_heap_sort_in_place: permutation R X, ordered R (kinds random dups sorted reversed equal organ sawtooth nearly zeros)" {
    assert_true(algo_t_ok_ta_heap_sort_in_place)
}

test "dijkstra_heap: ordered R (kinds random dups sorted reversed equal organ sawtooth nearly zeros)" {
    assert_true(algo_t_ok_dijkstra_heap)
}