From ea6c5d96d4d5138ab7c19467b84381e50e37716f Mon Sep 17 00:00:00 2001 From: Kamil Zabielski <50334623+limakzi@users.noreply.github.com> Date: Fri, 14 Aug 2026 09:57:06 +0200 Subject: [PATCH] feat: Parelell prover9 --- .prover9/.gitignore | 2 + .prover9/README.md | 395 +++++++++++++++++++++++- .prover9/antimagma.in | 22 -- .prover9/antimagma.py | 677 ++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 1066 insertions(+), 30 deletions(-) create mode 100644 .prover9/.gitignore delete mode 100644 .prover9/antimagma.in create mode 100755 .prover9/antimagma.py diff --git a/.prover9/.gitignore b/.prover9/.gitignore new file mode 100644 index 0000000..fe72782 --- /dev/null +++ b/.prover9/.gitignore @@ -0,0 +1,2 @@ +antimagma.sbatch +generated/ diff --git a/.prover9/README.md b/.prover9/README.md index a05a3e6..0684ffe 100644 --- a/.prover9/README.md +++ b/.prover9/README.md @@ -1,18 +1,397 @@ ### Process of classification -For history and science repeatability purposes, we keep _clauses_ and _formulas_ for `mace4` / `prover9`. -Although, a complete antimagmas enumeration is already +For history and science repeatability purposes, we keep _clauses_ and _formulas_ for `mace4` / `prover9`. +Although, a complete antimagmas enumeration is already available in the package. -To classify all antimagmas, one can use `mace4`. +The formulas are no longer a single hand-written input, they are generated by +[`antimagma.py`](./antimagma.py), which splits the search over the deranged +diagonals of the multiplication table. An antimagma satisfies +`(x * y) * z != x * (y * z)`, hence `(x * x) * x != x * (x * x)` and `x * x != x`, +so the diagonal `x -> x * x` is fixed-point-free. Each deranged diagonal gives one +independent `mace4` search pinning the cells `x * x`, and every antimagma is found +by exactly one of them. + +### A full run, for n = 2 + +Order 2 has a single deranged diagonal, `x * x = (1 0)`, hence a single search. +`generate` writes the `slurm` batch job of the whole classification and logs the +command to continue with. ``` -mace4 < ./.prover9/antimagma.in +./.prover9/antimagma.py generate 2 --storage /tmp/antimagma ``` -To classify all antimagmas up to the isomorphism. +``` +▸ antimagma generate order 2 + order 2 1 deranged diagonal(s) + 2 square(s) on the diagonal 1 search(es) + job array 1 task(s) · 12:00:00 · 4G · dell + jobs search → isofilter → encode, each waiting for the one before + batch job /home/user/smallantimagmas/.prover9/antimagma.sbatch + storage /tmp/antimagma + +next + 1 submit the searches, the isofilter and the encoding + $ /home/user/smallantimagmas/.prover9/antimagma.sbatch + 2 read the tables of order 2 in gap, once the jobs are done + $ __SmallAntimagmaHelper.TablesDecode(2, ReadAsFunction("/tmp/antimagma/data/2/small_2.g.gz")()) +``` + +The batch job holds the diagonal of every search and the three stages of the +classification. + +``` +head -20 ./.prover9/antimagma.sbatch +``` +```bash +#!/bin/bash +# Generated by .prover9/antimagma.py -- do not edit. +# Classifies all antimagmas of order 2 as three dependent slurm jobs: one array +# task per deranged diagonal x -> x * x of the multiplication table, then +# isofilter, then the encoding of the tables for gap. +# +# /home/user/smallantimagmas/.prover9/antimagma.sbatch submit the three jobs +# /home/user/smallantimagmas/.prover9/antimagma.sbatch search run one search, ... +# /home/user/smallantimagmas/.prover9/antimagma.sbatch isofilter reduce the models ... +# /home/user/smallantimagmas/.prover9/antimagma.sbatch encode encode the tables for gap +# +#SBATCH --partition=dell +#SBATCH --job-name=antimagma-2 +#SBATCH --output=/tmp/antimagma/logs/%x-%j.log +#SBATCH --time=12:00:00 +#SBATCH --cpus-per-task=1 +set -euo pipefail + +batch="${ANTIMAGMA_BATCH:-/home/user/smallantimagmas/.prover9/antimagma.sbatch}" +storage="${ANTIMAGMA_STORAGE:-/tmp/antimagma}" +``` + +Running it submits the three jobs, each one waiting for the one before it. + +``` +./.prover9/antimagma.sbatch +``` + +``` +search 1001 +isofilter 1002 +encode 1003 ``` -mace4 < ./.prover9/antimagma.in | interpformat standard > antimagma.interps -isofilter < antimagma.interps > antimagma.interps_uptoisomorphism -``` \ No newline at end of file + +The array task of the search writes the `mace4` input of its diagonal. + +``` +cat /tmp/antimagma/2/2/antimagma_1_0.in +``` + +``` +% Generated by .prover9/antimagma.py -- do not edit. +% Antimagmas of order 2 with diagonal x * x = (1 0). + +assign(domain_size, 2). + +assign(max_megs, -1). +assign(max_models, -1). +assign(max_seconds, -1). + +assign(selection_order, 2). +assign(selection_measure, 4). + +set(negprop). +set(neg_assign). +set(neg_assign_near). + +set(neg_elim). + +set(print_models). +clear(lnh). + +formulas(assumptions). + all x all y all z (x * y) * z != x * (y * z). + + 0 * 0 = 1. + 1 * 1 = 0. +end_of_list. +``` + +It then runs `mace4` on it, into `antimagma_1_0.out`. The search is exhaustive, so +both antimagmas of order 2 show up, the second one being the transpose of the +first. + +``` +cat /tmp/antimagma/2/2/antimagma_1_0.out +``` + +``` +============================== MODEL ================================= + +interpretation( 2, [number=1, seconds=0], [ + + function(*(_,_), [ + 1, 0, + 1, 0 ]) +]). + +============================== end of model ========================== + +============================== MODEL ================================= + +interpretation( 2, [number=2, seconds=0], [ + + function(*(_,_), [ + 1, 1, + 0, 0 ]) +]). + +============================== end of model ========================== + +Exiting with 2 models. +``` + +The `isofilter` job then checks that every search left its models behind, reduces +the models of every group of squares up to the isomorphism, and gathers the +groups into the order and the orders into one file, into +`logs/antimagma-2-isofilter-1002.log`. + +``` +1 search(es) left their models in /tmp/antimagma +order 2, 2 square(s): 2 model(s) in /tmp/antimagma/2/2/antimagma-2-2.interps +order 2: 2 model(s) up to the isomorphism in /tmp/antimagma/2/antimagma-2.interps +order 2: 2 model(s) up to the isomorphism in /tmp/antimagma/antimagma.interps +``` + +And the `encode` job leaves one antimagma of order 2, the two being +anti-isomorphic, into `logs/antimagma-2-encode-1003.log`. + +``` +▸ antimagma encode order 2 + order 2 2 model(s) of 1 file(s) + up to (anti-)isomorphism 1 antimagma(s) + encoded into 1 table(s) + written to /tmp/antimagma/data/2/small_2.g.gz + +next + 1 read the tables of order 2 in gap + $ __SmallAntimagmaHelper.TablesDecode(2, ReadAsFunction("/tmp/antimagma/data/2/small_2.g.gz")()) +``` + +The whole run leaves the search, its models, the interpretations and the data +directory behind. + +``` +find /tmp/antimagma | sort +``` + +``` +/tmp/antimagma +/tmp/antimagma/2 +/tmp/antimagma/2/2 +/tmp/antimagma/2/2/antimagma-2-2.interps +/tmp/antimagma/2/2/antimagma_1_0.in +/tmp/antimagma/2/2/antimagma_1_0.out +/tmp/antimagma/2/antimagma-2.interps +/tmp/antimagma/antimagma.interps +/tmp/antimagma/data +/tmp/antimagma/data/2 +/tmp/antimagma/data/2/small_2.g.gz +/tmp/antimagma/logs +``` + +The multiplication table `[[2, 1], [2, 1]]` is the rows `[3, 3]`, as `[2, 1]` is +the third tuple of `EnumeratorOfTuples([1 .. 2], 2)`, packed into +`(3 - 1) * 4 + (3 - 1) = 10`, and stored as the single delta from zero. + +``` +zcat /tmp/antimagma/data/2/small_2.g.gz +``` + +``` +local result;result:=[10];return result; +``` + +Which `gap` decodes back into the antimagma of order 2. + +``` +gap> __SmallAntimagmaHelper.TablesDecode(2, ReadAsFunction("/tmp/antimagma/data/2/small_2.g.gz")()); +[ [ 3, 3 ] ] +gap> __SmallAntimagmaHelper.MultiplicationTableReverse([3, 3]); +[ [ 2, 1 ], [ 2, 1 ] ] +``` + +### The commands + +The script has two commands, `generate` and `encode`, and each of them logs the +command to continue with. `--storage` is the one directory everything a run +produces is kept in -- the searches, their models, the interpretations, the +`slurm` logs and the encoded tables. Only the batch job itself is written next to +the script, as `.prover9/antimagma.sbatch`, and `--output` moves it. + +#### 1. generate + +`generate` writes one file, the `slurm` batch job of the whole classification of +the given orders. + +``` +./.prover9/antimagma.py generate 4 +``` + +Running that file submits three jobs, each one waiting for the one before it, so +nothing is left to be run by hand. + +``` +./.prover9/antimagma.sbatch +``` + +| job | what it does | +| ----------- | ------------------------------------------------------------ | +| `search` | a job array of one task per deranged diagonal, running `mace4` | +| `isofilter` | reduces the models of every group of squares up to the isomorphism | +| `encode` | encodes the tables into the data directory, for `gap` | + +The jobs wait with `afterany`, on the one before them ending rather than on it +succeeding, so a search that fails leaves nothing pending forever. What a failed +search must not do is pass for an exhaustive classification, so `isofilter` and +`encode` both start by counting the models of the searches, and stop unless every +one of them is there. + +``` +only 80 of 81 search(es) left their models in /tmp/antimagma, see the logs of antimagma-4-search +``` + +Every array task of the search writes the `mace4` input of its diagonal, runs the +search and keeps the models it finds next to the input. Magmas are grouped by +their number of squares, that is by the number of distinct elements on the +diagonal, and named after the diagonal itself. + +``` +/ +├── 4/ +│ ├── 2/ +│ │ ├── antimagma_1_0_0_0.in +│ │ ├── antimagma_1_0_0_0.out +│ │ ├── ... +│ │ └── antimagma-4-2.interps +│ ├── 3/ +│ │ └── ... +│ ├── 4/ +│ │ └── ... +│ └── antimagma-4.interps +├── data/ +│ └── 4/ +│ └── small_4.g.gz +├── logs/ +└── antimagma.interps +``` + +The jobs are shaped by `--account`, `--partition`, `--time` and `--throttle`, the +number of searches running at once. They go to `dell` for +`12:00:00`, the time limit of that partition, as the searches are single threaded +and small; a search that needs longer belongs on `dell-long`. + +``` +./.prover9/antimagma.py generate 5 --partition dell-long --time 7-00:00:00 +``` + +`--mace4`, `--interpformat`, `--isofilter` and `--python` name the commands the +jobs run, for a cluster where they are not on the `PATH`. Several orders can share +one batch job, and `--output -` writes it to standard output instead. Once +submitted, the jobs read `ANTIMAGMA_BATCH` and `ANTIMAGMA_STORAGE` from the +environment, so a batch job can be moved, or made to fill another storage, without +being generated again. + +#### 2. isofilter + +The second job gathers the models of every diagonal and reduces them up to the +isomorphism, which keeps the work of the encoding small. It runs one group of +squares at a time, over the models of the diagonals sharing a number of distinct +squares, and gathers the results afterwards. + +A magma and its relabellings have the same order and the same number of squares, +so no two models of different groups are ever isomorphic: reducing the groups on +their own loses nothing, and `isofilter` never runs over more models than the +group it is given. The gathering is then a concatenation, of the groups into the +order and of the orders into the one file the encoding reads. + +``` +/ +├── 4/ +│ ├── 2/ +│ │ └── antimagma-4-2.interps the models of order 4 with 2 squares +│ ├── 3/ +│ │ └── antimagma-4-3.interps the models of order 4 with 3 squares +│ ├── 4/ +│ │ └── antimagma-4-4.interps the models of order 4 with 4 squares +│ └── antimagma-4.interps the models of order 4 +├── 5/ +│ └── antimagma-5.interps the models of order 5 +└── antimagma.interps the models of every order, what encode reads +``` + +It is the `isofilter` stage of the batch job, and runs on its own as + +``` +./.prover9/antimagma.sbatch isofilter +``` + +#### 3. encode + +The third job turns the models into an `` directory `gap` is able to read. +It reads `antimagma.interps` left by `isofilter`, falling back to the +`antimagma-.interps` of the order, then to the +`antimagma--.interps` of its groups, and then to the models of +the searches themselves, so it also stands on its own. + +``` +./.prover9/antimagma.py encode 4 --storage /tmp/antimagma +``` + +``` +/data/ +└── 4/ + └── small_4.g.gz +``` + +Antimagmas are counted up to the isomorphism and the anti-isomorphism, a magma +and its transpose being the same antimagma, so `encode` keeps the least +relabelling of every model it reads -- of the 10 isomorphism classes of order 3, +the 5 the package stores. `--labelled` keeps every model instead. + +The counts to expect are the ones `NrSmallAntimagmas` gives, so the whole run is +worth checking against them. + +| order | models found | antimagmas encoded | +| ----- | ------------ | ------------------ | +| 2 | 2 | 1 | +| 3 | 52 | 5 | +| 4 | 421560 | 8891 | + +Every multiplication table is then converted row by row into a position in +`EnumeratorOfTuples([1 .. n], n)`, packed into a single integer in base `n ^ n`, +and the sorted integers are stored as the differences between the consecutive +ones -- the encoding of `__SmallAntimagmaHelper.TablesEncode`, so that + +``` +gap> __SmallAntimagmaHelper.TablesDecode(4, ReadAsFunction("./data/4/small_4.g.gz")()); +``` + +gives the tables back in row form. + +#### Options + +The diagonal of an antimagma need not be a permutation -- 48 of the 52 antimagmas +of order 3 have a non-injective diagonal -- so the search is split over all +`(n - 1)^n` fixed-point-free diagonals. `--bijective` narrows it down to the +derangements, that is to the `//` group of the antimagmas +with a bijective diagonal. + +Both commands log what they did and the commands to continue with to standard +error, in colour whenever it is a terminal, so that standard output stays free +for `generate --output -`. `--color never`, `--color always` and `NO_COLOR` in the +environment override the detection. + +The least number heuristic, `set(lnh)`, is off in the generated inputs, so that +each search enumerates its diagonal exhaustively and the model counts of the +searches add up; `isofilter` reduces afterwards, across the diagonals of a group +of squares at once, and `encode` across the orders. Pass `--lnh` to keep it on. diff --git a/.prover9/antimagma.in b/.prover9/antimagma.in deleted file mode 100644 index b2de91a..0000000 --- a/.prover9/antimagma.in +++ /dev/null @@ -1,22 +0,0 @@ -assign(domain_size, 2). -assign(increment, 1). - -assign(max_megs, -1). -assign(max_models, -1). -assign(max_seconds, -1). - -assign(selection_order, 2). -assign(selection_measure, 4). - -set(negprop). -set(neg_assign). -set(neg_assign_near). - -set(neg_elim). - -set(print_models). -set(lnh). - -formulas(assumptions). - all x all y all z (x * y) * z != x * (y * z). -end_of_list. diff --git a/.prover9/antimagma.py b/.prover9/antimagma.py new file mode 100755 index 0000000..9ef0675 --- /dev/null +++ b/.prover9/antimagma.py @@ -0,0 +1,677 @@ +#!/usr/bin/env python3 +"""Search for all antimagmas with mace4, split over the deranged diagonals. + +An antimagma is a magma satisfying (x * y) * z != x * (y * z) for all x, y, z. +Taking x = y = z gives (x * x) * x != x * (x * x), so x * x != x: the diagonal +x -> x * x of an antimagma is a fixed-point-free ("deranged") map of the domain. + + generate write the slurm batch job, one array task per deranged diagonal + encode encode the models found into a directory gap is able to read + +Rather than one mace4 search per order, generate writes a single bash file +scheduling one search per deranged diagonal, each of them pinning the cells +x * x of the multiplication table. The searches are independent, so the job +array runs them in parallel, and every antimagma is found by exactly one of them. +Each command logs the ones to continue with. + +The diagonal of an antimagma need not be a permutation -- 48 of the 52 +antimagmas of order 3 have a non-injective diagonal -- so the split ranges over +all (n - 1)^n fixed-point-free maps by default. Pass --bijective to restrict it +to the derangements of the domain, which searches for antimagmas with a +bijective diagonal only. + +Everything a run produces lives in the storage, --storage, and only the batch +job itself is written next to this script. The searches write their inputs and +their models there, grouped by the number of squares of the magma, that is by the +number of distinct elements on the diagonal; encode turns those models into +/data, one directory gap reads. + + ///antimagma_.in + ///antimagma_.out + ///antimagma--.interps + //antimagma-.interps + /antimagma.interps + /logs/ + /data//small_.g.gz + +The number of squares is an invariant of the isomorphism, as is the order, so +isofilter reduces one group at a time and its results are only gathered +afterwards: many small runs rather than one over every model found. + +encode keeps one model per antimagma, up to the isomorphism and the +anti-isomorphism, and holds the multiplication tables the way the package stores +them: every table packed into an integer in base n^n, sorted, and kept as the +differences between the consecutive ones. +""" + +from __future__ import annotations + +import argparse +import gzip +import itertools +import os +import re +import sys +from collections import Counter +from pathlib import Path + +# Everything a run produces lives in the storage, the batch job itself next to +# this script. +DEFAULT_STORAGE = Path(__file__).parent / "generated" +DEFAULT_BATCH = Path(__file__).parent / "antimagma.sbatch" + +# slurm rejects job arrays with an index above MaxArraySize, 1001 by default. +MAX_ARRAY_SIZE = 1001 + +# The searches are single threaded and small, so they go to the plain cpu nodes. +# dell caps a job at 12 hours; dell-long, 14 days, takes the searches that need +# more than that. +DEFAULT_PARTITION = "dell" +DEFAULT_TIME = "12:00:00" + +# The multiplication table of a model of mace4, cell by cell, row by row. +INTERPRETATION = re.compile(r"interpretation\(\s*(\d+).*?function\(\s*\*\(_,_\)\s*,\s*\[(.*?)\]", re.DOTALL) + +BATCH_TEMPLATE = """\ +#!/bin/bash +# Generated by .prover9/antimagma.py -- do not edit. +# Classifies all antimagmas of @ORDERS@ as three dependent slurm jobs: one array +# task per deranged diagonal x -> x * x of the multiplication table, then +# isofilter, then the encoding of the tables for gap. +# +# @BATCH@ submit the three jobs +# @BATCH@ search run one search, of $SLURM_ARRAY_TASK_ID +# @BATCH@ isofilter reduce the models of every group up to the isomorphism +# @BATCH@ encode encode the tables for gap +# +@DIRECTIVES@ +set -euo pipefail + +batch="${ANTIMAGMA_BATCH:-@BATCH@}" +storage="${ANTIMAGMA_STORAGE:-@STORAGE@}" + +orders=(@ORDERS_LIST@) + +# The order and the deranged diagonal of every search. +searches=( +@SEARCHES@ +) + +# The order and the number of squares of every group the searches fill, one run +# of isofilter each. +groups=( +@GROUPS@ +) + +# The jobs after the searches run whatever the searches ended as, so the models +# of every one of them have to be there before anything is reduced or encoded. +complete_searches() { + local found + found=$(find "$storage" -name '*.out' | wc -l | tr -d '[:space:]') + if [ "$found" -ne "${#searches[@]}" ]; then + echo "only $found of ${#searches[@]} search(es) left their models in $storage," \ + "see the logs of @NAME@-search" >&2 + return 1 + fi + echo "${#searches[@]} search(es) left their models in $storage" +} + +case "${1:-submit}" in + +submit) + # The jobs wait for the one before them to end, whatever its exit code, so a + # search that fails leaves nothing pending forever; the isofilter checks that + # every search did leave its models behind before the encoding goes on. + searching=$(sbatch --parsable --job-name=@NAME@-search --array=@ARRAY@ "$batch" search) + searching=${searching%%;*} + filtering=$(sbatch --parsable --job-name=@NAME@-isofilter --dependency=afterany:$searching "$batch" isofilter) + filtering=${filtering%%;*} + encoding=$(sbatch --parsable --job-name=@NAME@-encode --dependency=afterany:$filtering "$batch" encode) + echo "search $searching" + echo "isofilter $filtering" + echo "encode ${encoding%%;*}" + ;; + +search) + search=(${searches[$SLURM_ARRAY_TASK_ID]}) + order="${search[0]}" + diagonal=("${search[@]:1}") + + # Magmas are grouped by their number of squares, the distinct elements of the + # diagonal, and named after the diagonal itself. + squares="$(printf '%s\\n' "${diagonal[@]}" | sort -u | wc -l | tr -d '[:space:]')" + name="$(IFS=_; echo "${diagonal[*]}")" + group="$storage/$order/$squares" + mkdir -p "$group" + + input="$group/antimagma_$name.in" + { + cat < "$input" + + status=0 + @MACE4@ -f "$input" > "${input%.in}.out" || status=$? + + # mace4 exits with 0 once max_models models were found and with 2 once the + # search space was exhausted; both are normal terminations for these searches. + case "$status" in + 0 | 2) exit 0 ;; + *) exit "$status" ;; + esac + ;; + +isofilter) + complete_searches + + # A magma and its relabellings have the same order and the same number of + # squares, so no two models of different groups are ever isomorphic: every + # group is reduced on its own, which keeps each run of isofilter over the + # models of one squares count alone, and the results are gathered afterwards. + gathered=() + for order in "${orders[@]}"; do + reduced=() + for group in "${groups[@]}"; do + entry=($group) + [ "${entry[0]}" = "$order" ] || continue + squares="${entry[1]}" + + directory="$storage/$order/$squares" + interps="$directory/antimagma-$order-$squares.interps" + find "$directory" -name '*.out' -exec cat {} + | @INTERPFORMAT@ standard | @ISOFILTER@ > "$interps" + echo "order $order, $squares square(s): $(grep -c 'interpretation(' "$interps") model(s) in $interps" + reduced+=("$interps") + done + + # The groups of one order, then the orders themselves, are only concatenated: + # both are reduced already, and neither holds a model isomorphic to one of + # another. + interps="$storage/$order/antimagma-$order.interps" + cat "${reduced[@]}" > "$interps" + echo "order $order: $(grep -c 'interpretation(' "$interps") model(s) up to the isomorphism in $interps" + gathered+=("$interps") + done + + interps="$storage/antimagma.interps" + cat "${gathered[@]}" > "$interps" + echo "@ORDERS@: $(grep -c 'interpretation(' "$interps") model(s) up to the isomorphism in $interps" + ;; + +encode) + complete_searches + + @PYTHON@ "@SCRIPT@" encode "${orders[@]}" --storage "$storage" --color never + ;; + +*) + echo "usage: $batch [submit | search | isofilter | encode]" >&2 + exit 64 + ;; + +esac +""" + +MACE4_SETTINGS = """\ +assign(max_megs, -1). +assign(max_models, -1). +assign(max_seconds, -1). + +assign(selection_order, 2). +assign(selection_measure, 4). + +set(negprop). +set(neg_assign). +set(neg_assign_near). + +set(neg_elim). + +set(print_models).\ +""" + +ANTIASSOCIATIVITY = "all x all y all z (x * y) * z != x * (y * z)." + + +class Log: + """Reports what a command does to standard error, in colour when it can. + + Standard output is left to the batch job of generate --output -, so every + line of the log, the errors included, goes to standard error. + """ + + STYLES = { + "bold": "\033[1m", + "dim": "\033[2m", + "red": "\033[31m", + "green": "\033[32m", + "yellow": "\033[33m", + "blue": "\033[34m", + "cyan": "\033[36m", + "reset": "\033[0m", + } + + NAME_WIDTH = 12 + ITEM_WIDTH = 32 + + def __init__(self, colour: bool) -> None: + self.colour = colour + + def paint(self, text: str, *styles: str) -> str: + if not self.colour: + return text + return "".join(self.STYLES[style] for style in styles) + text + self.STYLES["reset"] + + def write(self, line: str = "") -> None: + print(line, file=sys.stderr) + + def title(self, command: str, subject: str) -> None: + """Announce the command, as `▸ antimagma generate order 3, 4`.""" + self.write() + self.write( + f"{self.paint('▸', 'blue')} {self.paint('antimagma', 'bold')}" + f" {self.paint(command, 'cyan', 'bold')} {self.paint(subject, 'dim')}" + ) + + def field(self, name: str, value: str) -> None: + self.write(f" {self.paint(f'{name} '.ljust(self.NAME_WIDTH), 'dim')}{value}") + + def item(self, name: str, value: str) -> None: + self.write(f" {f'{name} '.ljust(self.ITEM_WIDTH)}{value}") + + def count(self, amount: int, unit: str) -> str: + return f"{self.paint(str(amount), 'yellow', 'bold')} {unit}" + + def step(self, number: int, description: str, command: str) -> None: + self.write(f" {self.paint(str(number), 'blue', 'bold')} {description}") + self.write(f" {self.paint(f'$ {command}', 'green')}") + + def warning(self, message: str) -> None: + self.write(f" {self.paint('!', 'yellow', 'bold')} {self.paint(message, 'yellow')}") + + def fail(self, message: str) -> SystemExit: + return SystemExit(f" {self.paint('✗', 'red', 'bold')} {self.paint(message, 'red')}") + + +def colourful(choice: str) -> bool: + """Tell whether the log may be coloured, honouring NO_COLOR and dumb terminals.""" + if choice != "auto": + return choice == "always" + return sys.stderr.isatty() and "NO_COLOR" not in os.environ and os.environ.get("TERM") != "dumb" + + +def deranged_diagonals(order: int, bijective: bool = False): + """Yield every fixed-point-free diagonal x -> x * x on {0, ..., order - 1}.""" + if bijective: + candidates = itertools.permutations(range(order)) + else: + candidates = itertools.product(*([e for e in range(order) if e != x] for x in range(order))) + return (d for d in candidates if all(image != x for x, image in enumerate(d))) + + +def searches(orders: list[int], bijective: bool = False) -> list[tuple[int, tuple[int, ...]]]: + """List the searches, one per order and deranged diagonal of that order.""" + return [ + (order, diagonal) + for order in orders + for diagonal in sorted(deranged_diagonals(order, bijective=bijective), key=lambda d: (len(set(d)), d)) + ] + + +def groups_of(scheduled: list[tuple[int, tuple[int, ...]]]) -> list[tuple[int, int]]: + """List the groups the searches fill, by order and number of squares. + + The number of squares of a magma, the distinct elements of its diagonal, is + an invariant of the isomorphism, so a group is reduced on its own. + """ + return sorted({(order, len(set(diagonal))) for order, diagonal in scheduled}) + + +def job_name(orders: list[int]) -> str: + """Name the jobs of the batch, the stage being appended when they are submitted.""" + return f"antimagma-{orders[0]}" if len(orders) == 1 else "antimagma" + + +def render_batch(scheduled: list[tuple[int, tuple[int, ...]]], options: argparse.Namespace) -> str: + """Render the slurm batch job searching, filtering and encoding the antimagmas.""" + orders = sorted({order for order, _ in scheduled}) + name = job_name(orders) + + directives = [] + if options.account: + directives.append(f"#SBATCH --account={options.account}") + if options.partition: + directives.append(f"#SBATCH --partition={options.partition}") + directives += [ + # The stages are submitted with a job name of their own, %x below. + f"#SBATCH --job-name={name}", + f"#SBATCH --output={options.storage}/logs/%x-%j.log", + f"#SBATCH --time={options.time}", + # mace4 is a single threaded search, one core per job is enough. + "#SBATCH --cpus-per-task=1", + ] + + listing = "\n".join( + ' "{}"'.format(" ".join(str(element) for element in (order, *diagonal))) for order, diagonal in scheduled + ) + grouping = "\n".join(f' "{order} {squares}"' for order, squares in groups_of(scheduled)) + replacements = { + "@ORDERS@": "order " + ", ".join(str(order) for order in orders), + "@ORDERS_LIST@": " ".join(str(order) for order in orders), + "@DIRECTIVES@": "\n".join(directives), + "@NAME@": name, + "@ARRAY@": f"0-{len(scheduled) - 1}" + (f"%{options.throttle}" if options.throttle else ""), + "@BATCH@": str(options.batch), + "@STORAGE@": str(options.storage), + "@SEARCHES@": listing, + "@GROUPS@": grouping, + "@SETTINGS@": MACE4_SETTINGS, + "@LNH@": "set" if options.lnh else "clear", + "@ANTIASSOCIATIVITY@": ANTIASSOCIATIVITY, + "@MACE4@": options.mace4, + "@INTERPFORMAT@": options.interpformat, + "@ISOFILTER@": options.isofilter, + "@PYTHON@": options.python, + "@SCRIPT@": str(Path(__file__).resolve()), + } + batch = BATCH_TEMPLATE + for placeholder, value in replacements.items(): + batch = batch.replace(placeholder, value) + return batch + + +def models_of(order: int, directory: Path) -> list[Path]: + """List the files holding the models of one order. + + The interpretations left by isofilter are preferred over the models of the + searches themselves, so that encode reduces up to isomorphism whenever the + step has been run: the ones of every order first, then the ones of that order + alone, then the ones of its groups of squares, then the models of its + searches. + """ + for interps in (directory / "antimagma.interps", directory / str(order) / f"antimagma-{order}.interps"): + if interps.exists(): + return [interps] + grouped = sorted((directory / str(order)).glob(f"*/antimagma-{order}-*.interps")) + return grouped or sorted((directory / str(order)).rglob("*.out")) + + +def data_of(order: int, storage: Path) -> Path: + """Name the file of one order gap reads, in the data of the storage.""" + return storage / "data" / str(order) / f"small_{order}.g.gz" + + +def parse_models(text: str, order: int): + """Yield the multiplication table of every model mace4 printed.""" + for domain_size, cells in INTERPRETATION.findall(text): + if int(domain_size) != order: + continue + values = [int(cell) for cell in cells.replace(",", " ").split()] + if len(values) != order * order: + raise ValueError(f"a model of order {order} holds {len(values)} cell(s)") + yield [values[x * order : (x + 1) * order] for x in range(order)] + + +def canonical_table(table: list[list[int]]) -> tuple[tuple[int, ...], ...]: + """Return the least relabelling of a multiplication table, transpose included. + + The package counts antimagmas up to the isomorphism and the anti-isomorphism, + so a magma, its relabellings and its transpose share one canonical table: of + the 10 isomorphism classes of order 3, it keeps the 5 the package stores. + """ + order = len(table) + transposed = [list(column) for column in zip(*table)] + candidates = [] + for magma in (table, transposed): + for sigma in itertools.permutations(range(order)): + inverse = [0] * order + for element, image in enumerate(sigma): + inverse[image] = element + candidates.append( + tuple(tuple(sigma[magma[inverse[x]][inverse[y]]] for y in range(order)) for x in range(order)) + ) + return min(candidates) + + +def convert_table(table: list[list[int]]) -> list[int]: + """Convert a multiplication table into its row form. + + A row becomes its position in EnumeratorOfTuples([1 .. n], n), the conversion + of __SmallAntimagmaHelper.MultiplicationTableConvert. + """ + order = len(table) + return [sum(value * order ** (order - 1 - x) for x, value in enumerate(row)) + 1 for row in table] + + +def encode_tables(order: int, tables: list[list[int]]) -> list[int]: + """Encode the tables in row form the way the package stores them. + + A table is packed into a single integer in base n^n, the encoding of + __SmallAntimagmaHelper.TablesEncode, and the sorted integers are kept as the + differences between the consecutive ones. + """ + base = order**order + numbers = sorted({sum((row - 1) * base ** (order - 1 - x) for x, row in enumerate(table)) for table in tables}) + return [number - previous for number, previous in zip(numbers, [0] + numbers)] + + +def render_data(deltas: list[int]) -> str: + """Render the encoded tables as the gap file the package reads.""" + listing = ",".join(str(delta) for delta in deltas) + return f"local result;result:=[{listing}];return result;" + + +def subject_of(orders: list[int]) -> str: + """Name the orders a command works on, for the title of the log.""" + return "order " + ", ".join(str(order) for order in orders) + + +def generate(options: argparse.Namespace, log: Log) -> int: + """Write the slurm batch job searching for the antimagmas of the orders.""" + orders = sorted(set(options.orders)) + scheduled = searches(orders, bijective=options.bijective) + batch = render_batch(scheduled, options) + to_stdout = str(options.output) == "-" + + if to_stdout: + print(batch, end="") + else: + options.output.parent.mkdir(parents=True, exist_ok=True) + options.output.write_text(batch) + options.output.chmod(0o755) + + # slurm opens the log of a job itself, so its directory has to be there + # before the batch job is scheduled. + (options.storage / "logs").mkdir(parents=True, exist_ok=True) + + log.title("generate", subject_of(orders)) + for order in orders: + grouped = Counter(len(set(diagonal)) for scheduled_order, diagonal in scheduled if scheduled_order == order) + log.field(f"order {order}", log.count(sum(grouped.values()), "deranged diagonal(s)")) + for squares in sorted(grouped): + log.item(f"{squares} square(s) on the diagonal", log.count(grouped[squares], "search(es)")) + + shape = [f"{len(scheduled)} task(s)", f"{options.time}"] + if options.throttle: + shape.insert(1, f"{options.throttle} at once") + if options.partition: + shape.append(options.partition) + log.field("job array", log.paint(" · ".join(shape), "dim")) + log.field("jobs", log.paint("search → isofilter → encode, each waiting for the one before", "dim")) + log.field( + "isofilter", + log.count(len(groups_of(scheduled)), "group(s) of squares") + + log.paint(", reduced on their own then gathered", "dim"), + ) + log.field("batch job", str(options.batch) if not to_stdout else log.paint("standard output", "dim")) + log.field("storage", str(options.storage)) + if len(scheduled) > MAX_ARRAY_SIZE: + log.warning(f"more than {MAX_ARRAY_SIZE} tasks, which slurm accepts only with a raised MaxArraySize") + if to_stdout: + return 0 + + log.write() + log.write(log.paint("next", "bold")) + steps = itertools.count(1) + log.step(next(steps), "submit the searches, the isofilter and the encoding", str(options.batch)) + for order in orders: + data = data_of(order, options.storage) + log.step( + next(steps), + f"read the tables of order {order} in gap, once the jobs are done", + f'__SmallAntimagmaHelper.TablesDecode({order}, ReadAsFunction("{data}")())', + ) + log.write() + return 0 + + +def encode(options: argparse.Namespace, log: Log) -> int: + """Encode the models found into a directory gap is able to read.""" + orders = sorted(set(options.orders)) + log.title("encode", subject_of(orders)) + + for order in orders: + sources = models_of(order, options.storage) + if not sources: + raise log.fail(f"no model of order {order} in {options.storage}, run the searches first") + + models = [table for source in sources for table in parse_models(source.read_text(), order)] + if not models: + raise log.fail(f"the {len(sources)} file(s) of order {order} in {options.storage} hold no model") + + if options.labelled: + tables = [convert_table(model) for model in models] + else: + tables = [convert_table([list(row) for row in table]) for table in {canonical_table(m) for m in models}] + deltas = encode_tables(order, tables) + + data = data_of(order, options.storage) + data.parent.mkdir(parents=True, exist_ok=True) + # mtime 0 keeps the encoding of a set of models reproducible. + with gzip.GzipFile(data, "wb", mtime=0) as compressed: + compressed.write(render_data(deltas).encode()) + + log.field(f"order {order}", log.count(len(models), "model(s)") + f" of {log.count(len(sources), 'file(s)')}") + if not options.labelled: + log.item("up to (anti-)isomorphism", log.count(len(tables), "antimagma(s)")) + log.item("encoded into", log.count(len(deltas), "table(s)")) + log.item("written to", str(data)) + + log.write() + log.write(log.paint("next", "bold")) + for number, order in enumerate(orders, start=1): + data = data_of(order, options.storage) + log.step( + number, + f"read the tables of order {order} in gap", + f'__SmallAntimagmaHelper.TablesDecode({order}, ReadAsFunction("{data}")())', + ) + log.write() + return 0 + + +def parse_args(argv: list[str] | None = None) -> argparse.Namespace: + parser = argparse.ArgumentParser( + description=__doc__, + formatter_class=argparse.RawDescriptionHelpFormatter, + ) + commands = parser.add_subparsers(dest="command", required=True) + + common = argparse.ArgumentParser(add_help=False) + common.add_argument("orders", type=int, nargs="+", help="orders of the antimagmas to search for") + common.add_argument( + "--storage", + type=Path, + default=DEFAULT_STORAGE, + help=f"directory everything a run produces is kept in (default: {DEFAULT_STORAGE})", + ) + common.add_argument( + "--color", + "--colour", + dest="colour", + choices=("auto", "always", "never"), + default="auto", + help="colour of the log (default: auto, on when it is a terminal)", + ) + + batch = commands.add_parser( + "generate", + parents=[common], + help="write the slurm batch job searching for the antimagmas", + description="Write the slurm batch job, one array task per deranged diagonal.", + ) + batch.add_argument( + "--output", + type=Path, + default=DEFAULT_BATCH, + help=f"generated batch job, - for stdout (default: {DEFAULT_BATCH})", + ) + batch.add_argument( + "--bijective", + action="store_true", + help="split over the derangements only, skipping the non-bijective diagonals", + ) + batch.add_argument("--lnh", action="store_true", help="keep the least number heuristic on") + batch.add_argument("--account", help="account charged for the batch job") + batch.add_argument( + "--partition", + default=DEFAULT_PARTITION, + help=f"partition the batch job is submitted to (default: {DEFAULT_PARTITION})", + ) + batch.add_argument( + "--time", + default=DEFAULT_TIME, + help=f"time limit of a single search (default: {DEFAULT_TIME}, the limit of {DEFAULT_PARTITION})", + ) + batch.add_argument("--throttle", type=int, default=0, help="number of searches running at once (default: unlimited)") + batch.add_argument("--mace4", default="mace4", help="mace4 command of the batch job (default: mace4)") + batch.add_argument("--interpformat", default="interpformat", help="interpformat command (default: interpformat)") + batch.add_argument("--isofilter", default="isofilter", help="isofilter command (default: isofilter)") + batch.add_argument("--python", default="python3", help="python running the encoding (default: python3)") + + tables = commands.add_parser( + "encode", + parents=[common], + help="encode the models found into a directory gap is able to read", + description="Encode the multiplication tables of the models found, as the package stores them.", + ) + tables.add_argument( + "--labelled", + action="store_true", + help="encode every model found, without reducing up to isomorphism and anti-isomorphism", + ) + return parser.parse_args(argv) + + +def main(argv: list[str] | None = None) -> int: + args = parse_args(argv) + log = Log(colourful(args.colour)) + for order in args.orders: + if order < 2: + raise log.fail(" must be greater than or equal to 2") + + args.storage = args.storage.resolve() + if args.command == "encode": + return encode(args, log) + + # The batch job submits its own stages, so it has to know where it lives even + # when it is written to standard output. + args.batch = DEFAULT_BATCH.resolve() if str(args.output) == "-" else args.output.resolve() + return generate(args, log) + + +if __name__ == "__main__": + sys.exit(main())