diff options
author | Peter Wu <peter@lekensteyn.nl> | 2017-01-13 23:13:00 +0100 |
---|---|---|
committer | Peter Wu <peter@lekensteyn.nl> | 2017-01-13 23:13:00 +0100 |
commit | 040dbd43cc98074d6a20e9fe66bc99485f87ea86 (patch) | |
tree | 16b1b4cde5882e46125c602d96daaac698baf512 /food_delivery/generate-food.py | |
parent | 2b84767d5b493bde658b443637b8733cfaf57a34 (diff) | |
download | 2IMF25-AR-040dbd43cc98074d6a20e9fe66bc99485f87ea86.tar.gz |
FoodDelivery: adjust SMT and table output, add text for 1b
Diffstat (limited to 'food_delivery/generate-food.py')
-rwxr-xr-x | food_delivery/generate-food.py | 11 |
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 |