#!/bin/python
import sys
import math

nr_of_classes = 10
nr_of_rooms = math.ceil(nr_of_classes * 0.7)
hours_per_week = 26
time_slots_per_day = 8
days_per_week = 5
nr_of_courses = 10

literals = []
predicates = []

for d in range(days_per_week):
    for h in range(time_slots_per_day):
        for c in range(nr_of_classes):
            literals.append('(day_%i_hour_%i_class_%i_room Int)' % (d, h, c))     # (0, nr_of_rooms]
            predicates.append('(and (<= day_%i_hour_%i_class_%i_room %i) (>= day_%i_hour_%i_class_%i_room 0))' %
                              (d, h, c, nr_of_rooms, d, h, c))
            literals.append('(day_%i_hour_%i_class_%i_lecture Int)' % (d, h, c))  # (0, hours_per_week]
            predicates.append('(and (<= day_%i_hour_%i_class_%i_lecture %i) (>= day_%i_hour_%i_class_%i_lecture 0))' %
                              (d, h, c, hours_per_week, d, h, c))

# Every lecture must be followed in a given week
for co in range(hours_per_week):
    for c in range(nr_of_classes):
        tmp = '(xor\n'
        for d in range(days_per_week):
            for h in range(time_slots_per_day):
                tmp += ' (= day_%i_hour_%i_class_%i_lecture %i)\n' % (d, h, c, co + 1)
        tmp += ')'
        predicates.append(tmp)

# If a lecture is being followed at a specific time, a room needs to be scheduled
for d in range(days_per_week):
    for h in range(time_slots_per_day):
        for c in range(nr_of_classes):
            predicates.append('(ite (> day_%i_hour_%i_class_%i_lecture 0) (> day_%i_hour_%i_class_%i_room 0) (= '
                              'day_%i_hour_%i_class_%i_room 0))' % (d, h, c, d, h, c, d, h, c))

# Rooms may not be scheduled double
for d in range(days_per_week):
    for h in range(time_slots_per_day):
        for c1 in range(nr_of_classes):
            for c2 in range(nr_of_classes):
                if c2 > c1:
                    predicates.append('(not (= day_%i_hour_%i_class_%i_room day_%i_hour_%i_class_%i_room))' %
                                      (d, h, c1, d, h, c2))

s = """(benchmark test.smt
:logic QF_UFLIA
:extrafuns (
"""
s += "\n".join("%s" % x for x in literals)
s += """
)
:formula (and
"""
s += "\n".join(predicates)
s += """
))
"""

try:
    print(s)
    # Hack to avoid printing a ugly error in case stdin of next pipe is closed.
    sys.stdout.flush()
    sys.stdout.close()
except BrokenPipeError:
    pass