STP(1) | User Commands | STP(1) |
NAME
stp - Simple Theorem Prover SMT solver
DESCRIPTION
USAGE: stp [options] <input-file>
- where input is SMTLIB1/2 or CVC depending on options and file extension
Most important options:
- -h [ --help ]
- print this help
- --version
- print version number
Simplifications:
- --disable-simplifications
- disable all simplifications
- -w [ --switch-word ]
- switch off wordlevel solver
- -a [ --disable-opt-inc ]
- disable rewriting simplifier
- --disable-cbitp
- disable constant bit propagation
- --disable-equality
- disable equality propagation
- --size-reducing-only
- size reducing simplifications only
- --unconstrained-variable-elimination arg (=1)
- Unconstrained variables are eliminated.
- --aig-rewrite-passes arg (=0)
- Iterations of AIG rewriting to perform
- --flattening arg (=0)
- Enable sharing-aware flattening of >2 arity nodes
- --rewriting arg (=1)
- Enable sharing-aware rewriting
- --split-extracts arg (=1)
- Create new variables for some extracts
- --ite-context-simplifications arg (=0)
- Use what is known to be true in an if-then-else node to simplify the true or false branches
- --aig-core-simplification arg (=0)
- Simplify the propositional core with AIGs
- --use-intervals arg (=1)
- Simplify with interval analysis
- --pure-literals arg (=1)
- Pure literals are replaced.
- --always-true arg (=0)
- Nodes that are always true (e.g. asserted) are replaced through out the problem by true
- --merge-same arg (=0)
- Uses simple boolean algebra rules to combine conjuncts at the top level
- --bit-blast-simplification 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. -1 means always.
- --size-reducing-fixed-point-limit arg (=0)
- If the number of non-leaf nodes is fewer than this number, run size-reducing simplifications to a fixed-point. -1 means always.
- --simplify-to-constants-only arg (=0) Use just the simplifications from the
- potentially size increasing suite that transform nodes to constants
- --difficulty-reversion arg (=1)
- Undo size increasing simplifications if they haven't made the problem simpler
SAT Solver options:
- --cryptominisat
- use cryptominisat as the solver. Only use CryptoMiniSat 5.0 or above (default).
- --threads arg (=1)
- Number of threads for cryptominisat
- --simplifying-minisat
- use installed simplifying minisat version as the solver
- --minisat
- use installed minisat version as the solver
Refinement options:
- -r [ --ackermanize ]
- eagerly encode array-read axioms (Ackermannistaion)
Bit-blasting options:
- --bb.div-v1 arg (=1)
- unsigned division encoding variant 1
- --bb.div-v2 arg (=1)
- unsigned division encoding variant 2
- --bb.div-v3 arg (=0)
- unsigned division encoding variant 3
- --bb.add-v1 arg (=1)
- addition encoding variant 1
- --bb.add-v2 arg (=1)
- addition encoding variant 2
- --bb.vle-v1 arg (=1)
- comparison encoding variant 1
- --bb.mult-variant arg (=1)
- unsigned multiplication variant
- --bb.mult-v2 arg (=0)
- unsigned multiplication variant 2
- --bb.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
Printing options:
- -b [ --print-stpinput ]
- print STP input back to cout
- --print-back-CVC
- print input in CVC format, then exit
- --print-back-SMTLIB2
- print input in SMT-LIB2 format, then exit
- --print-back-SMTLIB1
- print input in SMT-LIB1 format, then exit
- --print-back-GDL
- print AiSee's graph format, then exit
- --print-back-dot
- print dotty/neato's graph format, then exit
- -p [ --print-counterex ]
- print counterexample
- -y [ --print-counterexbin ]
- print counterexample in binary
- -q [ --print-arrayval ]
- print arrayval declared order
- -s [ --print-functionstat ]
- print function statistics
- -t [ --print-quickstat ]
- print quick statistics
- -v [ --print-nodes ]
- print nodes
- -n [ --print-output ]
- Print output
Input options:
- -m [ --SMTLIB1 ]
- use the SMT-LIB1 format parser
- --SMTLIB2
- use the SMT-LIB2 format parser
- --CVC
- use the CVC format parser
Output options:
- --output-CNF
- 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
- --output-bench
- save in ABC's bench format to output.bench
Output options:
- --exit-after-CNF
- exit after the CNF has been generated
- -g [ --max-num-confl ] arg (=-1)
- Number of conflicts after which the SAT solver gives up. -1 means never
- -k [ --max-time ] arg (=-1)
- Number of seconds after which the SAT solver gives up. -1 means never.
- -d [ --check-sanity ]
- construct counterexample and check it
Hidden options:
- --file arg
- input file
SEE ALSO
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 |