#!/usr/bin/perl -w

use IPC::Open2;

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


# The function Comparator should return the formula phi_C for a given
# comparator C.
# * The indices of the wires are given by $top and $bottom,
#   where $top < $bottom.
# * In the formula, the variables corresponding to the input wires
#    are expressed as Current($top) and Current($bottom).
# * The variables for the output wires are Next($top) and Next($bottom).
#
# Express phi_C as a Boolean combination over these variables, connected
# with the primitives And(), Or(), Eq(), Implies(), Neg().
#
# (false) example: return And(Eq(Next($top), Current($top)),
#                             Eq(Next($bottom), Current($bottom)));
#
# This example enforces that the next value of $top is equal to
# $top and the next value of $bottom is equal to the current value
# of $bottom.

sub Comparator {
    my ($top,$bottom) = @_;

    return False ; # your formula here!
}


# This function should return a formula specifying that the final values
# be sorted. Hint: It can be done as a conjunction of clauses relating
# the final values of neighbouring wires.

sub Correct {
    @clauses = ();	# empty set
    for ($i = 1; $i < $n; $i++) {
	# add one clause relating Current($i) and Current($i+1)
	push @clauses, False ;	# your formula here
    }
    return And(@clauses);	# conjunction of all clauses
}

####################################################################
######################## do not change below #######################
####################################################################

$debug = 0;
if ($#ARGV >= 0 && $ARGV[0] eq "-d") {
	$debug = 1;
	shift @ARGV;
}

usage() if $#ARGV != 1;
$fn = shift @ARGV;
die "cannot read file $fn" unless -r $fn;
$n = shift @ARGV;
for ($i = 1; $i <= $n; $i++) { $dp[$i] = 0; }

%variableNames=();

open FD,$fn;
while (<FD>) {
	tr/\015\012//d;
	die "invalid instruction $_ in $fn" unless /^(\d+) (\d+)$/;
	($a,$b) = ($1,$2);
	die "number too large w.r.t. input" if $a > $n || $b > $n;
	die "smaller index must be first in $_" if $a >= $b;

	push @f, Comparator($a,$b);

	$dp[$a]++; $dp[$b]++;
}
close FD;

@sorter = And(@f);
@correct = Neg(Correct());

$cmd = "z3 -smt2 -in";
$cmd = "cat" if $debug;
open2(*Reader,*Writer,$cmd);

foreach my $key (keys(%variableNames)) {
    print Writer "(declare-const ", $key, " Bool)\n";
}

print Writer "(assert ",@sorter,")\n";
print Writer "(assert ",@correct,")\n";
print Writer "(check-sat)\n(get-model)\n";

close Writer;

$i = 0;
while (<Reader>) {
	if ($debug) { print $_ ; next; }
	tr/\015\012//d;
	if (/^unsat$/) {
		print "The network is correct for all inputs.\n";
		exit 1;
	}
	$i = $1 if /define-fun x_(\d*)_0/;
	if (/true/) { $y[$i] = 1; $i = 0; }
	if (/false/) { $y[$i] = 0; $i = 0; }
}

exit 0 if $debug;

shift @y;
print "The network is INCORRECT for the input ",join("",@y),".\n";

exit 0;

sub usage {
	print "\nusage: sn2sat.pl [-d] <filename> <n>\n",
		" -d          : debug, just print the generated formula\n",
		"  <filename> : contains sorting network\n",
		"  <n>        : number of inputs\n\n";
	exit 2;
}

sub Var {
	my ($i,$d) = @_;
	$variableNames{"x_${i}_${d}"} = 1;
	return "x_${i}_${d}";
}

sub Or {
	return "(or ".join(" ",@_).")";
}

sub And {
	return "(and ".join(" ",@_).")";
}

sub Implies {
    my ($left, $right) = @_;
    return "(=>", $left,$right,")";
}

sub Eq {
	my ($left,$right) = @_;
	return "(= $left $right)"
}

sub Neg {
	return "(not ".shift.")";
}

sub True {
	return "true";
}

sub False {
	return "false";
}

sub Current {
	my $a = shift;
	return Var($a,$dp[$a]);
}

sub Next {
	my $a = shift;
	return Var($a,$dp[$a]+1);
}