NeighborSum: add 4b (SMT soler part)

2 files changed, 15 insertions, 1 deletions

diff --git a/integer_sum_from_neighbours/generate-neighborsum.py b/integer_sum_from_neighbours/generate-neighborsum.py
index 7e06e02..14a8d23 100755
--- a/integer_sum_from_neighbours/generate-neighborsum.py
+++ b/integer_sum_from_neighbours/generate-neighborsum.py
@@ -1,9 +1,14 @@
 #!/usr/bin/env python
+# Usage for 4a (where 7 is the number of steps to run):
+#   $0 7 | z3 -smt -in
+# Usage for 4b:
+#   $0 7 b | z3 -smt -in
 import sys
 
 # i = 1..8
 n = 8
 steps = int(sys.argv[1])
+is_b = len(sys.argv) >= 3 and sys.argv[2] == 'b'
 
 literals = []
 preds = []
@@ -26,8 +31,12 @@ for i in range(1, n + 1):
     preds += ["(= a{i}_0 {i})".format(i=i)]
 
 # Goal: have a_3 = a_7 in any step:
+if not is_b:
+    goal = "(= a3_{i} a7_{i})"
+else:
+    goal = "(and (= a3_{i} a5_{i}) (= a5_{i} a7_{i}))"
 preds += [
-    "(or %s)" % " ".join("(= a3_{i} a7_{i})".format(i=i)
+    "(or %s)" % " ".join(goal.format(i=i)
     for i in range(steps + 1))
 ]
 
diff --git a/integer_sum_from_neighbours/neighborsum-to-latex.py b/integer_sum_from_neighbours/neighborsum-to-latex.py
index a920d9d..3fb3daa 100755
--- a/integer_sum_from_neighbours/neighborsum-to-latex.py
+++ b/integer_sum_from_neighbours/neighborsum-to-latex.py
@@ -34,6 +34,9 @@ for i, cells in enumerate(matrix):
             # Found changed cell!
             changedCells.append(col)
             break
+    else:
+        # Should not happen! Something got stuck?
+        changedCells.append(None)
 
 line = "  "
 for col in range(len(matrix[0])):
@@ -50,4 +53,6 @@ for step, cells in enumerate(matrix):
         else:
             line += " & %5d" % value
     line += r" \\"
+    if step > 0 and changedCells[step] is None:
+        line += " % unchanged!"
     print(line)