constraint solving cooking schedule

pizza_schedule.py

#!/usr/bin/python

import z3
import itertools

class Schedule(object):
    def __init__(self):
        self.s = z3.Solver()
        self.tasks = {}

    def set_start(self, name, start):
        assert name in self.tasks
        self.s.add(self.tasks[name][0] == start)

    def set_end(self, name, end):
        assert name in self.tasks
        self.s.add(self.tasks[name][1] == end)

    def add_task(self, name, duration=None):
        assert name not in self.tasks
        a = z3.Int('%s_start' % name)
        b = z3.Int('%s_end' % name)
        self.tasks[name] = (a, b)

        self.s.add(a >= 0)
        self.s.add(a < b)
        if duration is not None:
            self.s.add(b - a == duration)

    def sequential(self, *tasks):
        assert len(tasks) > 1
        for task in tasks:
            assert task in self.tasks

        ors = []
        for _tasks in itertools.permutations(tasks):
            values = []
            for i, task in enumerate(_tasks):
                if i == len(_tasks) - 1:
                    continue

                next_task = _tasks[i + 1]
                values.append(self.tasks[task][1] < self.tasks[next_task][0])
            ors.append(z3.And(values))

        x = z3.Or(ors)
        self.s.add(x)

    def during(self, a, b):
        assert a in self.tasks
        assert b in self.tasks

        self.s.add(self.tasks[b][0] > self.tasks[a][0])
        self.s.add(self.tasks[b][1] < self.tasks[a][1])

    def order(self, a, b):
        assert a in self.tasks
        assert b in self.tasks
        self.s.add(self.tasks[a][1] < self.tasks[b][0])

    def model(self):
        return self.s.model()

    def check(self):
        return self.s.check()

a = Schedule()
a.add_task('schedule')
a.add_task('make_dough', 3)
a.add_task('slice_onions', 1)
a.add_task('slice_tomatoes', 1)
a.add_task('slice_sausage', 1)
a.add_task('bake', 35)
a.add_task('serve_pizza', 2)
a.add_task('pour_wine', 2)

a.sequential('slice_onions', 'slice_tomatoes', 'slice_sausage')

a.order('slice_sausage', 'bake')
a.order('slice_onions', 'bake')
a.order('slice_tomatoes', 'bake')
a.order('make_dough', 'bake')
a.order('bake', 'pour_wine')
a.order('bake', 'serve_pizza')

[a.during('schedule', i) for i in a.tasks if i != 'schedule']
a.set_start('schedule', 0)
print a.check()
print a.model()
model = a.model()
print "schedule : %d - %d" % (model[a.tasks['schedule'][0]].as_long(), model[a.tasks['schedule'][1]].as_long())