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