summaryrefslogtreecommitdiff
path: root/food_delivery/generate-food.py
diff options
context:
space:
mode:
authorPeter Wu <peter@lekensteyn.nl>2017-01-13 23:13:00 +0100
committerPeter Wu <peter@lekensteyn.nl>2017-01-13 23:13:00 +0100
commit040dbd43cc98074d6a20e9fe66bc99485f87ea86 (patch)
tree16b1b4cde5882e46125c602d96daaac698baf512 /food_delivery/generate-food.py
parent2b84767d5b493bde658b443637b8733cfaf57a34 (diff)
download2IMF25-AR-040dbd43cc98074d6a20e9fe66bc99485f87ea86.tar.gz
FoodDelivery: adjust SMT and table output, add text for 1b
Diffstat (limited to 'food_delivery/generate-food.py')
-rwxr-xr-xfood_delivery/generate-food.py11
1 files changed, 5 insertions, 6 deletions
diff --git a/food_delivery/generate-food.py b/food_delivery/generate-food.py
index 192131b..ef9a00d 100755
--- a/food_delivery/generate-food.py
+++ b/food_delivery/generate-food.py
@@ -124,18 +124,17 @@ if is_b:
literals += ["k0", "k1"]
for k in range(1, m + 1):
for j in range(1, m + 1):
- if k >= j:
+ if j >= k:
continue
- jprev = j - 1
highers = " ".join([
- "(>= s{i}_{j} s{i}_{k})".format(i=i, j=j, k=k)
- for i in range(1, len(states))
+ "(<= s{i}_{j} s{i}_{k})".format(i=i, j=j, k=k)
+ for i in range(len(states))
])
stuff += fillin([
- "(and {highers} (= l{j} l{k}) (= k0 {j}) (= k1 {k}))"
+ "(and (= k0 {j}) (= k1 {k}) (= l{j} l{k}) {highers})"
], vars())
- preds += ["(or %s)" % " ".join(stuff)]
+ preds += ["(or %s)" % "\n".join(stuff)]
# Begin generator
s = """(benchmark test.smt