#!/usr/bin/perl -w

$rank = 0;
$tmpfile_otter = "/tmp/o2d.otter.$$";
$tmpfile_dot = "/tmp/o2d.dot.$$";
@initial = ();
$found = 0;

while ($#ARGV >= 0) {
	$arg = shift @ARGV;
	if ($arg eq "-r") { $rank = 1; }
	else { usage(); }
}

system("./otter > $tmpfile_otter");
open FD,$tmpfile_otter;

while (<FD>) {
	$found = 1 if (/PROOF/ and length >= 40);
	last if $found;
}

if (!$found) {
	unlink $tmpfile_otter;
	exit 1;
}

open FF,">".$tmpfile_dot;
print FF "digraph test {\n";

while (<FD>) {

	last if /end of proof/;
	next if /^$/;

	($nr,$origin,$clause) = /(\d+) \[(.*)\] (.*)\./;
	$clause = "{".$clause."}";
	$clause =~ s/ //g;
	$clause =~ s/\|/,/g;

	if ($clause eq '{$F}') {
		print FF "n$nr [label=\"\" shape=\"box\"];\n";
	} else {
		print FF "n$nr [label=\"$clause\"];\n";
	}

	if ($origin =~ /binary/) {
		($a,$b) = ($origin =~ /binary,(\d+)\.\d+,(\d+)\.\d+/);
		print FF "n$a -> n$nr;\n";
		print FF "n$b -> n$nr;\n";
	} else {
		push @initial,"n$nr";
	}
}

close FD;
unlink $tmpfile_otter;

print FF "{rank=same; @initial }\n" if $rank;
print FF "}\n";
close FF;

system("dot -Tps $tmpfile_dot");
unlink $tmpfile_dot;

exit 0;

sub usage {
print<<EOF;
o2d - convert otter proofs into PostScript drawings

usage: o2d [-options] < <otter file>

options:
  -r: put all initial clauses at the top

EOF
exit 1;
}