author | wenzelm |
Thu, 27 Mar 2008 14:41:17 +0100 | |
changeset 26429 | 1afbc0139b1b |
parent 20420 | 56ef2dfc41d6 |
child 29145 | b1c6f4563df7 |
permissions | -rw-r--r-- |
15153 | 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 |
|
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 | 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"; |
|
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 | 69 |
print FILE "oops\n"; |
70 |
print FILE "\n"; |
|
71 |
print FILE "end\n"; |
|
72 |
||
73 |
close FILE || die $!; |
|
74 |
||
75 |
print STDERR " done.\n"; |
|
76 |
} |
|
77 |
||
78 |
||
79 |
## main |
|
80 |
||
81 |
foreach $file (@ARGV) { |
|
82 |
eval { &dimacs2hol($file); }; |
|
83 |
if ($@) { print STDERR "\n*** dimacs2hol $file: ", $@, "\n"; unlink "$file.thy"; } |
|
84 |
} |