#!/usr/bin/env python3
from z3 import *

# from https://bertdobbelaere.github.io/sorting_networks.html
# "Sorting network for 32 inputs, 185 CEs, 14 layers"
# 20m on Intel(R) Core(TM) i7-2760QM CPU @ 2.40GHz
data=[
[(0,1),(2,3),(4,5),(6,7),(8,9),(10,11),(12,13),(14,15),(16,17),(18,19),(20,21),(22,23),(24,25),(26,27),(28,29),(30,31)],
[(0,2),(1,3),(4,6),(5,7),(8,10),(9,11),(12,14),(13,15),(16,18),(17,19),(20,22),(21,23),(24,26),(25,27),(28,30),(29,31)],
[(0,4),(1,5),(2,6),(3,7),(8,12),(9,13),(10,14),(11,15),(16,20),(17,21),(18,22),(19,23),(24,28),(25,29),(26,30),(27,31)],
[(0,8),(1,9),(2,10),(3,11),(4,12),(5,13),(6,14),(7,15),(16,24),(17,25),(18,26),(19,27),(20,28),(21,29),(22,30),(23,31)],
[(0,16),(1,8),(2,4),(3,12),(5,10),(6,9),(7,14),(11,13),(15,31),(17,24),(18,20),(19,28),(21,26),(22,25),(23,30),(27,29)],
[(1,2),(3,5),(4,8),(6,22),(7,11),(9,25),(10,12),(13,14),(17,18),(19,21),(20,24),(23,27),(26,28),(29,30)],
[(1,17),(2,18),(3,19),(4,20),(5,10),(7,23),(8,24),(11,27),(12,28),(13,29),(14,30),(21,26)],
[(3,17),(4,16),(5,21),(6,18),(7,9),(8,20),(10,26),(11,23),(13,25),(14,28),(15,27),(22,24)],
[(1,4),(3,8),(5,16),(7,17),(9,21),(10,22),(11,19),(12,20),(14,24),(15,26),(23,28),(27,30)],
[(2,5),(7,8),(9,18),(11,17),(12,16),(13,22),(14,20),(15,19),(23,24),(26,29)],
[(2,4),(6,12),(9,16),(10,11),(13,17),(14,18),(15,22),(19,25),(20,21),(27,29)],
[(5,6),(8,12),(9,10),(11,13),(14,16),(15,17),(18,20),(19,23),(21,22),(25,26)],
[(3,5),(6,7),(8,9),(10,12),(11,14),(13,16),(15,18),(17,20),(19,21),(22,23),(24,25),(26,28)],
[(3,4),(5,6),(7,8),(9,10),(11,12),(13,14),(15,16),(17,18),(19,20),(21,22),(23,24),(25,26),(27,28)]]

order=max(map(max, map(max, data)))+1

s=Solver()

inputs=[Int('input_%d' % i) for i in range(order)]

def Z3_min (a, b):
    return If(a<b, a, b)

def Z3_max (a, b):
    return If(a>b, a, b)

def comparator (a, b):
    return (Z3_min(a, b), Z3_max(a, b))

tmp=inputs
for layer in data:
    for pair in layer:
        x=["|"]*order
        tmp2=tmp
        first, second = pair
        one, two=comparator(tmp[first], tmp[second])
        tmp2[first], tmp2[second]=one, two
        tmp=tmp2
        x[first]=x[second]="+"
        print ("".join(x))

#for t in tmp:
#    print (t)

# construct expression like
# And(..., k[2]>=k[1], k[1]>=k[0])
expr=[(tmp[k+1]>=tmp[k]) for k in range(order-1)]

# True if everything works correctly:
correct=And(*expr)

# we want to find inputs for which correct==False:
s.add(Not(correct))

print (s.check()) # must be unsat