From 52974aed7521cff541c3124cf4a0b7fa0f20993b Mon Sep 17 00:00:00 2001
From: KtorZ <matthias.benkort@gmail.com>
Date: Wed, 17 Jul 2024 12:51:58 +0200
Subject: [PATCH] Add clausify benchmark.

---
 examples/benchmarks/README.md                 |  87 +++++
 .../lib/benchmarks/clausify/benchmark.ak      | 304 ++++++++++++++++++
 .../{knights.ak => knights/benchmark.ak}      |   2 +-
 .../lib/benchmarks/{ => knights}/queue.ak     |   0
 4 files changed, 392 insertions(+), 1 deletion(-)
 create mode 100644 examples/benchmarks/lib/benchmarks/clausify/benchmark.ak
 rename examples/benchmarks/lib/benchmarks/{knights.ak => knights/benchmark.ak} (99%)
 rename examples/benchmarks/lib/benchmarks/{ => knights}/queue.ak (100%)

diff --git a/examples/benchmarks/README.md b/examples/benchmarks/README.md
index 54644eea..25cbf09a 100644
--- a/examples/benchmarks/README.md
+++ b/examples/benchmarks/README.md
@@ -8,8 +8,49 @@ Note that the primary use-case of those benchmarks is to compare Aiken with itse
 
 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
@@ -19,6 +60,15 @@ v1.0.29-alpha & v1.0.28-alpha
 ==== 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
@@ -26,6 +76,15 @@ v1.0.26-alpha & V1.0.25-alpha
     ┕━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ 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
@@ -35,6 +94,15 @@ v1.0.24-alpha & V1.0.23-alpha
 ==== 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
@@ -42,6 +110,15 @@ V1.0.21-alpha
     ┕━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ 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
@@ -53,6 +130,11 @@ V1.0.20-alpha, v1.0.19-alpha & v1.0.18-alpha
 
 | 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%      |
@@ -61,6 +143,11 @@ V1.0.20-alpha, v1.0.19-alpha & v1.0.18-alpha
 
 | 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%      |
diff --git a/examples/benchmarks/lib/benchmarks/clausify/benchmark.ak b/examples/benchmarks/lib/benchmarks/clausify/benchmark.ak
new file mode 100644
index 00000000..4ffd36c5
--- /dev/null
+++ b/examples/benchmarks/lib/benchmarks/clausify/benchmark.ak
@@ -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
+          }
+        }
+      }
+  }
+}
diff --git a/examples/benchmarks/lib/benchmarks/knights.ak b/examples/benchmarks/lib/benchmarks/knights/benchmark.ak
similarity index 99%
rename from examples/benchmarks/lib/benchmarks/knights.ak
rename to examples/benchmarks/lib/benchmarks/knights/benchmark.ak
index 7e9374b6..15bea26e 100644
--- a/examples/benchmarks/lib/benchmarks/knights.ak
+++ b/examples/benchmarks/lib/benchmarks/knights/benchmark.ak
@@ -1,7 +1,7 @@
 use aiken/list
 use benchmarks/knights/heuristic.{descendants, start_tour, tour_finished}
+use benchmarks/knights/queue.{Queue}
 use benchmarks/knights/types.{ChessSet, Solution}
-use benchmarks/queue.{Queue}
 
 // ------------------------------------------------------------------ Benchmarks
 
diff --git a/examples/benchmarks/lib/benchmarks/queue.ak b/examples/benchmarks/lib/benchmarks/knights/queue.ak
similarity index 100%
rename from examples/benchmarks/lib/benchmarks/queue.ak
rename to examples/benchmarks/lib/benchmarks/knights/queue.ak