From 26a6cbfc6eaac73a51cf1207baa31dff2bbd321b Mon Sep 17 00:00:00 2001 From: Kristopher38 Date: Sat, 16 Dec 2023 17:55:44 +0100 Subject: [PATCH] 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 | 20 ++++ effects/game-of-life/satblit/README.md | 61 +++++++++++ effects/game-of-life/satblit/sat.ml | 133 ++++++++++++++++++++++++ effects/game-of-life/satblit/sat.mli | 31 ++++++ effects/game-of-life/satblit/satblit.ml | 132 +++++++++++++++++++++++ 5 files changed, 377 insertions(+) create mode 100644 effects/game-of-life/satblit/LICENSE create mode 100644 effects/game-of-life/satblit/README.md create mode 100644 effects/game-of-life/satblit/sat.ml create mode 100644 effects/game-of-life/satblit/sat.mli create mode 100644 effects/game-of-life/satblit/satblit.ml diff --git a/effects/game-of-life/satblit/LICENSE b/effects/game-of-life/satblit/LICENSE new file mode 100644 index 00000000..21791071 --- /dev/null +++ b/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. diff --git a/effects/game-of-life/satblit/README.md b/effects/game-of-life/satblit/README.md new file mode 100644 index 00000000..b32e4cde --- /dev/null +++ b/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 -o > 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 -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. + diff --git a/effects/game-of-life/satblit/sat.ml b/effects/game-of-life/satblit/sat.ml new file mode 100644 index 00000000..9435f8ba --- /dev/null +++ b/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 diff --git a/effects/game-of-life/satblit/sat.mli b/effects/game-of-life/satblit/sat.mli new file mode 100644 index 00000000..6c899344 --- /dev/null +++ b/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 diff --git a/effects/game-of-life/satblit/satblit.ml b/effects/game-of-life/satblit/satblit.ml new file mode 100644 index 00000000..a0f3dbf8 --- /dev/null +++ b/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