From fdae525c81636d257c7caef6ce75ebfec16ebe40 Mon Sep 17 00:00:00 2001
From: Peter Wu <peter@lekensteyn.nl>
Date: Wed, 14 Dec 2016 00:46:19 +0100
Subject: NeighborSum: finished 4a

Also uncommented questions (a, b, etc.)
---
 .../generate-neighborsum.py                        | 89 ++++++++++++++++++++++
 .../neighborsum-to-latex.py                        | 53 +++++++++++++
 2 files changed, 142 insertions(+)
 create mode 100755 integer_sum_from_neighbours/generate-neighborsum.py
 create mode 100755 integer_sum_from_neighbours/neighborsum-to-latex.py

(limited to 'integer_sum_from_neighbours')

diff --git a/integer_sum_from_neighbours/generate-neighborsum.py b/integer_sum_from_neighbours/generate-neighborsum.py
new file mode 100755
index 0000000..7e06e02
--- /dev/null
+++ b/integer_sum_from_neighbours/generate-neighborsum.py
@@ -0,0 +1,89 @@
+#!/usr/bin/env python
+import sys
+
+# i = 1..8
+n = 8
+steps = int(sys.argv[1])
+
+literals = []
+preds = []
+
+def fillin(cases, template_vars):
+    if type(cases) == str:
+        return cases.format(**template_vars)
+    return [template.format(**template_vars) for template in cases]
+
+# a. Repeat a number of steps, check in each step
+# if a_3 = a_7 is possible in that step.
+# Number a_i in step s is encoded as a_i_s.
+# The initial state is a_i_0.
+for step in range(steps + 1):
+    for i in range(1, n + 1):
+        literals += ["a{i}_{step}".format(**vars())]
+
+# Initial state, a_i_0 = i
+for i in range(1, n + 1):
+    preds += ["(= a{i}_0 {i})".format(i=i)]
+
+# Goal: have a_3 = a_7 in any step:
+preds += [
+    "(or %s)" % " ".join("(= a3_{i} a7_{i})".format(i=i)
+    for i in range(steps + 1))
+]
+
+# In each step, can sum neighbors (leaving others unchanged).
+for step in range(1, steps + 1):
+    # The first and last one cannot be changed. In a step, one can choose to
+    # change a_i for any i, leaving all other j (i != j) intact.
+    altpreds = []
+    for i in range(2, n):
+        laststep = step - 1
+        prev = i - 1
+        next = i + 1
+
+        # Require a'_i = a_{i-1} + a_{i+1}
+        statepreds = fillin([
+            "(= a{i}_{step} (+ a{prev}_{laststep} a{next}_{laststep}))"
+        ], vars())
+
+        # Require a'_j = a_j for i != j
+        for j in range(1, n + 1):
+            if i == j:
+                continue
+            statepreds += fillin([
+                "(= a{j}_{step} a{j}_{laststep})"
+            ], vars())
+        # All assignments must apply for this step.
+        altpreds += [
+            "(and %s)" % "\n".join(statepreds)
+        ]
+    preds += [
+        "(or",
+        "%s" % "\n".join(altpreds),
+        ")"
+    ]
+
+
+# Begin generator
+s = """(benchmark test.smt
+:logic QF_UFLIA
+:extrafuns (
+"""
+s += "\n".join("(%s Int)" % x for x in literals)
+s += """
+)
+:formula (and
+"""
+s += "\n".join(preds)
+s += """
+))
+"""
+
+try:
+    import sys
+    print(s)
+    # Hack to avoid printing a ugly error in case stdin of next pipe is closed.
+    sys.stdout.flush()
+    sys.stdout.close()
+except BrokenPipeError:
+    pass
diff --git a/integer_sum_from_neighbours/neighborsum-to-latex.py b/integer_sum_from_neighbours/neighborsum-to-latex.py
new file mode 100755
index 0000000..a920d9d
--- /dev/null
+++ b/integer_sum_from_neighbours/neighborsum-to-latex.py
@@ -0,0 +1,53 @@
+#!/usr/bin/env python3
+import re
+import sys
+
+# Maximum number of elements
+n = 8
+
+matrix = []
+
+for line in sys.stdin:
+    line = line.strip()
+    if line == "unsat":
+        sys.exit('unsat!')
+    if line == "sat":
+        continue
+    m = re.match(r'a(\d+)_(\d+) -> (\d+)', line)
+    var_number, step, value = map(int, m.groups())
+
+    # auto-detect size, extending matrix size if necessary.
+    while len(matrix) <= step:
+        matrix.append([None] * n)
+
+    matrix[step][var_number - 1] = value
+
+# List of cells that have changed since the previous iteration. Note that the
+# first row has no changed cell and therefore stores "None"
+changedCells = [None]
+for i, cells in enumerate(matrix):
+    if i == 0:
+        continue # skip first row
+    previousRow = matrix[i - 1]
+    for col, prevValue in enumerate(previousRow):
+        if cells[col] != prevValue:
+            # Found changed cell!
+            changedCells.append(col)
+            break
+
+line = "  "
+for col in range(len(matrix[0])):
+    line += " & $a_%d$" % (col + 1)
+line += r" \\"
+print(line)
+print(r"\hline")
+
+for step, cells in enumerate(matrix):
+    line = "%2d" % step
+    for col, value in enumerate(cells):
+        if changedCells[step] == col:
+            line += r" & \bf%2d" % value
+        else:
+            line += " & %5d" % value
+    line += r" \\"
+    print(line)
-- 
cgit v1.2.1