[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

9. deprose


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

9.1 NAME

deprose - condenses checkstat error output


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

9.2 SYNOPSIS

deprose [infile] [outfile]
[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

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.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

9.4 AUTHORS

Thorsten Engel
Christian Theobalt
Contact : Christoph Weidenbach <weidenb@mpi-sb.mpg.de>


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

9.5 SEE ALSO

checkstat(1), filestat(1), pcs(1), pgen(1), rescmp(1), tpform(1), tpget(1), dfg2otter(1), dfg2otterpl(1), SPASS(1)


[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

This document was generated by Renate Schmidt on March, 10 2003 using texi2html