STP(1) User Commands STP(1)

stp - Simple Theorem Prover SMT solver

USAGE: stp [options] <input-file>

where input is SMTLIB1/2 or CVC depending on options and file extension

print this help
print version number

disable all simplifications
switch off wordlevel solver
disable potentially size-increasing optimisations
disable constant bit propagation
disable equality propagation

use cryptominisat as the solver. Only use CryptoMiniSat 5.0 or above (default).
Number of threads for cryptominisat
use installed simplifying minisat version as the solver
use installed minisat version as the solver

eagerly encode array-read axioms (Ackermannistaion)

print STP input back to cout
print input in CVC format, then exit
print input in SMT-LIB2 format, then exit
print input in SMT-LIB1 format, then exit
print AiSee's graph format, then exit
print dotty/neato's graph format, then exit
print counterexample
print counterexample in binary
print arrayval declared order
print function statistics
print quick statistics
print nodes
Print output

use the SMT-LIB1 format parser
use the SMT-LIB2 format parser
use the CVC format parser

Output options:

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
save in ABC's bench format to output.bench

Output options:

exit after the CNF has been generated
Number of conflicts after which the SAT solver gives up. -1 means never (default)
construct counterexample and check it

input file

The full documentation for stp is maintained as a Texinfo manual. If the info and stp programs are properly installed at your site, the command

info stp

should give you access to the complete manual.

September 2023 stp 2.3.3