Puzzled Pint puzzle solver
change
commit fdbc3cde472697ed2aef579d8a1c32cee3a7a233
author Alpha Chen <alpha@kejadlen.dev>
date
parent 10a0d69b
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..3c3629e
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+node_modules
diff --git a/sentient/puzzled-pint/elementary-my-dear.snt b/sentient/puzzled-pint/elementary-my-dear.snt
new file mode 100644
index 0000000..66c7a0b
--- /dev/null
+++ b/sentient/puzzled-pint/elementary-my-dear.snt
@@ -0,0 +1,28 @@
+array5<array5<int5>> X;
+
+X.each(function (row) {
+  row.each(function (cell) {
+    invariant cell.between?(1, 5);
+  });
+});
+
+function valid?(ary) {
+  invariant ary.uniq?;
+};
+
+X.each(*valid?);
+X.transpose.each(*valid?);
+
+invariant X[0][1] == 2;
+invariant X[1][3] == 2;
+invariant X[2][2] == 2;
+invariant X[3][0] == 2;
+invariant X[4][4] == 2;
+
+invariant (X[0][0] * X[0][1]) + X[0][2] - X[0][3] + X[0][4] == 4;
+invariant (X[1][0] + X[1][1] - X[1][2]) * X[1][3] + X[1][4] == 2;
+invariant (X[2][0] + X[2][1]) * X[2][2] - X[2][3] + X[2][4] == 13;
+invariant  X[3][0] * X[3][1] + X[3][2] - X[3][3] + X[3][4] == 11;
+invariant (X[4][0] + X[4][1] - X[4][2] + X[4][3]) * X[4][4] == 14;
+
+expose X;