stp - Man Page

print this help

print version number

disable all simplifications

switch off wordlevel solver

disable potentially size-increasing optimisations

disable constant bit propagation

disable equality propagation

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)

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

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

exit after the CNF has been generated

Number of conflicts after which the SAT solver gives up. -1 means never (default)

construct counterexample and check it

input file