9. deprose
9.1 NAME
deprose - condenses checkstat error output
9.2 SYNOPSIS
deprose [infile] [outfile]
9.3 DESCRIPTION
deprose is a Perl script for condensing checkstat error output.
As input, it gets an arbitrary text containing messages of the
following form:
| * Problem 'xy':
* SPASS computes problem state 'satisfiable'
* which is declared 'unsatisfiable'
|
deprose outputs an annotated list of the files in which
errors occurred. Each file in this list is annotated with
'+', if SPASS found a proof on this file, or '--', if SPASS
found a model.
If no file arguments are given, deprose reads from stdin and writes to
stdout. If one file argument is given, deprose reads from that file, and if
a second argument is given, deprose writes to that file.
9.4 AUTHORS
Thorsten Engel
Christian Theobalt
Contact : Christoph Weidenbach <weidenb@mpi-sb.mpg.de>
9.5 SEE ALSO
checkstat(1), filestat(1), pcs(1), pgen(1), rescmp(1), tpform(1), tpget(1), dfg2otter(1), dfg2otterpl(1), SPASS(1)
This document was generated
by Renate Schmidt on March, 10 2003
using texi2html