#!/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 = {}

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)

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

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

def print_grid():
    # XXX currently hard-coding grid size
    print(r'\draw[step=1,gray,very thin] (0, 0) grid (30, 30);')

if not True:
    # Complete picture
    print(r'\begin{tikzpicture}')
    print_grid()
    print_boxes()
    print(r'\end{tikzpicture}')
else:
    # Just the boxes.
    print_boxes()