summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPeter Wu <peter@lekensteyn.nl>2017-01-13 17:46:11 +0100
committerPeter Wu <peter@lekensteyn.nl>2017-01-13 17:46:11 +0100
commitd1416bd2cb9651f3de7c12da3d8133d0287db5c3 (patch)
tree7566107ec5391ddd6db85fdd06c796ec896df7fd
parentd49ec13d1a039315fe3d137e003a01e635af855e (diff)
download2IMF25-AR-d1416bd2cb9651f3de7c12da3d8133d0287db5c3.tar.gz
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.
-rwxr-xr-xfood_delivery/generate-food.py35
1 files 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