#!/usr/bin/env python
# Run with: $0 | z3 -smt -in

# Power components
powers = [
    (4, 3),
    (4, 3),
]

# Regular components
regulars = [
    (4, 5),
    (4, 6),
    (5, 20),
    (6, 9),
    (6, 10),
    (6, 11),
    (7, 8),
    (7, 12),
    (10, 10),
    (10, 20),
]

# Chip dimensions
chip_w, chip_h = (30, 30)

# Minimum distance between centers
power_distance = 17


all_components = powers + regulars

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 = []
# Add X and Y coordinate for each component,
# and also the width/height
for i, (w, h) in enumerate(all_components):
    var_x = 'x%d' % i
    var_y = 'y%d' % i
    var_w = 'w%d' % i
    var_h = 'h%d' % i
    literals += [
        var_x,
        var_y,
        var_w,
        var_h,
    ]
    # Ensure each component stays in chip area
    newpreds = [
        '(>= {var_x} 0)',
        '(>= {var_y} 0)',
        '(<= {var_x} {chip_w})',
        '(<= {var_y} {chip_h})',
    ]
    # Dimensions are restricted:
    # either width and height are w, h; or they are rotated.
    newpreds += [
        '(or'
        ' (and (= {var_w} {w}) (= {var_h} {h}))'
        ' (and (= {var_w} {h}) (= {var_h} {w}))'
        ')',
    ]
    # Fill in template with vars
    preds += fillin(newpreds, vars())

# Avoid overlap between any pair, so any other component must be outside the
# current pivot.
for i in range(len(all_components)):
    for j in range(len(all_components)):
        if i == j:
            continue
        # other (j) must be below, on the left of pivot (i).
        # or above or on the right (mind the width/height!).
        altpreds = [
            '(<= y{j} y{i})',
            '(<= x{j} x{i})',
            '(>= y{j} (+ y{i} h{i}))',
            '(>= x{j} (+ x{i} x{i}))',
        ]
        preds += ['(or %s)' % ' '.join(fillin(altpreds, vars()))]

# require minimum distance between power components
for i in range(len(powers)):
    for j in range(len(powers)):
        if i == j:
            continue
        # need center_i >= center_j + distance (for center from {X,Y}, repeat
        # for i and j swapped in case j occurs after i)
        # center = x + w / 2
        center_x_i = fillin('(+ x{i} (/ w{i} 2))', vars())
        center_y_i = fillin('(+ y{i} (/ h{i} 2))', vars())
        center_x_j = fillin('(+ x{j} (/ w{j} 2))', vars())
        center_y_j = fillin('(+ y{j} (/ h{j} 2))', vars())
        altpreds = [
            '(>= {center_x_i} (+ {center_x_j} {power_distance}))',
            '(>= {center_x_j} (+ {center_x_i} {power_distance}))',
            '(>= {center_y_i} (+ {center_y_j} {power_distance}))',
            '(>= {center_y_j} (+ {center_y_i} {power_distance}))',
        ]
        preds += ['(or %s)' % ' '.join(fillin(altpreds, vars()))]

# Begin generator
s = """(benchmark test.smt
:logic QF_UFLRA
:extrafuns
(
"""
s += "\n".join("(%s Real)" % 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