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