Add satblit tool with readme (#92)

* Include ocaml in the prerequisites
* Change the output to generate blitter config macros
* Describe how to use the results in the readme
* Add acknowledgement and license

effects/game-of-life/satblit/LICENSE

@@ -0,0 +1,20 @@
+Copyright (c) 2021-2023 Piotr Polesiuk & Ghostown
+
+Permission is hereby granted, free of charge, to any person obtaining
+a copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject to
+the following conditions:
+
+The above copyright notice and this permission notice shall be
+included in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
+LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
+OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

effects/game-of-life/satblit/README.md

@@ -0,0 +1,61 @@
+# Cellular automata to blits tool
+
+This tool can generate blitter configurations to compute next generation of cellular automata from a previous generation.
+It generates a series of blitter configurations (passes) that start from a bitmap of a previous generation, run blitter on it and several intermediate results from those blitter phases and produce a new bitmap with the next generation.
+
+This is done by:
+1. Generating an input for a SAT-solver
+2. Running a SAT-solver on it
+3. Converting the result from a SAT-solver to blitter configs (if solution found)
+
+## Prerequisites
+
+- OCaml and the `ocamlbuild` build system
+- Any SAT-solver. `minisat` is a go to, but some more powerful ones might be required for more complex rulesets.
+
+## Compiling
+
+```
+ocamlbuild satblit.native
+```
+
+## Usage
+
+1. Generate input 
+```
+./satblit.native <N> -o <survive> <born> > solverinput.cnf
+```
+
+Where:
+- `N` is the amount of blits *in addition to 6 predefined blits* that must be present (2 of those are hardcoded, 4 of those use predefined inputs but blitter function is searched for by the SAT-solver)
+- `survive` is a string containing digits 0-8 that specifies how many alive neighbours a cell needs to survive (if it's alive). Default: 23
+- `born` is a string containing digits 0-8 that specifies how many alive neighbours a cell needs to become alive (if it's dead). Default: 3
+
+Example for [long life cellular automata](https://conwaylife.com/wiki/OCA:LongLife):
+```
+./satblit.native 3 -o 5 345 > solverinput.cnf
+```
+
+2. Run a SAT-solver
+Example using `minisat`:
+```
+minisat solverinput.cnf solveroutput.sat
+```
+
+If the formula was satisfiable `minisat` should print `SATISFIABLE` and produce the output file.
+Otherwise if the formula was not satisfiable and `UNSATISFIABLE` was printed then you need to go back to step 1. and increase N.
+
+3. Convert SAT-solver output to blitter passes:
+
+```
+./satblit.native <N> -d < solveroutput.sat
+```
+
+Value of `N` has to be the same as the one used to generate the input in step 1. corresponding to the output from step 2.
+Result is a list of macros of blitter configs that have to be run in sequence in order to calculate the next generation.
+They are used in a structure describing a set of blitter passes, see [here](https://github.com/cahirwpz/ghostown-electric-lifeforms/blob/478ca16e16fb5fd6446b255df8066ed984248b18/intro/gol-games.c#L48) for an example.
+
+# Acknowledgements
+
+**Piotr Polesiuk** - for the original idea to use a SAT-solver for finding blitter configurations and for kindly donating the initial version of the code contained here.
+

effects/game-of-life/satblit/sat.ml

@@ -0,0 +1,133 @@
+(*
+ * Copyright 2021-2023 Piotr Polesiuk & Ghostown
+ * SPDX-License-Identifier: MIT
+ *)
+
+type var = int
+
+let var_num = ref 0
+
+let fresh_var () =
+  var_num := !var_num + 1;
+  !var_num
+
+type lit =
+| Pos of var
+| Neg of var
+
+let pos x = Pos x
+let neg x = Neg x
+
+let clauses = ref []
+
+let add_clause c =
+  clauses := c :: !clauses
+
+let dump_dimacs () =
+  let dump_lit l =
+    match l with
+    | Pos n -> Printf.printf "%d " n
+    | Neg n -> Printf.printf "-%d " n
+  in
+  Printf.printf "p cnf %d %d\n" !var_num (List.length !clauses);
+  !clauses |> List.iter (fun cl ->
+    List.iter dump_lit cl;
+    Printf.printf "0\n")
+
+let values = Hashtbl.create 32
+let rec read_dimacs_loop () =
+  let n = Scanf.scanf " %d" (fun n -> n) in
+  if n = 0 then ()
+  else begin
+    if n > 0 then Hashtbl.add values n true
+    else Hashtbl.add values (-n) false;
+    read_dimacs_loop ()
+  end
+
+let read_dimacs () =
+  match read_line () with
+  | "SAT" ->
+    read_dimacs_loop ()
+  | l ->
+    Printf.printf "%s\n" l;
+    exit 1
+
+type one_hot_sel =
+| OHSel of var list
+
+let one_hot_sel n =
+  let xs = List.init n (fun _ -> fresh_var ()) in
+  add_clause (List.map pos xs);
+  List.iteri (fun i xi ->
+    List.iteri (fun j xj ->
+      if i > j then add_clause [ neg xi; neg xj ]
+    ) xs
+  ) xs;
+  OHSel xs
+
+let one_hot_mux (OHSel xs) ys =
+  let z = fresh_var () in
+  List.iter2 (fun x y ->
+    add_clause [ neg x; neg y; pos z ];
+    add_clause [ neg x; pos y; neg z ]
+  ) xs ys;
+  z
+
+type lut =
+| Lut of int * var list
+
+let lut_create n =
+  Lut(n, List.init (1 lsl n) (fun _ -> fresh_var ()))
+
+let lut_lookup (Lut(n, xs)) ys =
+  assert (List.length ys = n);
+  let z = fresh_var () in
+  List.iteri (fun i x ->
+    let cnd = ys |> List.mapi (fun j y ->
+      if ((i lsr j) land 1) = 0 then pos y else neg y) in
+    add_clause ( neg x :: pos z :: cnd );
+    add_clause ( pos x :: neg z :: cnd )
+  ) xs;
+  z
+
+let input n =
+  let tt = fresh_var () in
+  let ff = fresh_var () in
+  add_clause [ pos tt ];
+  add_clause [ neg ff ];
+  List.init (1 lsl n) (fun i ->
+    let xs = List.init n (fun j ->
+      if ((i lsr j) land 1) = 0 then ff else tt)
+    in
+    (xs, i))
+
+let set_true x  = add_clause [ pos x ]
+let set_false x = add_clause [ neg x ]
+
+let minterms = ["NANBNC"; "NANBC"; "NABNC"; "NABC"; "ANBNC"; "ANBC"; "ABNC"; "ABC"]
+let string_of_lut4 (Lut(_, xs)) =
+  minterms |> List.mapi (fun i minterm ->
+    let n_bits = (i land 0x1) + ((i lsr 1) land 0x1) + ((i lsr 2) land 0x1) in
+    let x = List.nth xs n_bits in
+    if Hashtbl.find values x then
+      minterm
+    else
+      ""
+  ) |> List.filter (fun s -> s <> "") |> String.concat " | "
+
+let string_of_lut8 (Lut(_, xs)) =
+  List.map2 (fun x minterm ->
+    if Hashtbl.find values x then
+      minterm
+    else
+      ""
+  ) xs minterms |> List.filter (fun s -> s <> "") |> String.concat " | "
+
+let one_hot_sel_n (OHSel xs) =
+  xs
+  |> List.mapi (fun i x -> if Hashtbl.find values x then i else 0)
+  |> List.fold_left (+) 0
+
+let lut_lookup_n (Lut(l, xs)) n =
+  let x = List.nth xs n in
+  if Hashtbl.find values x then 1 else 0

effects/game-of-life/satblit/sat.mli

@@ -0,0 +1,31 @@
+(*
+ * Copyright 2021-2023 Piotr Polesiuk & Ghostown
+ * SPDX-License-Identifier: MIT
+ *)
+
+type var
+
+val dump_dimacs : unit -> unit
+val read_dimacs : unit -> unit
+
+type one_hot_sel =
+| OHSel of var list
+
+val one_hot_sel : int -> one_hot_sel
+val one_hot_mux : one_hot_sel -> var list -> var
+
+type lut =
+| Lut of int * var list
+
+val lut_create : int -> lut
+val lut_lookup : lut -> var list -> var
+
+val input : int -> (var list * int) list
+
+val set_true  : var -> unit
+val set_false : var -> unit
+
+val string_of_lut4 : lut -> string
+val string_of_lut8 : lut -> string
+val one_hot_sel_n : one_hot_sel -> int
+val lut_lookup_n : lut -> int -> int

effects/game-of-life/satblit/satblit.ml

@@ -0,0 +1,132 @@
+(*
+ * Copyright 2021-2023 Piotr Polesiuk & Ghostown
+ * SPDX-License-Identifier: MIT
+ *)
+
+open Sat
+
+let blit_n = int_of_string Sys.argv.(1)
+let survive = if Array.length Sys.argv > 3 then Sys.argv.(3) else "23"
+let born    = if Array.length Sys.argv > 4 then Sys.argv.(4) else "3"
+
+let lut_a1 = lut_create 2
+let lut_a2 = lut_create 2
+let lut_b1 = lut_create 2
+let lut_b2 = lut_create 2
+
+let luts = Array.init blit_n (fun _ -> lut_create 3)
+
+let sels = Array.init blit_n (fun i ->
+  let n = 5 + i in
+  (one_hot_sel n, one_hot_sel n, one_hot_sel n))
+
+let inp = input 5
+
+let list_last xs =
+  List.nth xs (List.length xs - 1)
+
+let rec build dat layer_i =
+  if layer_i = blit_n then List.map list_last dat
+  else
+    let (sa, sb, sc) = sels.(layer_i) in
+    let dat =
+      dat |> List.map (fun dat_vec ->
+        let xa = one_hot_mux sa dat_vec in
+        let xb = one_hot_mux sb dat_vec in
+        let xc = one_hot_mux sc dat_vec in
+        dat_vec @ [ lut_lookup luts.(layer_i) [ xa; xb; xc ] ])
+    in build dat (layer_i + 1)
+
+let pre = inp |> List.map (fun (data, _) ->
+  match data with
+  | [ a0; a1; b0; b1; x ] ->
+    let v1 = lut_lookup lut_a1 [ a0; a1 ] in
+    let v2 = lut_lookup lut_a2 [ a0; a1 ] in
+    let v3 = lut_lookup lut_b1 [ b0; b1 ] in
+    let v4 = lut_lookup lut_b2 [ b0; b1 ] in
+    [ v1; v2; v3; v4; x ]
+  | _ -> assert false)
+
+let outp = build pre 0
+
+let () = outp |> List.iteri (fun i x ->
+  let n = (i land 3) + ((i lsr 1) land 6) in
+  let b =
+    if (i land 0x10) > 0 then
+      String.contains survive (Char.chr (Char.code '0' + n - 1))
+    else
+      String.contains born (Char.chr (Char.code '0' + n))
+  in
+  if b then set_true x else set_false x)
+
+let run_at i =
+  let v = ref (i land 0x10) in
+  v := !v lor (lut_lookup_n lut_a1 (i land 0x3) lsl 0);
+  v := !v lor (lut_lookup_n lut_a2 (i land 0x3) lsl 1);
+  v := !v lor (lut_lookup_n lut_b1 ((i lsr 2) land 0x3) lsl 2);
+  v := !v lor (lut_lookup_n lut_b2 ((i lsr 2) land 0x3) lsl 3);
+  for i = 0 to blit_n - 1 do
+    let (sa, sb, sc) = sels.(i) in
+    let b0 = (!v lsr (one_hot_sel_n sa)) land 1 in
+    let b1 = (!v lsr (one_hot_sel_n sb)) land 1 in
+    let b2 = (!v lsr (one_hot_sel_n sc)) land 1 in
+    v := !v lor (lut_lookup_n luts.(i) (b2*4 + b1*2 + b0) lsl (i + 5))
+  done;
+  !v
+
+(* due to how indexing was originally handled (first 2 blits were not counted
+   and index 4 was treated as previous generation) this corrects the indexing to
+   treat index 0 as having the previous generation and includes the first 2 blits *)
+let one_hot_to_amiga n =
+  if n < 4 then
+    n + 3
+  else if n = 4 then
+    0
+  else
+    n + 2
+
+let () = 
+  if Sys.argv.(2) = "-o" then dump_dimacs ()
+  else if Sys.argv.(2) = "-d" then begin
+    read_dimacs ();
+    Printf.printf "PHASE_SIMPLE(0, 1, FULL_ADDER, BlitAdjacentHorizontal),\n";
+    Printf.printf "PHASE_SIMPLE(0, 2, FULL_ADDER_CARRY, BlitAdjacentHorizontal),\n";
+    Printf.printf "PHASE_SIMPLE(1, 3, %s, BlitAdjacentVertical),\n" (string_of_lut4 lut_a1);
+    Printf.printf "PHASE_SIMPLE(1, 4, %s, BlitAdjacentVertical),\n" (string_of_lut4 lut_a2);
+    Printf.printf "PHASE_SIMPLE(2, 5, %s, BlitAdjacentVertical),\n" (string_of_lut4 lut_b1);
+    Printf.printf "PHASE_SIMPLE(2, 6, %s, BlitAdjacentVertical),\n" (string_of_lut4 lut_b2);
+    for i = 0 to blit_n - 1 do
+      let (sa, sb, sc) = sels.(i) in
+      Printf.printf "PHASE(%d, %d, %d, %d, %s, BlitFunc),\n" 
+        ((one_hot_sel_n sc) |> one_hot_to_amiga)
+        ((one_hot_sel_n sb) |> one_hot_to_amiga)
+        ((one_hot_sel_n sa) |> one_hot_to_amiga)
+        (* if last blit then output to bitplane 0 (next generation overwrites previous generation) *)
+        (if i <> blit_n - 1 then
+          (i + 7)
+        else
+          0
+        )
+        (string_of_lut8 luts.(i));
+    done
+  end else if Sys.argv.(2) = "-t" then begin
+    read_dimacs ();
+    for i = 0 to 31 do
+      let n = (i land 3) + ((i lsr 1) land 6) in
+      let v = run_at i in
+      Printf.printf "%s + %d -> %d%d%d%d_%d_%d%d%d\n"
+        (if (i land 0x10) > 0 then "alive" else "dead ")
+        n
+        ((v lsr 0) land 1)
+        ((v lsr 1) land 1)
+        ((v lsr 2) land 1)
+        ((v lsr 3) land 1)
+        ((v lsr 4) land 1)
+        ((v lsr 5) land 1)
+        ((v lsr 6) land 1)
+        ((v lsr 7) land 1)
+    done
+  end else begin
+    Printf.eprintf "Bad flags\n";
+    exit 1
+  end