.\" DO NOT MODIFY THIS FILE!  It was generated by help2man 1.49.3.
.TH STP "1" "April 2024" "stp 2.3.3" "User Commands"
.SH NAME
stp \- Simple\ Theorem\ Prover\ SMT\ solver
.SH DESCRIPTION
USAGE: stp [options] <input\-file>
.IP
where input is SMTLIB1/2 or CVC depending on options and file extension
.SS "Most important options:"
.TP
\fB\-h\fR [ \fB\-\-help\fR ]
print this help
.TP
\fB\-\-version\fR
print version number
.SS "Simplifications:"
.TP
\fB\-\-disable\-simplifications\fR
disable all simplifications
.TP
\fB\-w\fR [ \fB\-\-switch\-word\fR ]
switch off wordlevel solver
.TP
\fB\-a\fR [ \fB\-\-disable\-opt\-inc\fR ]
disable potentially size\-increasing
optimisations
.TP
\fB\-\-disable\-cbitp\fR
disable constant bit propagation
.TP
\fB\-\-disable\-equality\fR
disable equality propagation
.SS "SAT Solver options:"
.TP
\fB\-\-cryptominisat\fR
use cryptominisat as the solver. Only use
CryptoMiniSat 5.0 or above (default).
.TP
\fB\-\-threads\fR arg (=1)
Number of threads for cryptominisat
.TP
\fB\-\-simplifying\-minisat\fR
use installed simplifying minisat version as
the solver
.TP
\fB\-\-minisat\fR
use installed minisat version as the solver
.SS "Refinement options:"
.TP
\fB\-r\fR [ \fB\-\-ackermanize\fR ]
eagerly encode array\-read axioms
(Ackermannistaion)
.SS "Printing options:"
.TP
\fB\-b\fR [ \fB\-\-print\-stpinput\fR ]
print STP input back to cout
.TP
\fB\-\-print\-back\-CVC\fR
print input in CVC format, then exit
.TP
\fB\-\-print\-back\-SMTLIB2\fR
print input in SMT\-LIB2 format, then exit
.TP
\fB\-\-print\-back\-SMTLIB1\fR
print input in SMT\-LIB1 format, then exit
.TP
\fB\-\-print\-back\-GDL\fR
print AiSee's graph format, then exit
.TP
\fB\-\-print\-back\-dot\fR
print dotty/neato's graph format, then exit
.TP
\fB\-p\fR [ \fB\-\-print\-counterex\fR ]
print counterexample
.TP
\fB\-y\fR [ \fB\-\-print\-counterexbin\fR ]
print counterexample in binary
.TP
\fB\-q\fR [ \fB\-\-print\-arrayval\fR ]
print arrayval declared order
.TP
\fB\-s\fR [ \fB\-\-print\-functionstat\fR ]
print function statistics
.TP
\fB\-t\fR [ \fB\-\-print\-quickstat\fR ]
print quick statistics
.TP
\fB\-v\fR [ \fB\-\-print\-nodes\fR ]
print nodes
.TP
\fB\-n\fR [ \fB\-\-print\-output\fR ]
Print output
.SS "Input options:"
.TP
\fB\-m\fR [ \fB\-\-SMTLIB1\fR ]
use the SMT\-LIB1 format parser
.TP
\fB\-\-SMTLIB2\fR
use the SMT\-LIB2 format parser
.TP
\fB\-\-CVC\fR
use the CVC format parser
.SS "Output options:"
.TP
\fB\-\-output\-CNF\fR
Save the CNF into output_[0..n].cnf. NOTE:
variables cannot be mapped back, and problems
solved by the preprocessing simplifier alone
will not generate any CNF as the SAT solver is
never invoked
.TP
\fB\-\-output\-bench\fR
save in ABC's bench format to output.bench
.SS "Output options:"
.TP
\fB\-\-exit\-after\-CNF\fR
exit after the CNF has been generated
.TP
\fB\-g\fR [ \fB\-\-timeout\fR ] arg
Number of conflicts after which the SAT solver
gives up. \fB\-1\fR means never (default)
.TP
\fB\-d\fR [ \fB\-\-check\-sanity\fR ]
construct counterexample and check it
.SS "Hidden options:"
.TP
\fB\-\-file\fR arg
input file
.SH "SEE ALSO"
The full documentation for
.B stp
is maintained as a Texinfo manual.  If the
.B info
and
.B stp
programs are properly installed at your site, the command
.IP
.B info stp
.PP
should give you access to the complete manual.