From 040dbd43cc98074d6a20e9fe66bc99485f87ea86 Mon Sep 17 00:00:00 2001 From: Peter Wu Date: Fri, 13 Jan 2017 23:13:00 +0100 Subject: FoodDelivery: adjust SMT and table output, add text for 1b --- food_delivery/generate-food.py | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) (limited to 'food_delivery/generate-food.py') 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 -- cgit v1.2.1