presrewr
- orphan:
Usage
presrewr [OPTION]... [INFILE [OUTFILE]]
Description
Rewrite the PRES in INFILE, remove quantified variables and write the resulting PRES to OUTFILE. If INFILE is not present, stdin is used. If OUTFILE is not present, stdout is used.
Command line options
-iFORMAT , --in=FORMAT
use input format FORMAT:
presPRES in internal format
textPRES in textual (mCRL2) format
-oFORMAT , --out=FORMAT
use output format FORMAT:
presPRES in internal format
textPRES in textual (mCRL2) format
-pNAME , --pres-rewriter=NAME
use pres rewrite strategy NAME:
simplifyfor simplification
quantifier-allfor eliminating all quantifiers
quantifier-finitefor eliminating finite quantifier variables
quantifier-insidefor pushing quantifiers inside
quantifier-one-pointfor one point rule quantifier elimination
-QNUM , --qlimit=NUM
limit enumeration of quantifiers to NUM iterations. (Default NUM=1000, NUM=0 for unlimited).
-rNAME , --rewriter=NAME
use rewrite strategy NAME:
jittyjitty rewriting
jittyccompiled jitty rewriting
jittypjitty 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