Buffer management

[tpaviot]

Issue related to buffer management feature development. Tasks can be producers for a buffer or consumer. This is a common problem in manufacturing: a task assembly may need 8 bolts taken from a buffer where 50 bolts are available. After 6 assembly tasks are achieved, there are only 2 bolts left and then the task cannot be executed. Another task (let's say "bolt order") is required to fill the buffer up to at least 8 bolts.

[tpaviot]

Related code: bubble sort (this will be used later)

from z3 import *
import random

N = 10

list_to_sort = []
for i in range(N):
    list_to_sort.append(random.randint(0, 30))
print(list_to_sort)
N = len(list_to_sort)

s = SolverFor("QF_IDL")

a = [Int(f"x_{i}") for i in range(N)]  # build initial array in z3 variables

# add the related constraints
s.add([a[i] == list_to_sort[i] for i in range(N)])

def sort_bubble(IntSort_list, solver):
    """Take a list of int variables, return the list of new variables
    sorting using the bubble recursive sort"""
    sorted_list = IntSort_list.copy()

    def bubble_up(ar):
        arr = ar.copy()
        for i in range(len(arr) - 1):
            x = arr[i]
            y = arr[i + 1]
            # compare and swap x and y
            x1, y1 = FreshInt(), FreshInt()
            c = If(x <= y, And(x1 == x, y1 == y), And(x1 == y, y1 == x))
            # store values
            arr[i] = x1
            arr[i + 1] = y1
            s.add(c)
        return arr

    for _ in range(len(sorted_list)):
        sorted_list = bubble_up(sorted_list)
    return sorted_list

import time

b = sort_bubble(a, s)
init_time = time.time()
s.check()
final_time = time.time()
print(final_time - init_time)

# Get solution
solution = s.model()
# Display solution
print("[", end="")
for v in b:
    print(solution[v], end=",")
print("]")
print(s.statistics())

[tpaviot]

Code available at https://github.com/tpaviot/ProcessScheduler/tree/buffer

[tpaviot]

Branch merged, closing this issue.