lib/algo/legacy/tests/bench_qsort.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_permutation, algo_is_sorted, algo_is_sorted_answer, algo_is_stable_values,
)
from algo.legacy.bench_qsort import issorted, qsort

#| bench_qsort: the Julia microbenchmark's quicksort (middle element as pivot)
def algo_t_bench_qsort(kind, n, inside, skip: Arr) -> Bool {
    X = algo_case(kind, n, 1 + 97 * kind + n)
    print("@ bench_qsort", CASE_NAMES[kind], n)
    R = copy(X)
    if len(R) > 0 {
        qsort(R, 0, len(R) - 1)
    }
    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))
}

#| bench_issorted: the Julia microbenchmark's issorted
def algo_t_bench_issorted(kind, n, inside, skip: Arr) -> Bool {
    X = algo_case(kind, n, 1 + 97 * kind + n)
    print("@ bench_issorted", CASE_NAMES[kind], n)
    F = issorted(X)
    print("= X", fmt(X))
    print("= F", F)
    p0 = algo_is_sorted_answer(F, X)
    print("?", p0)
    return inside == 0 or ((p0 or skip[0] == 1))
}

algo_t_ok_bench_qsort = true
algo_t_kinds_bench_qsort = [0.0, 1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0, 9.0]
algo_t_inside_bench_qsort = [1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 0.0]
algo_t_sizes_bench_qsort = [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_bench_qsort = [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_bench_qsort) {
    for algo_t_s to len(algo_t_sizes_bench_qsort) {
        algo_t_r = algo_t_bench_qsort(algo_t_kinds_bench_qsort[algo_t_k], algo_t_sizes_bench_qsort[algo_t_s], algo_t_inside_bench_qsort[algo_t_k], algo_t_skip_bench_qsort[algo_t_k * 2:(algo_t_k + 1) * 2])
        algo_t_ok_bench_qsort = algo_t_ok_bench_qsort and algo_t_r
    }
}

algo_t_ok_bench_issorted = true
algo_t_kinds_bench_issorted = [0.0, 1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0, 9.0]
algo_t_inside_bench_issorted = [1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 0.0]
algo_t_sizes_bench_issorted = [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_bench_issorted = [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_bench_issorted) {
    for algo_t_s to len(algo_t_sizes_bench_issorted) {
        algo_t_r = algo_t_bench_issorted(algo_t_kinds_bench_issorted[algo_t_k], algo_t_sizes_bench_issorted[algo_t_s], algo_t_inside_bench_issorted[algo_t_k], algo_t_skip_bench_issorted[algo_t_k * 1:(algo_t_k + 1) * 1])
        algo_t_ok_bench_issorted = algo_t_ok_bench_issorted and algo_t_r
    }
}

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

test "bench_issorted: is-sorted-answer F X (kinds random dups sorted reversed equal organ sawtooth nearly zeros)" {
    assert_true(algo_t_ok_bench_issorted)
}