Buffer management
Closed this issue · 3 comments
tpaviot commented
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 commented
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 commented
Code available at https://github.com/tpaviot/ProcessScheduler/tree/buffer
tpaviot commented
Branch merged, closing this issue.