#!/usr/bin/env python
# Takes the solution from z3's output and converts it into a picture for LaTeX.

import operator
import re
import sys

# Map component index to (x, y, width, height)
boxes = {}

# Reads input, line-by-line. Ignore the first line that just says "sat".
# Other lines that are accepted:
# x0 -> 2.0
# y0 -> (/ 7.0 5.0)
# w0 -> 3.0
# h0 -> 4.0
# Reads it into: boxes[0] = (x, y, width, height) = (2, 7/5, 3, 4)
for line in sys.stdin:
    line = line.strip()
    if line == 'sat':
        continue
    m = re.match(r'([whxy])(\d+) -> (?:([0-9.]+)|\(/ ([0-9.]+) ([0-9.]+)\))', line)
    what = m.group(1)
    component_index = int(m.group(2))
    num = m.group(3)
    if num is not None:
        num = float(num)
    else:
        num = float(m.group(4)) / float(m.group(5))
    # Convert to something more readable if possible.
    if num.is_integer():
        num = int(num)

    if component_index not in boxes:
        boxes[component_index] = [None] * 4
    boxes_index = 'xywh'.index(what)
    assert boxes_index >= 0
    boxes[component_index][boxes_index] = num

# Predefined colors from https://en.wikibooks.org/wiki/LaTeX/PGF/TikZ#Color
colors = [
'red',
'green',
'blue',
'cyan',
'magenta',
#'yellow',
#'black',
'gray',
'darkgray',
'lightgray',
'brown',
#'lime',
'olive',
'orange',
'pink',
'purple',
'teal',
'violet',
#'white',
]


def is_power_component(i):
    return i < 2

def print_boxes():
    # Print results, sorted by the operator index (for consistency).
    for i, component in sorted(boxes.items(), key=operator.itemgetter(0)):
        x, y, w, h = component
        x2, y2 = x + w, y + h
        attrs = []
        # Add color
        attrs += ["draw=%s" % colors[i]]
        if is_power_component(i):
            attrs += ["fill=%s" % "red"]

        attrs = ','.join(attrs)

        # HACK: print coords for debugging
        if sys.argv[-1] == 'debug':
            print(x, y, w, h)
            continue

        # For easier detection, reduce box dimension (add margin)
        margin = 0.01
        x += margin
        y += margin
        x2 -= margin
        y2 -= margin

        tpl = r"\draw[{attrs}] ({x}, {y}) rectangle ({x2}, {y2});"
        print(tpl.strip().format(**vars()))

        # Reset for printing text
        x, y, w, h = component
        x2, y2 = x + w, y + h

        # Draw number, coordinate and dimensions for debugging
        tx = x + w/2
        ty = y + h/2
        text = r"%s\\(%s,%s)\\(%s x %s)" % (i, x, y, w, h)
        print(r'\node[align=center] at (%f,%f) {%s};' % (tx, ty, text))

# Just the boxes.
print_boxes()