From d1416bd2cb9651f3de7c12da3d8133d0287db5c3 Mon Sep 17 00:00:00 2001
From: Peter Wu <peter@lekensteyn.nl>
Date: Fri, 13 Jan 2017 17:46:11 +0100
Subject: Revert "generate-food.py: convert to array"

This reverts commit d49ec13d1a039315fe3d137e003a01e635af855e.

Arrays are unbounded, so avoid its use if possible. It would require
more changes.
---
 food_delivery/generate-food.py | 35 ++++++++++++++++++-----------------
 1 file changed, 18 insertions(+), 17 deletions(-)

diff --git a/food_delivery/generate-food.py b/food_delivery/generate-food.py
index b182cd7..dc87c03 100755
--- a/food_delivery/generate-food.py
+++ b/food_delivery/generate-food.py
@@ -53,29 +53,30 @@ def fillin(cases, template_vars):
         return cases.format(**template_vars)
     return [template.format(**template_vars) for template in cases]
 
-extrafuns = []
+literals = []
 preds = []
 
 # s0_j is the current stock of the truck
 # s1_j is the current stock of village 1
-extrafuns += ["(s Int Int Int)"]
-extrafuns += ["(l Int Int)"]
+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 += ["(= (l 0) 0)"]
-preds += ["(= (s 0 0) %d)" % truck_capacity]
+    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)]
+        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)]
+            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):
@@ -84,34 +85,34 @@ for j in range(1, m + 1):
     for (x, y), cost in trans.items():
         # Preds for this choice
         cpreds = fillin([
-            "(= (l {jprev}) {x})",
-            "(= (l {j}) {y})",
+            "(= l{jprev} {x})",
+            "(= l{j} {y})",
         ], vars())
 
         # All villages must have sufficient time to make the transition.
         for i in range(1, len(states)):
             cpreds += fillin([
-                "(>= (s {i} {jprev}) {cost})",
+                "(>= s{i}_{jprev} {cost})",
             ], vars())
 
         # Calculate new food stock per village.  All village lose the cost, but
         # the next village can be stocked from the truck.
         for i in range(1, len(states)):
-            newval = "(- (s {i} {jprev}) {cost})"
+            newval = "(- s{i}_{jprev} {cost})"
             if i == y:
                 # This is next village, so restock village from truck.
-                drop = "(- (s 0 {jprev}) (s 0 {j}))"
+                drop = "(- s0_{jprev} s0_{j})"
                 newval = "(+ %s %s)" % (newval, drop)
                 cpreds += fillin([
                     "(>= %s 0)" % drop,
                 ], vars())
             cpreds += fillin([
-                "(= (s {i} {j}) %s)" % newval,
+                "(= s{i}_{j} %s)" % newval,
             ], vars())
         # If next is truck, restock.
         if y == 0:
             cpreds += fillin([
-                "(= (s 0 {j}) {truck_capacity})",
+                "(= s0_{j} {truck_capacity})",
             ], vars())
         altpreds += ["(and %s)" % " ".join(cpreds)]
     preds += ["(or %s)" % "\n".join(altpreds)]
@@ -122,7 +123,7 @@ if is_b:
     for j in range(1, m + 1):
         jprev = j - 1
         highers = " ".join([
-            "(>= (s {i} {j}) (s {i} 0))".format(i=i, j=j)
+            "(>= s{i}_{j} s{i}_0)".format(i=i, j=j)
             for i in range(1, len(states))
         ])
         stuff += fillin([
@@ -136,7 +137,7 @@ s = """(benchmark test.smt
 :logic QF_UFLIA
 :extrafuns (
 """
-s += "\n".join(extrafuns)
+s += "\n".join("(%s Int)" % x for x in literals)
 s += """
 )
 :formula (and
-- 
cgit v1.2.1