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.

stp 2.3.3                        January 2025                           STP(1)