stp - Man Page

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.

Info

March 2021 stp 2.3.3