zchaff64/run_till_fix.pl

   1 #!/usr/bin/perl -w
   2
   3 use strict;
   4
   5 die "Usage:\nrun_till_fix CNF_Filename [Num_Max_Iterations]" if (@ARGV < 1);
   6
   7 my $file = $ARGV[0];
   8 my $max_iteration = @ARGV > 1 ? $ARGV[1] : 1000;
   9 my $last_cls_count = 0;
  10 my $filename = $file."_itr_0";
  11 $filename =~ s/.*\///;
  12
  13 system("cp $file $filename");
  14
  15 $file =~ s/.*\///;
  16
  17 for (my $i = 0; $i < $max_iteration; ++$i) {
  18
  19   open INPUT, "<$filename" or die "$!\n";
  20
  21   my @tokens;
  22
  23   while (<INPUT>) {
  24     @tokens = split / /;
  25     last if ($tokens[0] eq "p");
  26   }
  27
  28   last if $tokens[3] == $last_cls_count;
  29
  30   $last_cls_count = $tokens[3];
  31
  32   system("zchaff $filename");
  33   system("zverify_df $filename resolve_trace -core");
  34   my $j = $i + 1;
  35   $filename = $file."_itr_".$j;
  36   system("mv unsat_core.cnf $filename");
  37 }