food_delivery: initial implementation for b

2 files changed, 25 insertions, 0 deletions

diff --git a/food_delivery/food-to-table.py b/food_delivery/food-to-table.py
index c054f0c..b94ad0c 100755
--- a/food_delivery/food-to-table.py
+++ b/food_delivery/food-to-table.py
@@ -45,5 +45,8 @@ for step, cells in enumerate(matrix):
         else:
             line += " & %5d" % value
     line += r" & %s \\" % "SABCD"[nextNodes[step]]
+    if step > 0:
+        if all(x >= y for x, y in zip(matrix[step][1:], matrix[0][1:])):
+            line += " % HIGHER"
     #line += r" \\"
     print(line)
diff --git a/food_delivery/generate-food.py b/food_delivery/generate-food.py
index 0cf954d..dc87c03 100755
--- a/food_delivery/generate-food.py
+++ b/food_delivery/generate-food.py
@@ -1,9 +1,16 @@
 #!/usr/bin/env python3
+# Usage:
+#   $0 [number-of-steps [truck-capacity [b]]] | z3 -smt -in
+# Examples:
+#   $0 64 240
+#   $0 30 260 b
+
 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])
+is_b = len(sys.argv) >= 4 and sys.argv[3] == 'b'
 
 states = "SABCD"
 
@@ -110,6 +117,21 @@ for j in range(1, m + 1):
         altpreds += ["(and %s)" % " ".join(cpreds)]
     preds += ["(or %s)" % "\n".join(altpreds)]
 
+if is_b:
+    # If stock is higher or equal to initial state, then we found a loop.
+    stuff = []
+    for j in range(1, m + 1):
+        jprev = j - 1
+        highers = " ".join([
+            "(>= s{i}_{j} s{i}_0)".format(i=i, j=j)
+            for i in range(1, len(states))
+        ])
+        stuff += fillin([
+            "(and {highers})"
+        ], vars())
+
+    preds += ["(or %s)" % " ".join(stuff)]
+
 # Begin generator
 s = """(benchmark test.smt
 :logic QF_UFLIA