#!/usr/bin/perl -w

use IPC::Open2;

####################################################################
########################## snsynthesis.pl ##########################
################### converts .sn file to Z3 SAT ####################
####################################################################


# Given an input size n and a depth d, this script outputs a Z3 SAT
# formula that is satisfiable if, and only if, there exists a sorting
# network of depth d sorting n inputs. The network is encoded into
# the variables Pij, where Pij = Vk means that at depth i the j-th
# wire is connected to the k-th wire at the same depth. If
# Pij = j then this wire has no connection at that depth.

sub usage {
	print "\nusage: snsynthesis.pl <n> <d>\n",
	"  <n>        : number of inputs\n",
	"  <d>        : depth of the network\n\n";
	exit 2;
}

usage() if $#ARGV != 1;

open2 *Reader,*Writer,"z3 -smt2 -in";

$n = shift @ARGV;
$d = shift @ARGV;

for ($i = 0; $i < $n; $i++) {
    push @dataTypes, "V$i";
}

print Writer "(declare-datatypes () ((MatrixEntry ".join(" ", @dataTypes).")))\n";

for ($j = 0; $j < $d; $j++) {
    for ($i = 0; $i < $n; $i++) {
	print Writer "(declare-const ",P($j,$i)," MatrixEntry)\n";
    }
}

# permutation matrix

for ($j = 0; $j < $d; $j++) {
    for ($i = 0; $i < $n; $i++) {
	for ($k = 0; $k < $n; $k++) {
	    print Writer "(assert (=> (= ",P($j,$i)," V".$k.") (= ",P($j,$k)," V".$i.")))\n";
	}
    }
}


print Writer "(assert (forall (";

for ($i = 0; $i < $n; $i++) {
    print Writer "(I".$i." Bool) ";
}

print Writer ")\n (exists (";

for ($i = 0; $i < $n; $i++) {
    print Writer "(O".$i." Bool) ";
}

for ($j = 0; $j < $d; $j++) {
    for ($i = 0; $i < $n; $i++) {
	print Writer "(",C($j,$i)," Bool) ";
    }
}

print Writer ")\n (and ";

for ($i = 0; $i < $n; $i++) {
    for ($k = 0; $k <= $i; $k++) {
	print Writer "(=> (= ",P(0,$i)," V".$k.") (= ",C(0,$i)," (or I".$i." I".$k.")))\n";
    }
    for ($k = $i+1; $k < $n; $k++) {
	print Writer "(=> (= ",P(0,$i)." V".$k.") (= ",C(0,$i)," (and I".$i." I".$k.")))\n";
    }
}

for ($j = 1; $j < $d; $j++) {
    for ($i = 0; $i < $n; $i++) {
	for ($k = 0; $k <= $i; $k++) {
	    print Writer "(=> (= ",P($j,$i)," V".$k.") (= ",C($j,$i)," (or ",C($j-1,$i)," ",C($j-1,$k),")))\n";
	}
	for ($k = $i+1; $k < $n; $k++) {
	    print Writer "(=> (= ",P($j,$i)," V".$k.") (= ",C($j,$i)," (and ",C($j-1,$i)," ",C($j-1,$k),")))\n";
	}
    }
}

for ($i = 0; $i < $n; $i++) {
    print Writer "(= O".$i." ",C($d-1,$i),")\n";
}

for ($i = 0; $i < $n-1; $i++) {
    print Writer "(=> O".$i." O".($i+1).")\n";
}

print Writer "))))\n";
print Writer "(check-sat)\n(get-model)\n";

close Writer;

$k = -1;
while (<Reader>) {
	tr/\015\012//d;
	if (/^unsat$/) {
		print "There is NO CORRECT sorting network for n=$n",
			" and d=$d.\n";
		exit 1;
	}
	($k,$i) = ($1,$2) if /define-fun P_(\d*)_(\d*)/;
	if ($k >= 0 && /V(\d*)/) {
		($i,$j) = ($i+1,$1+1);
		push @cmps,"$k-$i $j" if $i < $j;
		$k = -1;
	}
}

print "There exists a correct sorting network for n=$n and d=$d,\n",
	"and it looks like this:\n";
for (sort @cmps) {
	s/^.*-//;
	print $_,"\n";
}

exit 0;

sub P {
	my ($i,$j) = @_;
	return "P_${i}_${j}";
}

sub C {
	my ($i,$j) = @_;
	return "C_${i}_${j}";
}