diff options
author | Peter Wu <peter@lekensteyn.nl> | 2017-01-13 12:12:28 +0100 |
---|---|---|
committer | Peter Wu <peter@lekensteyn.nl> | 2017-01-13 12:12:28 +0100 |
commit | 5b413ea5eabda1466cd902fc03e12e2644bc30a2 (patch) | |
tree | 4d2d36aeae4466eeb2acecd9ceecee91a9f01660 /food_delivery/generate-food.py | |
parent | e949ba318a979d30932d2938599761505e1c3b38 (diff) | |
download | 2IMF25-AR-5b413ea5eabda1466cd902fc03e12e2644bc30a2.tar.gz |
food_delivery: initial implementation for b
Diffstat (limited to 'food_delivery/generate-food.py')
-rwxr-xr-x | food_delivery/generate-food.py | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/food_delivery/generate-food.py b/food_delivery/generate-food.py index 0cf954d..dc87c03 100755 --- a/food_delivery/generate-food.py +++ b/food_delivery/generate-food.py @@ -1,9 +1,16 @@ #!/usr/bin/env python3 +# Usage: +# $0 [number-of-steps [truck-capacity [b]]] | z3 -smt -in +# Examples: +# $0 64 240 +# $0 30 260 b + import sys # Number of steps m = 64 if len(sys.argv) <= 1 else int(sys.argv[1]) truck_capacity = 240 if len(sys.argv) <= 2 else int(sys.argv[2]) +is_b = len(sys.argv) >= 4 and sys.argv[3] == 'b' states = "SABCD" @@ -110,6 +117,21 @@ for j in range(1, m + 1): altpreds += ["(and %s)" % " ".join(cpreds)] preds += ["(or %s)" % "\n".join(altpreds)] +if is_b: + # If stock is higher or equal to initial state, then we found a loop. + stuff = [] + for j in range(1, m + 1): + jprev = j - 1 + highers = " ".join([ + "(>= s{i}_{j} s{i}_0)".format(i=i, j=j) + for i in range(1, len(states)) + ]) + stuff += fillin([ + "(and {highers})" + ], vars()) + + preds += ["(or %s)" % " ".join(stuff)] + # Begin generator s = """(benchmark test.smt :logic QF_UFLIA |