equal
deleted
inserted
replaced
|
1 #!/usr/bin/env bash |
|
2 # |
|
3 # $Id$ |
|
4 # Author: Tjark Weber |
|
5 # Copyright 2004 |
|
6 # |
|
7 # DESCRIPTION: convert DIMACS CNF files into Isabelle/HOL theories |
|
8 |
|
9 |
|
10 ## diagnostics |
|
11 |
|
12 PRG="$(basename "$0")" |
|
13 |
|
14 function usage() |
|
15 { |
|
16 echo |
|
17 echo "Usage: $PRG FILES" |
|
18 echo |
|
19 echo " Convert files in DIMACS CNF format [1] into Isabelle/HOL theories." |
|
20 echo |
|
21 echo " For each CNF file, a theory file (with '.thy' appended to the original" |
|
22 echo " filename) is generated. The CNF files are not modified." |
|
23 echo |
|
24 echo " This script is not too strict about the format of the input file. However," |
|
25 echo " in rare cases it may produce a theory that will not be accepted by" |
|
26 echo " Isabelle/HOL (e.g. when a CNF file contains '\\end{verbatim}' or '*}' in a" |
|
27 echo " comment)." |
|
28 echo |
|
29 echo " Each CNF file must contain at least one clause, and may not contain empty" |
|
30 echo " clauses (i.e. '0' immediately followed by another '0')." |
|
31 echo |
|
32 echo " The CNF formula is negated, so that an unsatisfiable formula becomes" |
|
33 echo " provable." |
|
34 echo |
|
35 echo " [1] ftp://dimacs.rutgers.edu/pub/challenge/satisfiability/doc/satformat.dvi" |
|
36 echo |
|
37 exit 1 |
|
38 } |
|
39 |
|
40 |
|
41 ## process command line |
|
42 |
|
43 [ "$#" -eq 0 -o "$1" = "-?" ] && usage |
|
44 |
|
45 |
|
46 ## main |
|
47 |
|
48 #set by configure |
|
49 AUTO_PERL=perl |
|
50 |
|
51 "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/dimacs2hol.pl" "$@" |