#!/usr/bin/perl

use strict;

my %o=(); # original formula names
my %ro=(); # flas to original names
my %p=(); # parent to children
my %c=(); # child to parent
my %f=(); # name to fla
my %rf=(); # fla to all names
my $proofs=$ARGV[0];
my $toprove=$ARGV[1];
open(G,$proofs) or die;
while(<G>)
{
    chomp;
    my $fname0 = $_;
    open(F,$fname0) or die;
    while(<F>)
    {

	
	    if(m/^ *cnf\( *(i[^, ]+) *, *([^, ]+) *,(.*)\)\./)
    {
      my ($nm0,$status,$fla) = ($1,$2,$3);
      my $nm = "$fname0" . "___" . "$nm0";
            $o{"$nm"}=();
            $ro{$fla}{"$nm"}=();
            $f{"$nm"}=$fla;

    }
    elsif(m/^ *cnf\( *([^, ]+) *, *([^, ]+) *,(.*), *(inference|file)\((.*)/)
	{
	    my ($nm0,$status,$fla,$origin,$stuff) = ($1,$2,$3,$4,$5);
	    my $nm = "$fname0" . "___" . "$nm0";
	    $f{$nm}=$fla;
	    $rf{$fla}{$nm}= ();
	    if($origin eq 'file')
	    {
		$stuff =~ m/([^, ]+) *, *([^) ]+)/ or die;
		my ($file,$orignm) = ($1,$2);
		my $fff1 = "$file"  . "___" . "$orignm";
		$o{$fff1}=();
		$ro{$fla}{$fff1}=();
		$f{$fff1}=$fla;
		$p{$fff1}{$nm} = ();
		$c{$nm}= $fff1;
	    }
	    elsif($origin eq 'inference')
	    {
		$stuff =~ m/.*,\[.*\],\[(.*)\]/ or die;
		my ($refs) = ($1);
		my @refs = split(/,/,$refs);
		if($#refs == 0)
		{
		    for my $rr0 (@refs)
		    {
			my $rr = "$fname0" . "___" . "$rr0";
			$p{$rr}{$nm} = ();
			$c{$nm} = $rr;
		    }
		}
	    }
	}
    }
    close(F);
}
close G;


my %gcache=();
sub child
{
    my ($oo) = (@_);
    for my $k (keys %{$p{$oo}})
    {
#	print "$k : ";
	if($f{$k} ne $f{$oo}) { if(exists($gcache{$f{$k}})) {print F1 "% $k cached\n"} else {$gcache{$f{$k}}=$k; print F1 "cnf($k,plain,",$f{$k},").\n"; }} else {print F1 "% $k SAME\n";}
	child($k) ;
	#       print " ) ";
    }
}


open(G,$toprove) or die;
while(<G>)
{
    chomp;
    my $fname0 = $_;
    open(F,$fname0) or die;
    %gcache = ();
    open(F1,">$fname0.enh1") or die;
    while(<F>)
    {
	print F1 $_;
	if(m/^ *cnf\( *([^, ]+) *, *([^, ]+) *,(.*)\)\./)
	{
	    my ($nm0,$status,$fla) = ($1,$2,$3);
	    my $nm = "$fname0" . "___" ."$nm0";

	    print F1 "% ", $nm,":::",$fla,":\n";
	    for my $oo (keys %{$ro{$fla}})
	    {
		print F1 "% EQUIV1:::",$oo,"\n"; #,":::",$f{$oo},":\n";
		child($oo);
		#    for my $k (keys %{$p{$oo}})
		#    {
		#       child($k);
		#    }
	    }
	    print F1 "\n";

	}
    }
    close(F);
    close(F1);
}
close G;