#!/usr/bin/env python
# Usage for 3a (first argument is the deadline):
#   $0 -1 | z3 -smt -in
# Usage for 3b:
#   $0 90 b | z3 -smt -in

import sys

# Deadline
deadline = int(sys.argv[1])
is_b = len(sys.argv) >= 3 and sys.argv[2] == 'b'


# Number of jobs
n = 12

# For i: (j, ...), job i must not start before jobs j have ended.
job_dependencies_ended = {
    3:  (1, 2),
    5:  (3, 4),
    7:  (3, 4, 6),
    9:  (5, 8),
    11: (10,),
    12: (9, 11),
}

job_dependencies_started = {
    8: (5,),
}

job_durations = {
    i: i + 5 for i in range(1, n + 1)
}


def fillin(cases, template_vars):
    if type(cases) == str:
        return cases.format(**template_vars)
    return [template.format(**template_vars) for template in cases]

literals = []
preds = []

# Start time of all jobs
# and their duration
for i in range(1, n + 1):
    literals += fillin([
        "t{i}",
        "d{i}",
    ], vars())
    # times must be positive and
    # all jobs must finish before the deadline.
    preds += fillin([
        "(>= t{i} 0)",
        "(<= (+ t{i} d{i}) {deadline})",
    ], vars())

# Define duration
for i, duration in job_durations.items():
    preds += fillin([
        "(= d{i} {duration})"
    ], vars())

# Job i may not start before job(s) j have *ended*. Or:
# for all j: t_j + d_j <= t_i
for i, deps in job_dependencies_ended.items():
    for j in deps:
        preds += fillin([
            "(<= (+ t{j} d{j}) t{i})"
        ], vars())

# Job i may not start before job(s) j have *started*. Or:
# for all j: t_j <= t_i
for i, deps in job_dependencies_started.items():
    for j in deps:
        preds += fillin([
            "(<= t{j} t{i})"
        ], vars())

# Jobs 5, 7 en 10 require a special equipment of which only one copy is
# available, so no two of these jobs may run at the same time.
# Or:
# There must exist a pair of jobs (i, j) s.t. one starts after another ended:
# t_i + d_i <= t_j
jobs_max2_for_3 = (5, 7, 10)
altpreds = []
for i in jobs_max2_for_3:
    for j in jobs_max2_for_3:
        if i == j:
            continue
        altpreds += fillin([
            "(<= (+ t{i} d{i}) t{j})"
        ], vars())

preds += ["(or %s)" % " ".join(altpreds)]

# Job 6 may only run when job 12 is running.
if is_b:
    preds += [
        "(and (<= t12 t6) (<= (+ t6 d6) (+ t12 d12)))"
    ]

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

try:
    import sys
    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