add Sentient solver for speedbacks
change
commit 9aef576607713ce4d018eaa92a11a0b6687feacb
author Alpha Chen <alpha@kejadlen.dev>
date
parent fdbc3cde
diff --git a/sentient/speedback.snt b/sentient/speedback.snt
new file mode 100644
index 0000000..e88afef
--- /dev/null
+++ b/sentient/speedback.snt
@@ -0,0 +1,20 @@
+array7<array8<int4>> X;
+
+X.each(function (row) {
+  row.each(function (cell) {
+    invariant cell.between?(0, 8);
+  });
+});
+
+invariant X.all?(*uniq?);
+X.transpose.all?(*uniq?);
+
+pairs = [];
+X.each(function^ (row) {
+  row.eachSlice(2, function^ (pair) {
+    pairs = pairs.push(pair);
+  });
+});
+invariant pairs.uniq?;
+
+expose X;