accept x86_64 results gracefully -- NB: Mac OS does report that if booted in 64 bit mode;
## dimacs2hol.pl - convert files in DIMACS CNF format [1] into Isabelle/HOL# theories## Author: Tjark Weber# Copyright 2004## For each CNF file, a theory file (with '.thy' appended to the original# filename) is generated. The CNF files are not modified.## This script is not too strict about the format of the input file. However,# in rare cases it may produce a theory that will not be accepted by# Isabelle/HOL (e.g. when a CNF file contains '\end{verbatim}' or '*}' in a# comment).## Each CNF file must contain at least one clause, and may not contain empty# clauses (i.e. '0' immediately followed by another '0').## The CNF formula is negated, so that an unsatisfiable formula becomes# provable.## [1] ftp://dimacs.rutgers.edu/pub/challenge/satisfiability/doc/satformat.dvi#sub dimacs2hol { my ($file) = @_; print STDERR "Converting $file ..."; open (FILE, $file) || die $!; undef $/; $_ = <FILE>; $/ = "\n"; # slurp whole file close FILE || die $!; s/(^c.*\n\s*)*^p[ \t]+cnf[ \t]+\d+[ \t]+\d+[ \t]*\n//m || die "CNF header not found"; # find and remove header my ($header) = $&; s/^c.*\n//gm; # remove further comments s/\A\s*//; # remove leading whitespace s/(\s+0)?\s*\z//; # remove trailing whitespace, and possibly a last '0' s/-/~/g; # replace '-' by '~' (negation in HOL) s/[1-9]\d*/v$&/g; # add 'v' before variables s/\s+0\s+/\"\nand \"/g; # replace ' 0 ' by '"\nand "' s/(\d)(\s+[~v])/$1 |$2/g; # insert ' |' between literals my ($filename) = $file; $filename =~ s/.*\///g; # filter out directories, only leave what's after the last '/' open (FILE, "> $file.thy") || die $!; print FILE "(* Theory generated from \"$filename\" by dimacs2hol *)\n"; print FILE "\n"; print FILE "theory \"$filename\"\n"; print FILE "imports Main\n"; print FILE "begin\n"; print FILE "\n"; print FILE "text {*\n"; print FILE "\\begin{verbatim}\n"; print FILE $header; print FILE "\\end{verbatim}\n"; print FILE "*}\n"; print FILE "\n"; print FILE "theorem assumes \""; print FILE; print FILE "\"\n"; print FILE "shows \"False\"\n"; # negate the whole CNF formula print FILE "using prems\n"; print FILE "oops\n"; print FILE "\n"; print FILE "end\n"; close FILE || die $!; print STDERR " done.\n";}## mainforeach $file (@ARGV) { eval { &dimacs2hol($file); }; if ($@) { print STDERR "\n*** dimacs2hol $file: ", $@, "\n"; unlink "$file.thy"; }}