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 rewriting simplifier
disable constant bit propagation
disable equality propagation
size reducing simplifications only
Unconstrained variables are eliminated.
Iterations of AIG rewriting to perform
Enable sharing-aware flattening of >2 arity nodes
Enable sharing-aware rewriting
Create new variables for some extracts
Use what is known to be true in an if-then-else node to simplify the true or false branches
Simplify the propositional core with AIGs
Simplify with interval analysis
Pure literals are replaced.
Nodes that are always true (e.g. asserted) are replaced through out the problem by true
Uses simple boolean algebra rules to combine conjuncts at the top level
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. -1 means always.
If the number of non-leaf nodes is fewer than this number, run size-reducing simplifications to a fixed-point. -1 means always.
potentially size increasing suite that transform nodes to constants
Undo size increasing simplifications if they haven't made the problem simpler

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)

unsigned division encoding variant 1
unsigned division encoding variant 2
unsigned division encoding variant 3
addition encoding variant 1
addition encoding variant 2
comparison encoding variant 1
unsigned multiplication variant
unsigned multiplication variant 2
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

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
Number of seconds after which the SAT solver gives up. -1 means never.
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.

January 2025 stp 2.3.3