.\" DO NOT MODIFY THIS FILE!  It was generated by help2man 1.49.3.
.TH STP "1" "November 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 rewriting simplifier
.TP
\fB\-\-disable\-cbitp\fR
disable constant bit propagation
.TP
\fB\-\-disable\-equality\fR
disable equality propagation
.TP
\fB\-\-size\-reducing\-only\fR
size reducing simplifications only
.TP
\fB\-\-unconstrained\-variable\-elimination\fR arg (=1)
Unconstrained variables are eliminated.
.TP
\fB\-\-aig\-rewrite\-passes\fR arg (=0)
Iterations of AIG rewriting to perform
.TP
\fB\-\-flattening\fR arg (=0)
Enable sharing\-aware flattening of >2
arity nodes
.TP
\fB\-\-rewriting\fR arg (=1)
Enable sharing\-aware rewriting
.TP
\fB\-\-split\-extracts\fR arg (=1)
Create new variables for some extracts
.TP
\fB\-\-ite\-context\-simplifications\fR arg (=0)
Use what is known to be true in an
if\-then\-else node to simplify the true
or false branches
.TP
\fB\-\-aig\-core\-simplification\fR arg (=0)
Simplify the propositional core with
AIGs
.TP
\fB\-\-use\-intervals\fR arg (=1)
Simplify with interval analysis
.TP
\fB\-\-pure\-literals\fR arg (=1)
Pure literals are replaced.
.TP
\fB\-\-always\-true\fR arg (=0)
Nodes that are always true (e.g.
asserted) are replaced through out the
problem by true
.TP
\fB\-\-merge\-same\fR arg (=0)
Uses simple boolean algebra rules to
combine conjuncts at the top level
.TP
\fB\-\-bit\-blast\-simplification\fR arg (=0)
Part\-way through simplifying, convert
to AIGs and look for bits that the AIGs
figure out are true/false or the same
as another node. If the difficulty is
less than this number. \fB\-1\fR means always.
.TP
\fB\-\-size\-reducing\-fixed\-point\-limit\fR arg (=0)
If the number of non\-leaf nodes is
fewer than this number, run
size\-reducing simplifications to a
fixed\-point. \fB\-1\fR means always.
.TP
\fB\-\-simplify\-to\-constants\-only\fR arg (=0) Use just the simplifications from the
potentially size increasing suite that
transform nodes to constants
.TP
\fB\-\-difficulty\-reversion\fR arg (=1)
Undo size increasing simplifications if
they haven't made the problem simpler
.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 "Bit-blasting options:"
.TP
\fB\-\-bb\fR.div\-v1 arg (=1)
unsigned division encoding variant 1
.TP
\fB\-\-bb\fR.div\-v2 arg (=1)
unsigned division encoding variant 2
.TP
\fB\-\-bb\fR.div\-v3 arg (=0)
unsigned division encoding variant 3
.TP
\fB\-\-bb\fR.add\-v1 arg (=1)
addition encoding variant 1
.TP
\fB\-\-bb\fR.add\-v2 arg (=1)
addition encoding variant 2
.TP
\fB\-\-bb\fR.vle\-v1 arg (=1)
comparison encoding variant 1
.TP
\fB\-\-bb\fR.mult\-variant arg (=1)
unsigned multiplication variant
.TP
\fB\-\-bb\fR.mult\-v2 arg (=0)
unsigned multiplication variant 2
.TP
\fB\-\-bb\fR.conjoin\-constant arg (=0)
When constant\-bit propagation detects a
constant bit during AIG construction,
assert the AIG node and replace it, in
the AIG, by the constant bit
.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\-\-max\-num\-confl\fR ] arg (=\-1)
Number of conflicts after which the SAT
solver gives up. \fB\-1\fR means never
.TP
\fB\-k\fR [ \fB\-\-max\-time\fR ] arg (=\-1)
Number of seconds after which the SAT
solver gives up. \fB\-1\fR means never.
.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.