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