lib/scripts/dimacs2hol.pl
author wenzelm
Thu May 20 20:20:52 2010 +0200 (2010-05-20)
changeset 37012 106c56e916f8
parent 29145 b1c6f4563df7
permissions -rw-r--r--
enable shell script editor mode;
     1 #
     2 # dimacs2hol.pl - convert files in DIMACS CNF format [1] into Isabelle/HOL
     3 #                 theories
     4 #
     5 # Author: Tjark Weber
     6 # Copyright 2004
     7 #
     8 # For each CNF file, a theory file (with '.thy' appended to the original
     9 # filename) is generated.  The CNF files are not modified.
    10 #
    11 # This script is not too strict about the format of the input file.  However,
    12 # in rare cases it may produce a theory that will not be accepted by
    13 # Isabelle/HOL (e.g. when a CNF file contains '\end{verbatim}' or '*}' in a
    14 # comment).
    15 #
    16 # Each CNF file must contain at least one clause, and may not contain empty
    17 # clauses (i.e. '0' immediately followed by another '0').
    18 #
    19 # The CNF formula is negated, so that an unsatisfiable formula becomes
    20 # provable.
    21 #
    22 # [1] ftp://dimacs.rutgers.edu/pub/challenge/satisfiability/doc/satformat.dvi
    23 #
    24 
    25 
    26 sub dimacs2hol {
    27     my ($file) = @_;
    28 
    29     print STDERR "Converting $file ...";
    30 
    31     open (FILE, $file) || die $!;
    32     undef $/; $_ = <FILE>; $/ = "\n";  # slurp whole file
    33     close FILE || die $!;
    34 
    35     s/(^c.*\n\s*)*^p[ \t]+cnf[ \t]+\d+[ \t]+\d+[ \t]*\n//m || die "CNF header not found";  # find and remove header
    36     my ($header) = $&;
    37 
    38     s/^c.*\n//gm;                            # remove further comments
    39     s/\A\s*//;                               # remove leading whitespace
    40     s/(\s+0)?\s*\z//;                        # remove trailing whitespace, and possibly a last '0'
    41     s/-/~/g;                                 # replace '-' by '~' (negation in HOL)
    42     s/[1-9]\d*/v$&/g;                        # add 'v' before variables
    43     s/\s+0\s+/\"\nand \"/g;                  # replace ' 0 ' by '"\nand "'
    44     s/(\d)(\s+[~v])/$1 |$2/g;                # insert ' |' between literals
    45 
    46     my ($filename) = $file;
    47     $filename =~ s/.*\///g;                  # filter out directories, only leave what's after the last '/'
    48 
    49     open (FILE, "> $file.thy") || die $!;
    50 
    51     print FILE "(* Theory generated from \"$filename\" by dimacs2hol *)\n";
    52     print FILE "\n";
    53     print FILE "theory \"$filename\"\n";
    54     print FILE "imports Main\n";
    55     print FILE "begin\n";
    56     print FILE "\n";
    57     print FILE "text {*\n";
    58     print FILE "\\begin{verbatim}\n";
    59     print FILE $header;
    60     print FILE "\\end{verbatim}\n";
    61     print FILE "*}\n";
    62     print FILE "\n";
    63     print FILE "theorem assumes \""; print FILE;
    64     print FILE "\"\n";
    65     print FILE "shows \"False\"\n";  # negate the whole CNF formula
    66     print FILE "using prems\n";
    67     print FILE "oops\n";
    68     print FILE "\n";
    69     print FILE "end\n";
    70 
    71     close FILE || die $!;
    72 
    73     print STDERR " done.\n";
    74 }
    75 
    76 
    77 ## main
    78 
    79 foreach $file (@ARGV) {
    80   eval { &dimacs2hol($file); };
    81   if ($@) { print STDERR "\n*** dimacs2hol $file: ", $@, "\n"; unlink "$file.thy"; }
    82 }