lib/scripts/dimacs2hol.pl
changeset 20420 56ef2dfc41d6
parent 15153 3f3926337c39
child 29145 b1c6f4563df7
equal deleted inserted replaced
20419:df257a9cf0e9 20420:56ef2dfc41d6
    40     s/^c.*\n//gm;                            # remove further comments
    40     s/^c.*\n//gm;                            # remove further comments
    41     s/\A\s*//;                               # remove leading whitespace
    41     s/\A\s*//;                               # remove leading whitespace
    42     s/(\s+0)?\s*\z//;                        # remove trailing whitespace, and possibly a last '0'
    42     s/(\s+0)?\s*\z//;                        # remove trailing whitespace, and possibly a last '0'
    43     s/-/~/g;                                 # replace '-' by '~' (negation in HOL)
    43     s/-/~/g;                                 # replace '-' by '~' (negation in HOL)
    44     s/[1-9]\d*/v$&/g;                        # add 'v' before variables
    44     s/[1-9]\d*/v$&/g;                        # add 'v' before variables
    45     s/(\s+)0(\s+)/\)$1&$2\(/g;               # replace ' 0 ' by ') & ('
    45     s/\s+0\s+/\"\nand \"/g;                  # replace ' 0 ' by '"\nand "'
    46     s/(\d)(\s+[~v])/$1 |$2/g;                # insert ' |' between literals
    46     s/(\d)(\s+[~v])/$1 |$2/g;                # insert ' |' between literals
    47 
    47 
    48     my ($filename) = $file;
    48     my ($filename) = $file;
    49     $filename =~ s/.*\///g;                  # filter out directories, only leave what's after the last '/'
    49     $filename =~ s/.*\///g;                  # filter out directories, only leave what's after the last '/'
    50 
    50 
    60     print FILE "\\begin{verbatim}\n";
    60     print FILE "\\begin{verbatim}\n";
    61     print FILE $header;
    61     print FILE $header;
    62     print FILE "\\end{verbatim}\n";
    62     print FILE "\\end{verbatim}\n";
    63     print FILE "*}\n";
    63     print FILE "*}\n";
    64     print FILE "\n";
    64     print FILE "\n";
    65     print FILE "theorem \"~((";  # negate the whole CNF formula
    65     print FILE "theorem assumes \""; print FILE;
    66     print FILE;
    66     print FILE "\"\n";
    67     print FILE "))\"\n";
    67     print FILE "shows \"False\"\n";  # negate the whole CNF formula
       
    68     print FILE "using prems\n";
    68     print FILE "oops\n";
    69     print FILE "oops\n";
    69     print FILE "\n";
    70     print FILE "\n";
    70     print FILE "end\n";
    71     print FILE "end\n";
    71 
    72 
    72     close FILE || die $!;
    73     close FILE || die $!;