Move benchmarks one level up.
This commit is contained in:
304
benchmarks/lib/benchmarks/clausify/benchmark.ak
Normal file
304
benchmarks/lib/benchmarks/clausify/benchmark.ak
Normal file
@@ -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
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
496
benchmarks/lib/benchmarks/knights/benchmark.ak
Normal file
496
benchmarks/lib/benchmarks/knights/benchmark.ak
Normal file
@@ -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),
|
||||
],
|
||||
},
|
||||
),
|
||||
]
|
||||
}
|
||||
56
benchmarks/lib/benchmarks/knights/chess_set.ak
Normal file
56
benchmarks/lib/benchmarks/knights/chess_set.ak
Normal file
@@ -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)
|
||||
}
|
||||
172
benchmarks/lib/benchmarks/knights/heuristic.ak
Normal file
172
benchmarks/lib/benchmarks/knights/heuristic.ak
Normal file
@@ -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)
|
||||
}
|
||||
}
|
||||
38
benchmarks/lib/benchmarks/knights/queue.ak
Normal file
38
benchmarks/lib/benchmarks/knights/queue.ak
Normal file
@@ -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
|
||||
}
|
||||
19
benchmarks/lib/benchmarks/knights/sort.ak
Normal file
19
benchmarks/lib/benchmarks/knights/sort.ak
Normal file
@@ -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])
|
||||
}
|
||||
}
|
||||
}
|
||||
12
benchmarks/lib/benchmarks/knights/types.ak
Normal file
12
benchmarks/lib/benchmarks/knights/types.ak
Normal file
@@ -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)>
|
||||
Reference in New Issue
Block a user