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

# from https://bertdobbelaere.github.io/sorting_networks.html
data=[
[(0,2),(1,3)],
[(0,1),(2,3)],
[(1,2)]]

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)
    print ("")

# 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