From 5b413ea5eabda1466cd902fc03e12e2644bc30a2 Mon Sep 17 00:00:00 2001 From: Peter Wu Date: Fri, 13 Jan 2017 12:12:28 +0100 Subject: food_delivery: initial implementation for b --- food_delivery/food-to-table.py | 3 +++ food_delivery/generate-food.py | 22 ++++++++++++++++++++++ 2 files changed, 25 insertions(+) diff --git a/food_delivery/food-to-table.py b/food_delivery/food-to-table.py index c054f0c..b94ad0c 100755 --- a/food_delivery/food-to-table.py +++ b/food_delivery/food-to-table.py @@ -45,5 +45,8 @@ for step, cells in enumerate(matrix): else: line += " & %5d" % value line += r" & %s \\" % "SABCD"[nextNodes[step]] + if step > 0: + if all(x >= y for x, y in zip(matrix[step][1:], matrix[0][1:])): + line += " % HIGHER" #line += r" \\" print(line) 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 -- cgit v1.2.1