From a9a010623c75610cafe67d4ce7accc678f94937b Mon Sep 17 00:00:00 2001
From: Peter Wu <peter@lekensteyn.nl>
Date: Wed, 11 Jan 2017 18:23:31 +0100
Subject: WIP food delivery

---
 food_delivery/food-to-table.py |  49 ++++++++++++++++
 food_delivery/generate-food.py | 129 +++++++++++++++++++++++++++++++++++++++++
 2 files changed, 178 insertions(+)
 create mode 100755 food_delivery/food-to-table.py
 create mode 100755 food_delivery/generate-food.py

diff --git a/food_delivery/food-to-table.py b/food_delivery/food-to-table.py
new file mode 100755
index 0000000..c054f0c
--- /dev/null
+++ b/food_delivery/food-to-table.py
@@ -0,0 +1,49 @@
+#!/usr/bin/env python3
+import re
+import sys
+
+# Maximum number of elements
+n = 5
+
+matrix = []
+nextNodes = {}
+
+for line in sys.stdin:
+    line = line.strip()
+    if line == "unsat":
+        sys.exit('unsat!')
+    if line == "sat":
+        continue
+    m = re.match(r's(\d+)_(\d+) -> (\d+)', line)
+    if m:
+        villagenr, step, value = map(int, m.groups())
+
+        # auto-detect size, extending matrix size if necessary.
+        while len(matrix) <= step:
+            matrix.append([None] * n)
+
+        matrix[step][villagenr] = value
+    else:
+        m = re.match(r'l(\d+) -> (\d+)', line)
+        step, value = map(int, m.groups())
+        nextNodes[step] = value
+
+if False:
+    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 = "%3d" % step
+    for col, value in enumerate(cells):
+        if nextNodes.get(step + 1) == col:
+            #line += r" & \bf%2d" % value
+            line += r" & %4d." % value
+        else:
+            line += " & %5d" % value
+    line += r" & %s \\" % "SABCD"[nextNodes[step]]
+    #line += r" \\"
+    print(line)
diff --git a/food_delivery/generate-food.py b/food_delivery/generate-food.py
new file mode 100755
index 0000000..0e0295d
--- /dev/null
+++ b/food_delivery/generate-food.py
@@ -0,0 +1,129 @@
+#!/usr/bin/env python3
+import sys
+
+# Number of steps
+m = 64 if len(sys.argv) <= 1 else int(sys.argv[1])
+truck_capacity = 240 if len(sys.argv) <= 2 else int(sys.argv[2])
+
+states = "SABCD"
+
+capacities = [
+None,
+120,
+160,
+100,
+120
+]
+
+# Possible transitions from x to y and the travel cost c.
+# trans[x, y] = c
+# trans[x, y] = None  if there is no such transition.
+trans = {}
+trans[0, 1] = 15
+trans[0, 3] = 15
+trans[1, 2] = 17
+trans[1, 3] = 12
+trans[2, 3] = 10
+trans[2, 4] = 20
+trans[3, 4] = 20
+# and the other direction
+for (x, y), c in dict(trans).items():
+    trans[y, x] = c
+
+if False:
+    # Print table for debugging
+    for x in range(len(states)):
+        for y in range(len(states)):
+            c = trans.get((x, y))
+            if c:
+                print(" %2d " % c, end="")
+            else:
+                print(" -- ", end="")
+        print("")
+
+def fillin(cases, template_vars):
+    if type(cases) == str:
+        return cases.format(**template_vars)
+    return [template.format(**template_vars) for template in cases]
+
+literals = []
+preds = []
+
+# s0_j is the current stock of the truck
+# s1_j is the current stock of village 1
+for j in range(m + 1):
+    literals += ["s%d_%d" % (i, j) for i in range(len(states))]
+    literals += ["l%d" % j]
+
+# Initially the villages have 80 food,
+# the truck is at the supply (l=0),
+# and the truck is fully loaded
+for i in range(1, len(states)):
+    preds += ["(= s%d_0 80)" % i]
+preds += ["(= l0 0)"]
+preds += ["(= s0_0 %d)" % truck_capacity]
+
+# The truck and village capacity should never drop below zero in any state.
+for j in range(m + 1):
+    for i, capacity in enumerate(capacities):
+        preds += ["(>= s%d_%d 0)" % (i, j)]
+        # The village also has a maximum capacity
+        if i > 0:
+            preds += ["(<= s%d_%d %d)" % (i, j, capacity)]
+
+# For every step, any of the edge transitions can be done.
+for j in range(1, m + 1):
+    altpreds = []
+    jprev = j - 1
+    for (x, y), cost in trans.items():
+        # Preds for this choice
+        cpreds = fillin([
+            "(= l{jprev} {x})",
+            "(= l{j} {y})",
+        ], vars())
+        # Villages other than the next village just lose time
+        # The new village are additionally restocked.
+        for i in range(1, len(states)):
+            newval = "(- s{i}_{jprev} {cost})"
+            if i == y:
+                drop = "(- s0_{jprev} s0_{j})"
+                newval = "(+ %s %s)" % (newval, drop)
+                cpreds += fillin([
+                    "(>= %s 0)" % drop,
+                ], vars())
+            cpreds += fillin([
+                # Can only do the step if there was sufficient time
+                "(>= s{i}_{jprev} {cost})",
+                "(= s{i}_{j} %s)" % newval,
+            ], vars())
+        # If next is truck, restock.
+        if y == 0:
+            cpreds += fillin([
+                "(= s0_{j} {truck_capacity})",
+            ], vars())
+        altpreds += ["(and %s)" % " ".join(cpreds)]
+    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
-- 
cgit v1.2.1