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 potentially size-increasing optimisations

       --disable-cbitp
              disable constant bit propagation

       --disable-equality
              disable equality propagation

   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)

   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 [ --timeout ] arg
              Number of conflicts after which the SAT solver gives up. -1
              means never (default)

       -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                         April 2024                            STP(1)