'\" -*- coding: us-ascii -*- .if \n(.g .ds T< \\FC .if \n(.g .ds T> \\F[\n[.fam]] .de URL \\$2 \(la\\$1\(ra\\$3 .. .if \n(.g .mso www.tmac .TH spadesimp 1 "22 March 2011" "" "" .SH NAME spadesimp \- simplifies SPARK verification conditions .SH SYNOPSIS 'nh .fi .ad l \fBspadesimp\fR \kx .if (\nx>(\n(.l/2)) .nr x (\n(.l/5) 'in \n(.iu+\nxu [OPTIONS] [UNIT] 'in \n(.iu-\nxu .ad b 'hy .SH DESCRIPTION The Simplifier for SPARK, \fBspadesimp\fR, analyses verification conditions generated by the Examiner for SPARK and attempts to discharge them automatically. For each \*(T file read, the Simplifier will produce a \*(T (simplified vcs) file and an optional \*(T (simplifier log) file. .PP This manual page only summarises the \fBspadesimp\fR command-line flags, please refer to the full Simplifier manual for further information. .SH OPTIONS These options do not quite follow the usual GNU command line syntax as options start with a single dash instead of the usual two. .TP \*(T<\fB\-help\fR\*(T> Displays command line help. .TP \*(T<\fB\-version\fR\*(T> Displays version information. .TP \*(T<\fB\-nolog\fR\*(T> Do not generate a simplification log file. .TP \*(T<\fB\-log=\fR\*(T>\fIfile_spec\fR Specify filename for the simplification log file. .TP \*(T<\fB\-nowrap\fR\*(T> Do not line wrap output files. .TP \*(T<\fB\-verbose\fR\*(T> Display attempted simplification strategies. .TP \*(T<\fB\-nouserrules\fR\*(T> Do not use user rules. .TP \*(T<\fB\-plain\fR\*(T> Adopt a plain output style (e.g. no dates or version numbers). .TP \*(T<\fB\-typecheck\fR\*(T> Only typecheck the input files. .TP \*(T<\fB\-norenum\fR\*(T> Do not renumber hypotheses and conclusions in \*(T files. .TP \*(T<\fB\-nosimplification=\fR\*(T>\fIRANGES\fR, \*(T<\fB\-nostandardisation=\fR\*(T>\fIRANGES\fR, \*(T<\fB\-norule_substitution=\fR\*(T>\fIRANGES\fR, \*(T<\fB\-nocontradiction_hunt=\fR\*(T>\fIRANGES\fR, \*(T<\fB\-nosubstitution_elimination=\fR\*(T>\fIRANGES\fR, \*(T<\fB\-noexpression_reduction=\fR\*(T>\fIRANGES\fR Adjust strategy for different VCs. \fIRANGES\fR can be a comma separated list of ranges. Each range can be either a single VC number or a simple range of the form VC-VC. .TP \*(T<\fB\-complexity_limit=\fR\*(T>\fILIMIT\fR (Limit in range 10 .. 200) .TP \*(T<\fB\-depth_limit=\fR\*(T>\fILIMIT\fR (Limit in range 1 .. 10) .TP \*(T<\fB\-inference_limit=\fR\*(T>\fILIMIT\fR (Limit in range 10 .. 400) .SH "SEE ALSO" spark(1), sparksimp(1), zombiescope(1), victor(1), pogs(1) .PP sparkformat(1), sparkmake(1) .SH AUTHOR This manual page was written by Florian Schanda <\*(T> for the \fIDebian GNU/Linux\fR system (but may be used by others). Permission is granted to copy, distribute and/or modify this document under the terms of the GNU Free Documentation License, Version 1.3 or any later version published by the Free Software Foundation; with no Invariant Sections, no Front-Cover Texts and no Back-Cover Texts.