presconstelm
- orphan:
Usage
presconstelm [OPTION]... [INFILE [OUTFILE]]
Description
Reads a file containing a PRES, and applies constant parameter elimination to it. If OUTFILE is not present, standard output is used. If INFILE is not present, standard input is used.
Command line options
-a
, --check-quantifiers
also analyse which quantified parameters are constant
-c
, --compute-conditions
compute propagation conditions
-iFORMAT
, --in=FORMAT
use input format FORMAT:
pres
PRES in internal format
text
PRES in textual (mCRL2) format
-oFORMAT
, --out=FORMAT
use output format FORMAT:
pres
PRES in internal format
text
PRES in textual (mCRL2) format
-pNAME
, --pres-rewriter=NAME
use pres rewrite strategy NAME:
simplify
for simplification
quantifier-all
for eliminating all quantifiers
quantifier-finite
for eliminating finite quantifier variables
quantifier-inside
for pushing quantifiers inside
quantifier-one-point
for one point rule quantifier elimination
-QNUM
, --qlimit=NUM
limit enumeration of universal and existential quantifiers in data expressions to NUM iterations (default NUM=10, NUM=0 for unlimited).
-e
, --remove-equations
remove redundant equations
-rNAME
, --rewriter=NAME
use rewrite strategy NAME:
jitty
jitty rewriting
jittyc
compiled jitty rewriting
jittyp
jitty rewriting with prover
--timings[=FILE]
append timing measurements to FILE. Measurements are written to standard error if no FILE is provided
Standard options
-q
, --quiet
do not display warning messages
-v
, --verbose
display short log messages
-d
, --debug
display detailed log messages
--log-level=LEVEL
display log messages up to and including level; either warn, verbose, debug or trace
-h
, --help
display help information
--version
display version information
--help-all
display help information, including hidden and experimental options