Merge branch 'benchmark-knights'
This commit is contained in:
KtorZ
commit
61a991cb23
|
|
@ -14,6 +14,10 @@ jobs:
|
||||||
runs-on: ubuntu-latest
|
runs-on: ubuntu-latest
|
||||||
steps:
|
steps:
|
||||||
- uses: actions/checkout@v4
|
- uses: actions/checkout@v4
|
||||||
|
- uses: Swatinem/rust-cache@v2
|
||||||
|
with:
|
||||||
|
save-if: ${{ github.ref == 'refs/heads/main' }}
|
||||||
|
key: ${{ runner.os }}-cache-build-v${{ inputs.cache-version }}
|
||||||
- name: Run examples
|
- name: Run examples
|
||||||
run: |
|
run: |
|
||||||
cargo run -r -- check examples/hello_world
|
cargo run -r -- check examples/hello_world
|
||||||
|
|
@ -29,13 +33,33 @@ jobs:
|
||||||
runs-on: ubuntu-latest
|
runs-on: ubuntu-latest
|
||||||
steps:
|
steps:
|
||||||
- uses: actions/checkout@v4
|
- uses: actions/checkout@v4
|
||||||
|
- uses: Swatinem/rust-cache@v2
|
||||||
|
with:
|
||||||
|
save-if: ${{ github.ref == 'refs/heads/main' }}
|
||||||
|
key: ${{ runner.os }}-cache-tests-v${{ inputs.cache-version }}
|
||||||
- name: Run unit tests
|
- name: Run unit tests
|
||||||
run: cargo test --verbose --workspace
|
run: cargo test --verbose --workspace
|
||||||
|
|
||||||
|
benchmarks:
|
||||||
|
runs-on: ubuntu-latest
|
||||||
|
steps:
|
||||||
|
- uses: actions/checkout@v4
|
||||||
|
- uses: Swatinem/rust-cache@v2
|
||||||
|
with:
|
||||||
|
save-if: ${{ github.ref == 'refs/heads/main' }}
|
||||||
|
key: ${{ runner.os }}-cache-build-v${{ inputs.cache-version }}
|
||||||
|
- name: Run benchmarks
|
||||||
|
run: |
|
||||||
|
cargo run -r -- check benchmarks
|
||||||
|
|
||||||
checks:
|
checks:
|
||||||
runs-on: ubuntu-latest
|
runs-on: ubuntu-latest
|
||||||
steps:
|
steps:
|
||||||
- uses: actions/checkout@v4
|
- uses: actions/checkout@v4
|
||||||
|
- uses: Swatinem/rust-cache@v2
|
||||||
|
with:
|
||||||
|
save-if: ${{ github.ref == 'refs/heads/main' }}
|
||||||
|
key: ${{ runner.os }}-cache-unit-v${{ inputs.cache-version }}
|
||||||
- name: Format
|
- name: Format
|
||||||
run: cargo fmt --all -- --check
|
run: cargo fmt --all -- --check
|
||||||
- name: Clippy
|
- name: Clippy
|
||||||
|
|
|
||||||
|
|
@ -0,0 +1,6 @@
|
||||||
|
# Aiken compilation artifacts
|
||||||
|
artifacts/
|
||||||
|
# Aiken's project working directory
|
||||||
|
build/
|
||||||
|
# Aiken's default documentation export
|
||||||
|
docs/
|
||||||
|
|
@ -0,0 +1,153 @@
|
||||||
|
# (No Fib) Benchmarks
|
||||||
|
|
||||||
|
This folder contains a set of benchmarks inspired and ported from the [plutus-benchmarks](https://github.com/IntersectMBO/plutus/tree/master/plutus-benchmark/nofib#plutus-nofib-benchmarks), written in Haskell. The idea is to provide benchmarks which can capture more realistic patterns and behaviours than usual "Fibonacci" benchmarks often used for benchmarking applications but falling short in capturing real-world scenarios.
|
||||||
|
|
||||||
|
Note that the primary use-case of those benchmarks is to compare Aiken with itself across compiler versions. As optimizations get implemented, it comes as a supplimentary means to assess their impact.
|
||||||
|
|
||||||
|
## Summary
|
||||||
|
|
||||||
|
Results are summarized below, relatively to the previous version. For brevity, we only report versions for which there's a deviation from a previous version.
|
||||||
|
|
||||||
|
<!--
|
||||||
|
Plutus-Tx
|
||||||
|
|
||||||
|
Script Size CPU budget Memory budget
|
||||||
|
-----------------------------------------------------------------
|
||||||
|
clausify/F1 1573 3316814452 19803348
|
||||||
|
clausify/F2 1573 4329805760 25708376
|
||||||
|
clausify/F3 1573 11847889335 70086982
|
||||||
|
clausify/F4 1573 26924400260 152296076
|
||||||
|
clausify/F5 1573 57792275160 340971480
|
||||||
|
knights/4x4 2049 16660243968 86107706
|
||||||
|
knights/6x6 2049 49595956778 271079788
|
||||||
|
knights/8x8 2049 89757683708 495426680
|
||||||
|
primes/05digits 1501 9617902676 37194205
|
||||||
|
primes/08digits 1501 15888515320 60723255
|
||||||
|
primes/10digits 1501 18980946392 71916641
|
||||||
|
primes/20digits 1501 36493682732 137260387
|
||||||
|
primes/30digits 1501 57224069574 214186802
|
||||||
|
primes/40digits 1501 75870264649 282727215
|
||||||
|
primes/50digits 1501 93666987132 345920797
|
||||||
|
queens4x4/bt 1867 5135006267 28184130
|
||||||
|
queens4x4/bm 1867 6345082859 35502236
|
||||||
|
queens4x4/bjbt1 1867 6252769293 34895616
|
||||||
|
queens4x4/bjbt2 1867 5820721293 32195316
|
||||||
|
queens4x4/fc 1867 13740412571 78668768
|
||||||
|
queens5x5/bt 1867 71081240426 381100320
|
||||||
|
queens5x5/bm 1867 71574838831 400366576
|
||||||
|
queens5x5/bjbt1 1867 82536005114 449984088
|
||||||
|
queens5x5/bjbt2 1867 79887717114 433432288
|
||||||
|
queens5x5/fc 1867 179227518621 1023295666
|
||||||
|
-->
|
||||||
|
|
||||||
|
<!--
|
||||||
|
v1.0.29-alpha & v1.0.28-alpha
|
||||||
|
|
||||||
|
┍━ benchmarks/clausify/benchmark ━━━━━━━━━━━━━━━━━━━━━━━━━━━
|
||||||
|
│ PASS [mem: 53769377, cpu: 21594809455] bench_clausify_f1
|
||||||
|
│ PASS [mem: 67108683, cpu: 26864755594] bench_clausify_f2
|
||||||
|
│ PASS [mem: 179606857, cpu: 71814854199] bench_clausify_f3
|
||||||
|
│ PASS [mem: 231444137, cpu: 93024749730] bench_clausify_f4
|
||||||
|
│ PASS [mem: 874286879, cpu: 349894049008] bench_clausify_f5
|
||||||
|
┕━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ 5 tests | 5 passed | 0 failed
|
||||||
|
|
||||||
|
┍━ benchmarks/knights ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
|
||||||
|
│ PASS [mem: 172256715, cpu: 71851995726] bench_knights_100_4x4
|
||||||
|
│ PASS [mem: 321712271, cpu: 159767368294] bench_knights_100_6x6
|
||||||
|
│ PASS [mem: 601065675, cpu: 319834775948] bench_knights_100_8x8
|
||||||
|
┕━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ 3 tests | 3 passed | 0 failed
|
||||||
|
|
||||||
|
==== There's no 1.0.27-alpha
|
||||||
|
|
||||||
|
v1.0.26-alpha & V1.0.25-alpha
|
||||||
|
|
||||||
|
┍━ benchmarks/clausify/benchmark ━━━━━━━━━━━━━━━━━━━━━━━━━━━
|
||||||
|
│ PASS [mem: 52538257, cpu: 20243486892] bench_clausify_f1
|
||||||
|
│ PASS [mem: 65404263, cpu: 25235091975] bench_clausify_f2
|
||||||
|
│ PASS [mem: 174866054, cpu: 67523028814] bench_clausify_f3
|
||||||
|
│ PASS [mem: 225087758, cpu: 88367835856] bench_clausify_f4
|
||||||
|
│ PASS [mem: 851294369, cpu: 328896952793] bench_clausify_f5
|
||||||
|
┕━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ 5 tests | 5 passed | 0 failed
|
||||||
|
|
||||||
|
┍━ benchmarks/knights ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
|
||||||
|
│ PASS [mem: 171421863, cpu: 72861467671] bench_knights_100_4x4
|
||||||
|
│ PASS [mem: 354137347, cpu: 174027736310] bench_knights_100_6x6
|
||||||
|
│ PASS [mem: 688090183, cpu: 356296429240] bench_knights_100_8x8
|
||||||
|
┕━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ 3 tests | 3 passed | 0 failed
|
||||||
|
|
||||||
|
v1.0.24-alpha & V1.0.23-alpha
|
||||||
|
|
||||||
|
┍━ benchmarks/clausify/benchmark ━━━━━━━━━━━━━━━━━━━━━━━━━━━━
|
||||||
|
│ PASS [mem: 64738801, cpu: 24123180244] bench_clausify_f1
|
||||||
|
│ PASS [mem: 80280627, cpu: 29901360387] bench_clausify_f2
|
||||||
|
│ PASS [mem: 214423277, cpu: 79840016473] bench_clausify_f3
|
||||||
|
│ PASS [mem: 269232481, cpu: 101739948515] bench_clausify_f4
|
||||||
|
│ PASS [mem: 1045036759, cpu: 389233562263] bench_clausify_f5
|
||||||
|
┕━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ 5 tests | 5 passed | 0 failed
|
||||||
|
|
||||||
|
┍━ benchmarks/knights ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
|
||||||
|
│ PASS [mem: 180946463, cpu: 75052125671] bench_knights_100_4x4
|
||||||
|
│ PASS [mem: 374910247, cpu: 178805503310] bench_knights_100_6x6
|
||||||
|
│ PASS [mem: 729107683, cpu: 365730454240] bench_knights_100_8x8
|
||||||
|
┕━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ 3 tests | 3 passed | 0 failed
|
||||||
|
|
||||||
|
==== There's no 1.0.22-alpha
|
||||||
|
|
||||||
|
V1.0.21-alpha
|
||||||
|
|
||||||
|
┍━ benchmarks/clausify/benchmark ━━━━━━━━━━━━━━━━━━━━━━━━━━━━
|
||||||
|
│ PASS [mem: 64738801, cpu: 24123180244] bench_clausify_f1
|
||||||
|
│ PASS [mem: 80280627, cpu: 29901360387] bench_clausify_f2
|
||||||
|
│ PASS [mem: 214423277, cpu: 79840016473] bench_clausify_f3
|
||||||
|
│ PASS [mem: 269232481, cpu: 101739948515] bench_clausify_f4
|
||||||
|
│ PASS [mem: 1045036759, cpu: 389233562263] bench_clausify_f5
|
||||||
|
┕━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ 5 tests | 5 passed | 0 failed
|
||||||
|
|
||||||
|
┍━ benchmarks/knights ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
|
||||||
|
│ PASS [mem: 180697463, cpu: 74944457471] bench_knights_100_4x4
|
||||||
|
│ PASS [mem: 374661247, cpu: 178697835110] bench_knights_100_6x6
|
||||||
|
│ PASS [mem: 728858683, cpu: 365622786040] bench_knights_100_8x8
|
||||||
|
┕━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ 3 tests | 3 passed | 0 failed
|
||||||
|
|
||||||
|
V1.0.20-alpha, v1.0.19-alpha & v1.0.18-alpha
|
||||||
|
|
||||||
|
┍━ benchmarks/clausify/benchmark ━━━━━━━━━━━━━━━━━━━━━━━━━━━━
|
||||||
|
│ PASS [mem: 64861501, cpu: 24151401244] bench_clausify_f1
|
||||||
|
│ PASS [mem: 80442927, cpu: 29938689387] bench_clausify_f2
|
||||||
|
│ PASS [mem: 214833977, cpu: 79934477473] bench_clausify_f3
|
||||||
|
│ PASS [mem: 269959981, cpu: 101907273515] bench_clausify_f4
|
||||||
|
│ PASS [mem: 1046684059, cpu: 389612441263] bench_clausify_f5
|
||||||
|
┕━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ 5 tests | 5 passed | 0 failed
|
||||||
|
|
||||||
|
┍━ benchmarks/knights ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
|
||||||
|
│ PASS [mem: 182244075, cpu: 75300076471] bench_knights_100_4x4
|
||||||
|
│ PASS [mem: 380548699, cpu: 180051720110] bench_knights_100_6x6
|
||||||
|
│ PASS [mem: 740194031, cpu: 368229509040] bench_knights_100_8x8
|
||||||
|
┕━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ 3 tests | 3 passed | 0 failed
|
||||||
|
-->
|
||||||
|
|
||||||
|
### CPU
|
||||||
|
|
||||||
|
| Benchmark | `v1.0.29` | vs `v1.0.25` | vs `v1.0.23` | vs `v1.0.21` | vs `v1.0.18` |
|
||||||
|
| --- | ---: | ---: | ---: | ---: | ---: |
|
||||||
|
| `clausify_f1` | 21594809455 | -6.26% | +11.71% | +11.71% | +11.84% |
|
||||||
|
| `clausify_f2` | 26864755594 | -6.07% | +11.30% | +11.30% | +11.44% |
|
||||||
|
| `clausify_f3` | 71814854199 | -5.98% | +11.17% | +11.17% | +11.31% |
|
||||||
|
| `clausify_f4` | 93024749730 | -5.01% | +9.37% | +9.37% | +9.55% |
|
||||||
|
| `clausify_f5` | 349894049008 | -6.00% | +11.24% | +11.24% | +11.35% |
|
||||||
|
| `knights_100_4x4` | 71851995726 | +1.40% | +4.45% | +4.30% | +4.80% |
|
||||||
|
| `knights_100_6x6` | 159767368294 | +8.93% | +11.92% | +11.85% | +12.70% |
|
||||||
|
| `knights_100_8x8` | 319834775948 | +11.40% | +14.35% | +14.32% | +15.13% |
|
||||||
|
|
||||||
|
### Mem
|
||||||
|
|
||||||
|
| Benchmark | `v1.0.29` | vs `v1.0.25` | vs `v1.0.23` | vs `v1.0.21` | vs `v1.0.18` |
|
||||||
|
| --- | ---: | ---: | ---: | ---: | ---: |
|
||||||
|
| `clausify_f1` | 53769377 | -2.29% | +20.40% | +20.40% | +20.63% |
|
||||||
|
| `clausify_f2` | 67108683 | -2.54% | +19.63% | +19.63% | +19.87% |
|
||||||
|
| `clausify_f3` | 179606857 | -2.64% | +19.38% | +19.38% | +19.61% |
|
||||||
|
| `clausify_f4` | 231444137 | -2.75% | +16.33% | +16.33% | +16.64% |
|
||||||
|
| `clausify_f5` | 874286879 | -2.63% | +19.53% | +19.53% | +19.72% |
|
||||||
|
| `knights_100_4x4` | 172256715 | -0.48% | +5.04% | +4.90% | +5.80% |
|
||||||
|
| `knights_100_6x6` | 321712271 | +10.08% | +16.54% | +16.46% | +18.29% |
|
||||||
|
| `knights_100_8x8` | 601065675 | +14.48% | +21.30% | +21.26% | +23.15% |
|
||||||
|
|
@ -0,0 +1,15 @@
|
||||||
|
# This file was generated by Aiken
|
||||||
|
# You typically do not need to edit this file
|
||||||
|
|
||||||
|
[[requirements]]
|
||||||
|
name = "aiken-lang/stdlib"
|
||||||
|
version = "1.9.0"
|
||||||
|
source = "github"
|
||||||
|
|
||||||
|
[[packages]]
|
||||||
|
name = "aiken-lang/stdlib"
|
||||||
|
version = "1.9.0"
|
||||||
|
requirements = []
|
||||||
|
source = "github"
|
||||||
|
|
||||||
|
[etags]
|
||||||
|
|
@ -0,0 +1,14 @@
|
||||||
|
name = "aiken/benchmarks"
|
||||||
|
version = "0.0.0"
|
||||||
|
license = "Apache-2.0"
|
||||||
|
description = "Aiken contracts for project 'aiken/benchmarks'"
|
||||||
|
|
||||||
|
[repository]
|
||||||
|
user = "aiken"
|
||||||
|
project = "benchmarks"
|
||||||
|
platform = "github"
|
||||||
|
|
||||||
|
[[dependencies]]
|
||||||
|
name = "aiken-lang/stdlib"
|
||||||
|
version = "1.9.0"
|
||||||
|
source = "github"
|
||||||
|
|
@ -0,0 +1,304 @@
|
||||||
|
use aiken/int
|
||||||
|
use aiken/list
|
||||||
|
|
||||||
|
// ------------------------------------------------------------------ Benchmarks
|
||||||
|
|
||||||
|
test bench_clausify_f1() {
|
||||||
|
run_clausify(F1) == []
|
||||||
|
}
|
||||||
|
|
||||||
|
test bench_clausify_f2() {
|
||||||
|
run_clausify(F2) == []
|
||||||
|
}
|
||||||
|
|
||||||
|
test bench_clausify_f3() {
|
||||||
|
run_clausify(F3) == [([1], [])]
|
||||||
|
}
|
||||||
|
|
||||||
|
test bench_clausify_f4() {
|
||||||
|
run_clausify(F4) == [
|
||||||
|
([1], [2, 3, 4, 5, 6, 7]),
|
||||||
|
([1, 2, 3], [4, 5, 6, 7]),
|
||||||
|
([1, 2, 3, 4, 5], [6, 7]),
|
||||||
|
([1, 2, 3, 4, 5, 6, 7], []),
|
||||||
|
([1, 2, 3, 4, 6], [5, 7]),
|
||||||
|
([1, 2, 3, 4, 7], [5, 6]),
|
||||||
|
([1, 2, 3, 5, 6], [4, 7]),
|
||||||
|
([1, 2, 3, 5, 7], [4, 6]),
|
||||||
|
([1, 2, 3, 6, 7], [4, 5]),
|
||||||
|
([1, 2, 4], [3, 5, 6, 7]),
|
||||||
|
([1, 2, 4, 5, 6], [3, 7]),
|
||||||
|
([1, 2, 4, 5, 7], [3, 6]),
|
||||||
|
([1, 2, 4, 6, 7], [3, 5]),
|
||||||
|
([1, 2, 5], [3, 4, 6, 7]),
|
||||||
|
([1, 2, 5, 6, 7], [3, 4]),
|
||||||
|
([1, 2, 6], [3, 4, 5, 7]),
|
||||||
|
([1, 2, 7], [3, 4, 5, 6]),
|
||||||
|
([1, 3, 4], [2, 5, 6, 7]),
|
||||||
|
([1, 3, 4, 5, 6], [2, 7]),
|
||||||
|
([1, 3, 4, 5, 7], [2, 6]),
|
||||||
|
([1, 3, 4, 6, 7], [2, 5]),
|
||||||
|
([1, 3, 5], [2, 4, 6, 7]),
|
||||||
|
([1, 3, 5, 6, 7], [2, 4]),
|
||||||
|
([1, 3, 6], [2, 4, 5, 7]),
|
||||||
|
([1, 3, 7], [2, 4, 5, 6]),
|
||||||
|
([1, 4, 5], [2, 3, 6, 7]),
|
||||||
|
([1, 4, 5, 6, 7], [2, 3]),
|
||||||
|
([1, 4, 6], [2, 3, 5, 7]),
|
||||||
|
([1, 4, 7], [2, 3, 5, 6]),
|
||||||
|
([1, 5, 6], [2, 3, 4, 7]),
|
||||||
|
([1, 5, 7], [2, 3, 4, 6]),
|
||||||
|
([1, 6, 7], [2, 3, 4, 5]),
|
||||||
|
([2], [1, 3, 4, 5, 6, 7]),
|
||||||
|
([2, 3, 4], [1, 5, 6, 7]),
|
||||||
|
([2, 3, 4, 5, 6], [1, 7]),
|
||||||
|
([2, 3, 4, 5, 7], [1, 6]),
|
||||||
|
([2, 3, 4, 6, 7], [1, 5]),
|
||||||
|
([2, 3, 5], [1, 4, 6, 7]),
|
||||||
|
([2, 3, 5, 6, 7], [1, 4]),
|
||||||
|
([2, 3, 6], [1, 4, 5, 7]),
|
||||||
|
([2, 3, 7], [1, 4, 5, 6]),
|
||||||
|
([2, 4, 5], [1, 3, 6, 7]),
|
||||||
|
([2, 4, 5, 6, 7], [1, 3]),
|
||||||
|
([2, 4, 6], [1, 3, 5, 7]),
|
||||||
|
([2, 4, 7], [1, 3, 5, 6]),
|
||||||
|
([2, 5, 6], [1, 3, 4, 7]),
|
||||||
|
([2, 5, 7], [1, 3, 4, 6]),
|
||||||
|
([2, 6, 7], [1, 3, 4, 5]),
|
||||||
|
([3], [1, 2, 4, 5, 6, 7]),
|
||||||
|
([3, 4, 5], [1, 2, 6, 7]),
|
||||||
|
([3, 4, 5, 6, 7], [1, 2]),
|
||||||
|
([3, 4, 6], [1, 2, 5, 7]),
|
||||||
|
([3, 4, 7], [1, 2, 5, 6]),
|
||||||
|
([3, 5, 6], [1, 2, 4, 7]),
|
||||||
|
([3, 5, 7], [1, 2, 4, 6]),
|
||||||
|
([3, 6, 7], [1, 2, 4, 5]),
|
||||||
|
([4], [1, 2, 3, 5, 6, 7]),
|
||||||
|
([4, 5, 6], [1, 2, 3, 7]),
|
||||||
|
([4, 5, 7], [1, 2, 3, 6]),
|
||||||
|
([4, 6, 7], [1, 2, 3, 5]),
|
||||||
|
([5], [1, 2, 3, 4, 6, 7]),
|
||||||
|
([5, 6, 7], [1, 2, 3, 4]),
|
||||||
|
([6], [1, 2, 3, 4, 5, 7]),
|
||||||
|
([7], [1, 2, 3, 4, 5, 6]),
|
||||||
|
]
|
||||||
|
}
|
||||||
|
|
||||||
|
test bench_clausify_f5() {
|
||||||
|
run_clausify(F5) == []
|
||||||
|
}
|
||||||
|
|
||||||
|
// ----------------------------------------------------------------------- Setup
|
||||||
|
|
||||||
|
type Var =
|
||||||
|
Int
|
||||||
|
|
||||||
|
type LRVars =
|
||||||
|
(List<Var>, List<Var>)
|
||||||
|
|
||||||
|
type Formula {
|
||||||
|
Sym(Var)
|
||||||
|
Not(Formula)
|
||||||
|
Dis(Formula, Formula)
|
||||||
|
Con(Formula, Formula)
|
||||||
|
Imp(Formula, Formula)
|
||||||
|
Eqv(Formula, Formula)
|
||||||
|
}
|
||||||
|
|
||||||
|
type StaticFormula {
|
||||||
|
F1
|
||||||
|
F2
|
||||||
|
F3
|
||||||
|
F4
|
||||||
|
F5
|
||||||
|
}
|
||||||
|
|
||||||
|
fn run_clausify(static_formula: StaticFormula) -> List<LRVars> {
|
||||||
|
static_formula
|
||||||
|
|> get_formula
|
||||||
|
|> clauses
|
||||||
|
}
|
||||||
|
|
||||||
|
fn get_formula(static_formula: StaticFormula) -> Formula {
|
||||||
|
when static_formula is {
|
||||||
|
// (a = a) = (a = a) = (a = a)
|
||||||
|
F1 ->
|
||||||
|
Eqv(Eqv(Sym(1), Sym(1)), Eqv(Eqv(Sym(1), Sym(1)), Eqv(Sym(1), Sym(1))))
|
||||||
|
|
||||||
|
// (a = a = a) = (a = a = a)
|
||||||
|
F2 ->
|
||||||
|
Eqv(Eqv(Sym(1), Eqv(Sym(1), Sym(1))), Eqv(Sym(1), Eqv(Sym(1), Sym(1))))
|
||||||
|
|
||||||
|
// (a = a = a) = (a = a) = (a = a)
|
||||||
|
F3 ->
|
||||||
|
Eqv(
|
||||||
|
Eqv(Sym(1), Eqv(Sym(1), Sym(1))),
|
||||||
|
Eqv(Eqv(Sym(1), Sym(1)), Eqv(Sym(1), Sym(1))),
|
||||||
|
)
|
||||||
|
|
||||||
|
// (a = b = c) = (d = e) = (f = g)
|
||||||
|
F4 ->
|
||||||
|
Eqv(
|
||||||
|
Eqv(Sym(1), Eqv(Sym(2), Sym(3))),
|
||||||
|
Eqv(Eqv(Sym(4), Sym(5)), Eqv(Sym(6), Sym(7))),
|
||||||
|
)
|
||||||
|
|
||||||
|
// (a = a = a) = (a = a = a) = (a = a)
|
||||||
|
F5 ->
|
||||||
|
Eqv(
|
||||||
|
Eqv(Sym(1), Eqv(Sym(1), Sym(1))),
|
||||||
|
Eqv(Eqv(Sym(1), Eqv(Sym(1), Sym(1))), Eqv(Sym(1), Sym(1))),
|
||||||
|
)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
fn clauses(formula: Formula) -> List<LRVars> {
|
||||||
|
formula
|
||||||
|
|> elim
|
||||||
|
|> negin
|
||||||
|
|> disin
|
||||||
|
|> split
|
||||||
|
|> unicl
|
||||||
|
}
|
||||||
|
|
||||||
|
fn clause(formula: Formula) -> LRVars {
|
||||||
|
do_clause(formula, ([], []))
|
||||||
|
}
|
||||||
|
|
||||||
|
fn do_clause(formula: Formula, vars: LRVars) -> LRVars {
|
||||||
|
when formula is {
|
||||||
|
Dis(p, q) -> do_clause(p, do_clause(q, vars))
|
||||||
|
Sym(s) -> (insert_ordered(vars.1st, s, int.compare), vars.2nd)
|
||||||
|
Not(Sym(s)) -> (vars.1st, insert_ordered(vars.2nd, s, int.compare))
|
||||||
|
_ -> fail
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
fn conjunct(formula: Formula) -> Bool {
|
||||||
|
when formula is {
|
||||||
|
Con(_, _) -> True
|
||||||
|
_ -> False
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
/// eliminate connectives other than not, disjunction and conjunction
|
||||||
|
fn elim(formula: Formula) -> Formula {
|
||||||
|
when formula is {
|
||||||
|
Sym(s) -> Sym(s)
|
||||||
|
Not(p) -> Not(elim(p))
|
||||||
|
Dis(p, q) -> Dis(elim(p), elim(q))
|
||||||
|
Con(p, q) -> Con(elim(p), elim(q))
|
||||||
|
Imp(p, q) -> Dis(Not(elim(p)), elim(q))
|
||||||
|
Eqv(f1, f2) -> Con(elim(Imp(f1, f2)), elim(Imp(f2, f1)))
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
/// -- shift negation to innermost positions
|
||||||
|
fn negin(formula: Formula) -> Formula {
|
||||||
|
when formula is {
|
||||||
|
Not(Not(p)) -> negin(p)
|
||||||
|
Not(Con(p, q)) -> Dis(negin(Not(p)), negin(Not(q)))
|
||||||
|
Not(Dis(p, q)) -> Con(negin(Not(p)), negin(Not(q)))
|
||||||
|
Dis(p, q) -> Dis(negin(p), negin(q))
|
||||||
|
Con(p, q) -> Con(negin(p), negin(q))
|
||||||
|
p -> p
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
/// shift disjunction within conjunction
|
||||||
|
fn disin(formula: Formula) -> Formula {
|
||||||
|
when formula is {
|
||||||
|
Dis(p, Con(q, r)) -> Con(disin(Dis(p, q)), disin(Dis(p, r)))
|
||||||
|
Dis(Con(p, q), r) -> Con(disin(Dis(p, r)), disin(Dis(q, r)))
|
||||||
|
Dis(p, q) -> {
|
||||||
|
let dp = disin(p)
|
||||||
|
let dq = disin(q)
|
||||||
|
if conjunct(dp) || conjunct(dq) {
|
||||||
|
disin(Dis(dp, dq))
|
||||||
|
} else {
|
||||||
|
Dis(dp, dq)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
Con(p, q) -> Con(disin(p), disin(q))
|
||||||
|
p -> p
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
/// split conjunctive proposition into a list of conjuncts
|
||||||
|
fn split(formula: Formula) -> List<Formula> {
|
||||||
|
do_split(formula, [])
|
||||||
|
}
|
||||||
|
|
||||||
|
fn do_split(f: Formula, fs: List<Formula>) -> List<Formula> {
|
||||||
|
when f is {
|
||||||
|
Con(p, q) -> do_split(p, do_split(q, fs))
|
||||||
|
_ ->
|
||||||
|
[f, ..fs]
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
/// form unique clausal axioms excluding tautologies
|
||||||
|
fn unicl(formulas: List<Formula>) -> List<LRVars> {
|
||||||
|
list.foldr(
|
||||||
|
formulas,
|
||||||
|
[],
|
||||||
|
fn(p, xs) {
|
||||||
|
let cp = clause(p)
|
||||||
|
if tautclause(cp) {
|
||||||
|
xs
|
||||||
|
} else {
|
||||||
|
insert_ordered(xs, cp, compare_lr_vars)
|
||||||
|
}
|
||||||
|
},
|
||||||
|
)
|
||||||
|
}
|
||||||
|
|
||||||
|
/// does any symbol appear in both consequent and antecedent of clause
|
||||||
|
fn tautclause(var: LRVars) -> Bool {
|
||||||
|
list.any(var.1st, list.has(var.2nd, _))
|
||||||
|
}
|
||||||
|
|
||||||
|
/// insertion of an item into an ordered list
|
||||||
|
fn insert_ordered(es: List<a>, e: a, compare: fn(a, a) -> Ordering) -> List<a> {
|
||||||
|
when es is {
|
||||||
|
[] ->
|
||||||
|
[e]
|
||||||
|
[head, ..tail] ->
|
||||||
|
when compare(e, head) is {
|
||||||
|
Less ->
|
||||||
|
[e, ..es]
|
||||||
|
Greater ->
|
||||||
|
[head, ..insert_ordered(tail, e, compare)]
|
||||||
|
Equal -> es
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
fn compare_lr_vars(a: LRVars, b: LRVars) -> Ordering {
|
||||||
|
when compare_list(a.1st, b.1st) is {
|
||||||
|
Equal -> compare_list(a.2nd, b.2nd)
|
||||||
|
ord -> ord
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
fn compare_list(xs: List<Int>, ys: List<Int>) -> Ordering {
|
||||||
|
when xs is {
|
||||||
|
[] ->
|
||||||
|
when ys is {
|
||||||
|
[] -> Equal
|
||||||
|
_ -> Less
|
||||||
|
}
|
||||||
|
[x, ..xs] ->
|
||||||
|
when ys is {
|
||||||
|
[] -> Greater
|
||||||
|
[y, ..ys] -> {
|
||||||
|
let ord = int.compare(x, y)
|
||||||
|
if ord == Equal {
|
||||||
|
compare_list(xs, ys)
|
||||||
|
} else {
|
||||||
|
ord
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
@ -0,0 +1,496 @@
|
||||||
|
use aiken/list
|
||||||
|
use benchmarks/knights/heuristic.{descendants, start_tour, tour_finished}
|
||||||
|
use benchmarks/knights/queue.{Queue}
|
||||||
|
use benchmarks/knights/types.{ChessSet, Solution}
|
||||||
|
|
||||||
|
// ------------------------------------------------------------------ Benchmarks
|
||||||
|
|
||||||
|
test bench_knights_100_4x4() {
|
||||||
|
run_knights(100, 4) == []
|
||||||
|
}
|
||||||
|
|
||||||
|
test bench_knights_100_6x6() {
|
||||||
|
run_knights(100, 6) == solution_100_6x6()
|
||||||
|
}
|
||||||
|
|
||||||
|
test bench_knights_100_8x8() {
|
||||||
|
run_knights(100, 8) == solution_100_8x8()
|
||||||
|
}
|
||||||
|
|
||||||
|
// ----------------------------------------------------------------------- Setup
|
||||||
|
|
||||||
|
fn run_knights(depth: Int, board_size: Int) -> Solution {
|
||||||
|
depth_search(depth, root(board_size), grow, done) |> queue.to_list
|
||||||
|
}
|
||||||
|
|
||||||
|
fn depth_search(
|
||||||
|
depth: Int,
|
||||||
|
xs: Queue<a>,
|
||||||
|
grow: fn(a) -> List<a>,
|
||||||
|
done: fn(a) -> Bool,
|
||||||
|
) -> Queue<a> {
|
||||||
|
if depth == 0 || queue.is_empty(xs) {
|
||||||
|
queue.new()
|
||||||
|
} else if done(queue.head(xs)) {
|
||||||
|
depth_search(depth - 1, queue.remove_front(xs), grow, done)
|
||||||
|
|> queue.append_front(queue.head(xs))
|
||||||
|
} else {
|
||||||
|
queue.append_all_front(queue.remove_front(xs), grow(queue.head(xs)))
|
||||||
|
|> depth_search(depth - 1, _, grow, done)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
fn root(size: Int) -> Queue<(Int, ChessSet)> {
|
||||||
|
queue.append_all_front(queue.new(), mk_starts(size))
|
||||||
|
}
|
||||||
|
|
||||||
|
fn mk_starts(size: Int) -> List<(Int, ChessSet)> {
|
||||||
|
let it = interval(1, size)
|
||||||
|
|
||||||
|
let l =
|
||||||
|
list.flat_map(
|
||||||
|
it,
|
||||||
|
fn(x) { list.map(it, fn(y) { start_tour((x, y), size) }) },
|
||||||
|
)
|
||||||
|
|
||||||
|
let length = list.length(l)
|
||||||
|
|
||||||
|
expect length == size * size
|
||||||
|
|
||||||
|
list.zip(list.repeat(1 - length, length), l)
|
||||||
|
}
|
||||||
|
|
||||||
|
fn interval(a: Int, b: Int) -> List<Int> {
|
||||||
|
if a > b {
|
||||||
|
[]
|
||||||
|
} else {
|
||||||
|
[a, ..interval(a + 1, b)]
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
fn grow(item: (Int, ChessSet)) -> List<(Int, ChessSet)> {
|
||||||
|
let (x, y) = item
|
||||||
|
descendants(y) |> list.map(fn(list_item) { (x + 1, list_item) })
|
||||||
|
}
|
||||||
|
|
||||||
|
fn done(item: (Int, ChessSet)) -> Bool {
|
||||||
|
tour_finished(item.2nd)
|
||||||
|
}
|
||||||
|
|
||||||
|
// ------------------------------------------------------------------ Fixtures
|
||||||
|
|
||||||
|
fn solution_100_6x6() -> Solution {
|
||||||
|
[
|
||||||
|
(
|
||||||
|
0,
|
||||||
|
ChessSet {
|
||||||
|
size: 6,
|
||||||
|
move_number: 36,
|
||||||
|
start: Some((1, 1)),
|
||||||
|
visited: [
|
||||||
|
(3, 2),
|
||||||
|
(5, 3),
|
||||||
|
(6, 1),
|
||||||
|
(4, 2),
|
||||||
|
(3, 4),
|
||||||
|
(2, 6),
|
||||||
|
(4, 5),
|
||||||
|
(6, 6),
|
||||||
|
(5, 4),
|
||||||
|
(6, 2),
|
||||||
|
(4, 1),
|
||||||
|
(2, 2),
|
||||||
|
(1, 4),
|
||||||
|
(3, 3),
|
||||||
|
(2, 1),
|
||||||
|
(1, 3),
|
||||||
|
(2, 5),
|
||||||
|
(4, 6),
|
||||||
|
(6, 5),
|
||||||
|
(4, 4),
|
||||||
|
(5, 2),
|
||||||
|
(6, 4),
|
||||||
|
(5, 6),
|
||||||
|
(3, 5),
|
||||||
|
(1, 6),
|
||||||
|
(2, 4),
|
||||||
|
(1, 2),
|
||||||
|
(3, 1),
|
||||||
|
(4, 3),
|
||||||
|
(5, 1),
|
||||||
|
(6, 3),
|
||||||
|
(5, 5),
|
||||||
|
(3, 6),
|
||||||
|
(1, 5),
|
||||||
|
(2, 3),
|
||||||
|
(1, 1),
|
||||||
|
],
|
||||||
|
},
|
||||||
|
),
|
||||||
|
(
|
||||||
|
0,
|
||||||
|
ChessSet {
|
||||||
|
size: 6,
|
||||||
|
move_number: 36,
|
||||||
|
start: Some((1, 1)),
|
||||||
|
visited: [
|
||||||
|
(3, 2),
|
||||||
|
(5, 3),
|
||||||
|
(6, 1),
|
||||||
|
(4, 2),
|
||||||
|
(3, 4),
|
||||||
|
(2, 2),
|
||||||
|
(4, 1),
|
||||||
|
(6, 2),
|
||||||
|
(5, 4),
|
||||||
|
(6, 6),
|
||||||
|
(4, 5),
|
||||||
|
(2, 6),
|
||||||
|
(1, 4),
|
||||||
|
(3, 3),
|
||||||
|
(2, 1),
|
||||||
|
(1, 3),
|
||||||
|
(2, 5),
|
||||||
|
(4, 6),
|
||||||
|
(6, 5),
|
||||||
|
(4, 4),
|
||||||
|
(5, 2),
|
||||||
|
(6, 4),
|
||||||
|
(5, 6),
|
||||||
|
(3, 5),
|
||||||
|
(1, 6),
|
||||||
|
(2, 4),
|
||||||
|
(1, 2),
|
||||||
|
(3, 1),
|
||||||
|
(4, 3),
|
||||||
|
(5, 1),
|
||||||
|
(6, 3),
|
||||||
|
(5, 5),
|
||||||
|
(3, 6),
|
||||||
|
(1, 5),
|
||||||
|
(2, 3),
|
||||||
|
(1, 1),
|
||||||
|
],
|
||||||
|
},
|
||||||
|
),
|
||||||
|
(
|
||||||
|
0,
|
||||||
|
ChessSet {
|
||||||
|
size: 6,
|
||||||
|
move_number: 36,
|
||||||
|
start: Some((1, 1)),
|
||||||
|
visited: [
|
||||||
|
(3, 2),
|
||||||
|
(5, 3),
|
||||||
|
(6, 1),
|
||||||
|
(4, 2),
|
||||||
|
(3, 4),
|
||||||
|
(2, 2),
|
||||||
|
(1, 4),
|
||||||
|
(2, 6),
|
||||||
|
(4, 5),
|
||||||
|
(6, 6),
|
||||||
|
(5, 4),
|
||||||
|
(6, 2),
|
||||||
|
(4, 1),
|
||||||
|
(3, 3),
|
||||||
|
(2, 1),
|
||||||
|
(1, 3),
|
||||||
|
(2, 5),
|
||||||
|
(4, 6),
|
||||||
|
(6, 5),
|
||||||
|
(4, 4),
|
||||||
|
(5, 2),
|
||||||
|
(6, 4),
|
||||||
|
(5, 6),
|
||||||
|
(3, 5),
|
||||||
|
(1, 6),
|
||||||
|
(2, 4),
|
||||||
|
(1, 2),
|
||||||
|
(3, 1),
|
||||||
|
(4, 3),
|
||||||
|
(5, 1),
|
||||||
|
(6, 3),
|
||||||
|
(5, 5),
|
||||||
|
(3, 6),
|
||||||
|
(1, 5),
|
||||||
|
(2, 3),
|
||||||
|
(1, 1),
|
||||||
|
],
|
||||||
|
},
|
||||||
|
),
|
||||||
|
(
|
||||||
|
0,
|
||||||
|
ChessSet {
|
||||||
|
size: 6,
|
||||||
|
move_number: 36,
|
||||||
|
start: Some((1, 1)),
|
||||||
|
visited: [
|
||||||
|
(3, 2),
|
||||||
|
(5, 3),
|
||||||
|
(6, 1),
|
||||||
|
(4, 2),
|
||||||
|
(3, 4),
|
||||||
|
(2, 6),
|
||||||
|
(1, 4),
|
||||||
|
(2, 2),
|
||||||
|
(4, 1),
|
||||||
|
(6, 2),
|
||||||
|
(5, 4),
|
||||||
|
(6, 6),
|
||||||
|
(4, 5),
|
||||||
|
(3, 3),
|
||||||
|
(2, 1),
|
||||||
|
(1, 3),
|
||||||
|
(2, 5),
|
||||||
|
(4, 6),
|
||||||
|
(6, 5),
|
||||||
|
(4, 4),
|
||||||
|
(5, 2),
|
||||||
|
(6, 4),
|
||||||
|
(5, 6),
|
||||||
|
(3, 5),
|
||||||
|
(1, 6),
|
||||||
|
(2, 4),
|
||||||
|
(1, 2),
|
||||||
|
(3, 1),
|
||||||
|
(4, 3),
|
||||||
|
(5, 1),
|
||||||
|
(6, 3),
|
||||||
|
(5, 5),
|
||||||
|
(3, 6),
|
||||||
|
(1, 5),
|
||||||
|
(2, 3),
|
||||||
|
(1, 1),
|
||||||
|
],
|
||||||
|
},
|
||||||
|
),
|
||||||
|
]
|
||||||
|
}
|
||||||
|
|
||||||
|
fn solution_100_8x8() -> Solution {
|
||||||
|
[
|
||||||
|
(
|
||||||
|
0,
|
||||||
|
ChessSet {
|
||||||
|
size: 8,
|
||||||
|
move_number: 64,
|
||||||
|
start: Some((1, 1)),
|
||||||
|
visited: [
|
||||||
|
(3, 2),
|
||||||
|
(4, 4),
|
||||||
|
(5, 6),
|
||||||
|
(6, 4),
|
||||||
|
(8, 5),
|
||||||
|
(7, 7),
|
||||||
|
(6, 5),
|
||||||
|
(8, 4),
|
||||||
|
(7, 2),
|
||||||
|
(5, 3),
|
||||||
|
(3, 4),
|
||||||
|
(4, 6),
|
||||||
|
(5, 8),
|
||||||
|
(6, 6),
|
||||||
|
(4, 5),
|
||||||
|
(3, 7),
|
||||||
|
(1, 8),
|
||||||
|
(2, 6),
|
||||||
|
(4, 7),
|
||||||
|
(5, 5),
|
||||||
|
(6, 3),
|
||||||
|
(5, 1),
|
||||||
|
(4, 3),
|
||||||
|
(3, 5),
|
||||||
|
(5, 4),
|
||||||
|
(7, 3),
|
||||||
|
(8, 1),
|
||||||
|
(6, 2),
|
||||||
|
(4, 1),
|
||||||
|
(2, 2),
|
||||||
|
(1, 4),
|
||||||
|
(3, 3),
|
||||||
|
(2, 5),
|
||||||
|
(1, 3),
|
||||||
|
(2, 1),
|
||||||
|
(4, 2),
|
||||||
|
(6, 1),
|
||||||
|
(8, 2),
|
||||||
|
(7, 4),
|
||||||
|
(8, 6),
|
||||||
|
(7, 8),
|
||||||
|
(5, 7),
|
||||||
|
(3, 8),
|
||||||
|
(1, 7),
|
||||||
|
(3, 6),
|
||||||
|
(2, 8),
|
||||||
|
(1, 6),
|
||||||
|
(2, 4),
|
||||||
|
(1, 2),
|
||||||
|
(3, 1),
|
||||||
|
(5, 2),
|
||||||
|
(7, 1),
|
||||||
|
(8, 3),
|
||||||
|
(7, 5),
|
||||||
|
(8, 7),
|
||||||
|
(6, 8),
|
||||||
|
(7, 6),
|
||||||
|
(8, 8),
|
||||||
|
(6, 7),
|
||||||
|
(4, 8),
|
||||||
|
(2, 7),
|
||||||
|
(1, 5),
|
||||||
|
(2, 3),
|
||||||
|
(1, 1),
|
||||||
|
],
|
||||||
|
},
|
||||||
|
),
|
||||||
|
(
|
||||||
|
0,
|
||||||
|
ChessSet {
|
||||||
|
size: 8,
|
||||||
|
move_number: 64,
|
||||||
|
start: Some((1, 1)),
|
||||||
|
visited: [
|
||||||
|
(3, 2),
|
||||||
|
(4, 4),
|
||||||
|
(5, 6),
|
||||||
|
(7, 7),
|
||||||
|
(8, 5),
|
||||||
|
(6, 4),
|
||||||
|
(7, 2),
|
||||||
|
(8, 4),
|
||||||
|
(6, 5),
|
||||||
|
(5, 3),
|
||||||
|
(3, 4),
|
||||||
|
(4, 6),
|
||||||
|
(5, 8),
|
||||||
|
(6, 6),
|
||||||
|
(4, 5),
|
||||||
|
(3, 7),
|
||||||
|
(1, 8),
|
||||||
|
(2, 6),
|
||||||
|
(4, 7),
|
||||||
|
(5, 5),
|
||||||
|
(6, 3),
|
||||||
|
(5, 1),
|
||||||
|
(4, 3),
|
||||||
|
(3, 5),
|
||||||
|
(5, 4),
|
||||||
|
(7, 3),
|
||||||
|
(8, 1),
|
||||||
|
(6, 2),
|
||||||
|
(4, 1),
|
||||||
|
(2, 2),
|
||||||
|
(1, 4),
|
||||||
|
(3, 3),
|
||||||
|
(2, 5),
|
||||||
|
(1, 3),
|
||||||
|
(2, 1),
|
||||||
|
(4, 2),
|
||||||
|
(6, 1),
|
||||||
|
(8, 2),
|
||||||
|
(7, 4),
|
||||||
|
(8, 6),
|
||||||
|
(7, 8),
|
||||||
|
(5, 7),
|
||||||
|
(3, 8),
|
||||||
|
(1, 7),
|
||||||
|
(3, 6),
|
||||||
|
(2, 8),
|
||||||
|
(1, 6),
|
||||||
|
(2, 4),
|
||||||
|
(1, 2),
|
||||||
|
(3, 1),
|
||||||
|
(5, 2),
|
||||||
|
(7, 1),
|
||||||
|
(8, 3),
|
||||||
|
(7, 5),
|
||||||
|
(8, 7),
|
||||||
|
(6, 8),
|
||||||
|
(7, 6),
|
||||||
|
(8, 8),
|
||||||
|
(6, 7),
|
||||||
|
(4, 8),
|
||||||
|
(2, 7),
|
||||||
|
(1, 5),
|
||||||
|
(2, 3),
|
||||||
|
(1, 1),
|
||||||
|
],
|
||||||
|
},
|
||||||
|
),
|
||||||
|
(
|
||||||
|
0,
|
||||||
|
ChessSet {
|
||||||
|
size: 8,
|
||||||
|
move_number: 64,
|
||||||
|
start: Some((1, 1)),
|
||||||
|
visited: [
|
||||||
|
(3, 2),
|
||||||
|
(4, 4),
|
||||||
|
(6, 5),
|
||||||
|
(8, 4),
|
||||||
|
(7, 2),
|
||||||
|
(5, 3),
|
||||||
|
(3, 4),
|
||||||
|
(4, 6),
|
||||||
|
(5, 8),
|
||||||
|
(7, 7),
|
||||||
|
(5, 6),
|
||||||
|
(6, 4),
|
||||||
|
(8, 5),
|
||||||
|
(6, 6),
|
||||||
|
(4, 5),
|
||||||
|
(3, 7),
|
||||||
|
(1, 8),
|
||||||
|
(2, 6),
|
||||||
|
(4, 7),
|
||||||
|
(5, 5),
|
||||||
|
(6, 3),
|
||||||
|
(5, 1),
|
||||||
|
(4, 3),
|
||||||
|
(3, 5),
|
||||||
|
(5, 4),
|
||||||
|
(7, 3),
|
||||||
|
(8, 1),
|
||||||
|
(6, 2),
|
||||||
|
(4, 1),
|
||||||
|
(2, 2),
|
||||||
|
(1, 4),
|
||||||
|
(3, 3),
|
||||||
|
(2, 5),
|
||||||
|
(1, 3),
|
||||||
|
(2, 1),
|
||||||
|
(4, 2),
|
||||||
|
(6, 1),
|
||||||
|
(8, 2),
|
||||||
|
(7, 4),
|
||||||
|
(8, 6),
|
||||||
|
(7, 8),
|
||||||
|
(5, 7),
|
||||||
|
(3, 8),
|
||||||
|
(1, 7),
|
||||||
|
(3, 6),
|
||||||
|
(2, 8),
|
||||||
|
(1, 6),
|
||||||
|
(2, 4),
|
||||||
|
(1, 2),
|
||||||
|
(3, 1),
|
||||||
|
(5, 2),
|
||||||
|
(7, 1),
|
||||||
|
(8, 3),
|
||||||
|
(7, 5),
|
||||||
|
(8, 7),
|
||||||
|
(6, 8),
|
||||||
|
(7, 6),
|
||||||
|
(8, 8),
|
||||||
|
(6, 7),
|
||||||
|
(4, 8),
|
||||||
|
(2, 7),
|
||||||
|
(1, 5),
|
||||||
|
(2, 3),
|
||||||
|
(1, 1),
|
||||||
|
],
|
||||||
|
},
|
||||||
|
),
|
||||||
|
]
|
||||||
|
}
|
||||||
|
|
@ -0,0 +1,56 @@
|
||||||
|
use aiken/list
|
||||||
|
use benchmarks/knights/types.{ChessSet, Tile}
|
||||||
|
|
||||||
|
pub fn create_board(size: Int, init_square: Tile) -> ChessSet {
|
||||||
|
ChessSet {
|
||||||
|
size,
|
||||||
|
move_number: 1,
|
||||||
|
start: Some(init_square),
|
||||||
|
visited: [init_square],
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn add_piece(board: ChessSet, tile: Tile) -> ChessSet {
|
||||||
|
ChessSet {
|
||||||
|
..board,
|
||||||
|
move_number: board.move_number + 1,
|
||||||
|
visited: [tile, ..board.visited],
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn first_piece(board: ChessSet) -> Tile {
|
||||||
|
expect Some(tile) = board.start
|
||||||
|
tile
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn last_piece(board: ChessSet) -> Tile {
|
||||||
|
when board.visited is {
|
||||||
|
[] -> fail
|
||||||
|
[x, ..] -> x
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn delete_first(board: ChessSet) -> ChessSet {
|
||||||
|
let ChessSet { move_number, visited, .. } = board
|
||||||
|
|
||||||
|
expect Some(new_visited) = list.init(visited)
|
||||||
|
|
||||||
|
ChessSet {
|
||||||
|
..board,
|
||||||
|
move_number: move_number - 1,
|
||||||
|
start: second_last(visited),
|
||||||
|
visited: new_visited,
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
fn second_last(visited: List<a>) -> Option<a> {
|
||||||
|
when list.reverse(visited) is {
|
||||||
|
[] -> fail
|
||||||
|
[_] -> None
|
||||||
|
[_, a, ..] -> Some(a)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn is_square_free(board: ChessSet, tile: Tile) -> Bool {
|
||||||
|
!list.has(board.visited, tile)
|
||||||
|
}
|
||||||
|
|
@ -0,0 +1,172 @@
|
||||||
|
use aiken/builtin
|
||||||
|
use aiken/int
|
||||||
|
use aiken/list
|
||||||
|
use benchmarks/knights/chess_set.{
|
||||||
|
add_piece, create_board, delete_first, first_piece, is_square_free, last_piece,
|
||||||
|
}
|
||||||
|
use benchmarks/knights/sort.{quicksort}
|
||||||
|
use benchmarks/knights/types.{ChessSet, Tile}
|
||||||
|
|
||||||
|
type Direction {
|
||||||
|
UL
|
||||||
|
UR
|
||||||
|
DL
|
||||||
|
DR
|
||||||
|
LU
|
||||||
|
LD
|
||||||
|
RU
|
||||||
|
RD
|
||||||
|
}
|
||||||
|
|
||||||
|
fn direction_list() {
|
||||||
|
[UL, UR, DL, DR, LU, LD, RU, RD]
|
||||||
|
}
|
||||||
|
|
||||||
|
fn move(direction: Direction, tile: Tile) -> Tile {
|
||||||
|
let (x, y) = tile
|
||||||
|
when direction is {
|
||||||
|
UL -> (x - 1, y - 2)
|
||||||
|
UR -> (x + 1, y - 2)
|
||||||
|
DL -> (x - 1, y + 2)
|
||||||
|
DR -> (x + 1, y + 2)
|
||||||
|
LU -> (x - 2, y - 1)
|
||||||
|
LD -> (x - 2, y + 1)
|
||||||
|
RU -> (x + 2, y - 1)
|
||||||
|
RD -> (x + 2, y + 1)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn start_tour(st: Tile, size: Int) -> ChessSet {
|
||||||
|
expect 0 = builtin.remainder_integer(size, 2)
|
||||||
|
create_board(size, st)
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn tour_finished(board: ChessSet) -> Bool {
|
||||||
|
let ChessSet { move_number, size, .. } = board
|
||||||
|
move_number == size * size && can_jump_first(board)
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn descendants(board: ChessSet) -> List<ChessSet> {
|
||||||
|
if and {
|
||||||
|
can_jump_first(board),
|
||||||
|
board
|
||||||
|
|> first_piece
|
||||||
|
|> add_piece(board, _)
|
||||||
|
|> dead_end,
|
||||||
|
} {
|
||||||
|
[]
|
||||||
|
} else {
|
||||||
|
let singles = single_descend(board)
|
||||||
|
|
||||||
|
when singles is {
|
||||||
|
[] ->
|
||||||
|
board
|
||||||
|
|> desc_and_no
|
||||||
|
|> quicksort(compare_chess_set)
|
||||||
|
|> list.map(fn(t) { t.2nd })
|
||||||
|
[_] -> singles
|
||||||
|
_ ->
|
||||||
|
[]
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn can_jump_first(board: ChessSet) -> Bool {
|
||||||
|
can_move_to(delete_first(board), first_piece(board))
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn dead_end(board: ChessSet) -> Bool {
|
||||||
|
board |> possible_moves |> builtin.null_list
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn single_descend(board: ChessSet) -> List<ChessSet> {
|
||||||
|
list.filter_map(
|
||||||
|
desc_and_no(board),
|
||||||
|
fn(item) {
|
||||||
|
let (moves, board) = item
|
||||||
|
if moves == 1 {
|
||||||
|
Some(board)
|
||||||
|
} else {
|
||||||
|
None
|
||||||
|
}
|
||||||
|
},
|
||||||
|
)
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn desc_and_no(board: ChessSet) -> List<(Int, ChessSet)> {
|
||||||
|
board
|
||||||
|
|> all_descend
|
||||||
|
|> list.map(
|
||||||
|
fn(item) {
|
||||||
|
(item |> delete_first |> possible_moves |> list.length, item)
|
||||||
|
},
|
||||||
|
)
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn can_move_to(board: ChessSet, tile: Tile) -> Bool {
|
||||||
|
let (x, y) = tile
|
||||||
|
let size = board.size
|
||||||
|
and {
|
||||||
|
x >= 1,
|
||||||
|
x <= size,
|
||||||
|
y >= 1,
|
||||||
|
y <= size,
|
||||||
|
is_square_free(board, tile),
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
fn can_move(board: ChessSet, direction: Direction) -> Bool {
|
||||||
|
board |> can_move_to(move(direction, last_piece(board)))
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn all_descend(board: ChessSet) -> List<ChessSet> {
|
||||||
|
board
|
||||||
|
|> possible_moves
|
||||||
|
|> list.map(move_knight(board, _))
|
||||||
|
}
|
||||||
|
|
||||||
|
fn move_knight(board: ChessSet, direction: Direction) -> ChessSet {
|
||||||
|
add_piece(board, move(direction, last_piece(board)))
|
||||||
|
}
|
||||||
|
|
||||||
|
fn possible_moves(board: ChessSet) -> List<Direction> {
|
||||||
|
direction_list() |> list.filter(can_move(board, _))
|
||||||
|
}
|
||||||
|
|
||||||
|
fn compare_chess_set(a: (Int, ChessSet), b: (Int, ChessSet)) -> Ordering {
|
||||||
|
if a.1st != b.1st {
|
||||||
|
int.compare(a.1st, b.1st)
|
||||||
|
} else {
|
||||||
|
compare_list(a.2nd.visited, b.2nd.visited)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
fn compare_list(xs: List<Tile>, ys: List<Tile>) -> Ordering {
|
||||||
|
when xs is {
|
||||||
|
[] ->
|
||||||
|
when ys is {
|
||||||
|
[] -> Equal
|
||||||
|
_ -> Less
|
||||||
|
}
|
||||||
|
[x, ..xs] ->
|
||||||
|
when ys is {
|
||||||
|
[] -> Greater
|
||||||
|
[y, ..ys] -> {
|
||||||
|
let ord = compare_tile(x, y)
|
||||||
|
if ord == Equal {
|
||||||
|
compare_list(xs, ys)
|
||||||
|
} else {
|
||||||
|
ord
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
fn compare_tile(a: Tile, b: Tile) -> Ordering {
|
||||||
|
if a.1st == b.1st {
|
||||||
|
int.compare(a.2nd, b.2nd)
|
||||||
|
} else {
|
||||||
|
int.compare(a.1st, b.1st)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
@ -0,0 +1,38 @@
|
||||||
|
use aiken/list
|
||||||
|
|
||||||
|
pub opaque type Queue<a> {
|
||||||
|
inner: List<a>,
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn new() -> Queue<a> {
|
||||||
|
[] |> Queue
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn to_list(self: Queue<a>) -> List<a> {
|
||||||
|
self.inner
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn is_empty(self: Queue<a>) -> Bool {
|
||||||
|
when self.inner is {
|
||||||
|
[] -> True
|
||||||
|
_ -> False
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn append_front(self: Queue<a>, item: a) -> Queue<a> {
|
||||||
|
list.push(self.inner, item) |> Queue
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn append_all_front(self: Queue<a>, items: List<a>) -> Queue<a> {
|
||||||
|
list.concat(items, self.inner) |> Queue
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn remove_front(self: Queue<a>) -> Queue<a> {
|
||||||
|
expect [_, ..rest] = self.inner
|
||||||
|
rest |> Queue
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn head(self: Queue<a>) -> a {
|
||||||
|
expect [q, ..] = self.inner
|
||||||
|
q
|
||||||
|
}
|
||||||
|
|
@ -0,0 +1,19 @@
|
||||||
|
use aiken/list
|
||||||
|
|
||||||
|
pub fn quicksort(xs: List<a>, compare: fn(a, a) -> Ordering) -> List<a> {
|
||||||
|
when xs is {
|
||||||
|
[] ->
|
||||||
|
[]
|
||||||
|
[head, ..tail] -> {
|
||||||
|
let before =
|
||||||
|
tail
|
||||||
|
|> list.filter(fn(x) { compare(x, head) == Less })
|
||||||
|
|> quicksort(compare)
|
||||||
|
let after =
|
||||||
|
tail
|
||||||
|
|> list.filter(fn(x) { compare(x, head) != Less })
|
||||||
|
|> quicksort(compare)
|
||||||
|
list.concat(before, [head, ..after])
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
@ -0,0 +1,12 @@
|
||||||
|
pub type Tile =
|
||||||
|
(Int, Int)
|
||||||
|
|
||||||
|
pub type ChessSet {
|
||||||
|
size: Int,
|
||||||
|
move_number: Int,
|
||||||
|
start: Option<Tile>,
|
||||||
|
visited: List<Tile>,
|
||||||
|
}
|
||||||
|
|
||||||
|
pub type Solution =
|
||||||
|
List<(Int, ChessSet)>
|
||||||
|
|
@ -0,0 +1,14 @@
|
||||||
|
{
|
||||||
|
"preamble": {
|
||||||
|
"title": "aiken/benchmarks",
|
||||||
|
"description": "Aiken contracts for project 'aiken/benchmarks'",
|
||||||
|
"version": "0.0.0",
|
||||||
|
"plutusVersion": "v2",
|
||||||
|
"compiler": {
|
||||||
|
"name": "Aiken",
|
||||||
|
"version": "v1.0.21-alpha+4b04517"
|
||||||
|
},
|
||||||
|
"license": "Apache-2.0"
|
||||||
|
},
|
||||||
|
"validators": []
|
||||||
|
}
|
||||||
Loading…
Reference in New Issue