#!/usr/bin/perl
#
#   intp  -- maps atom numbers into atom names.
#
#
# usage: intp dimacs_file  < model_file
#
# The program reads the atom names from 'dimacs_file' and a model from
# 'model_file', and prints the textual representation of the model.

$atom_file = shift;

if (!$atom_file) {
  print STDERR  "usage: intp dimacs_file < model_file\n";
  exit(1);
}

open (IN, "$atom_file") || die "can't open $atom_file";

while (<IN>) {
  if (/^c ([0-9]+) (.*)$/) {
    $atom[$1] = $2;
  }
}

close IN;


sub complement {
  my $atom = $_[0];
  my $res;
  if ($atom =~ /^-(.*)/) {
    $res = $1;
  } else {
    $res = "-" . $atom;
  }
  $res;
}

$num = 1;
while (<>) {
  if (/^-?[0-9]/) {
    print "Model: "; $num++;
    @lits = split / /;
    foreach $lit (@lits) {
      if ($lit =~ /-([0-9]+)/) {
	if (!$printed{$atom[$1]}) {
	  $compl = complement($atom[$1]);
	  if ($compl =~ /^-/) {
	    # no negatives
	  } else {
	    print "$compl ";
	    $printed{$atom[$1]} = 1;
	    $printed{$compl} = 1;
	  }
	}
      } elsif ($lit =~ /([0-9]+)/) {
	if (!$printed{$atom[$1]}) {
	  if ($atom[$1] =~ /^-/) {
	    # no negatives 
	  } else {
	    print "$atom[$1] ";
	    $printed{$atom[$1]} = 1;
	    $printed{"-".$atom[$1]} = 1;
	  }
	}
      }
    }
  }
}

print "\n";