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