Running STP¶
stp is the solver’s command-line front end, and the only program an
installation puts on the path. It reads one problem, from a file or from
standard input, and writes the answer to standard output:
stp [options] [input-file]
stp --help lists every option, with its default where it has one,
and man stp shows the same list where the manpage was installed – on
Linux, a build makes it whenever help2man is available.
stp --version prints the version, the commit it was built from, the
build configuration and the SAT solvers compiled in.
Input¶
With no file named, stp reads standard input. The input is SMT-LIB2,
whatever the file is called; --SMTLIB2 is accepted, and changes
nothing. (Releases up to 2.4 also read STP’s original CVC language and the
pre-2010 SMT-LIB1 format.)
stp problem.smt2
stp < problem.smt2
Output¶
An SMT-LIB2 input is a script, and STP answers its commands as it reaches
them: sat, unsat or unknown for each (check-sat), and the
responses to (get-model) and (get-value ...). Those two need
(set-option :produce-models true) before solving, or -p or
-d on the command line, and require a current satisfiable context.
Without the option, they report an error and end the script.
SMT-LIB 2.7 compatibility describes the command modes and other compatibility rules.
$ cat example.smt2
(set-option :produce-models true)
(set-logic QF_BV)
(declare-fun x () (_ BitVec 8))
(declare-fun y () (_ BitVec 8))
(assert (= (bvadd x y) #x10))
(assert (bvugt x #x0c))
(check-sat)
(get-value (x))
(exit)
$ stp example.smt2
sat
(
( |x| #xFF )
)
-p (--print-counterex) prints a model with every satisfiable
answer without the input asking for one, as define-fun lines after
the answer.
Exit status¶
stp exits with 0 once it has read and answered the input, whatever
the answers were – unsat and unknown included. It exits
non-zero when it could not: usually with 255, for an unreadable file, an
unknown or conflicting option, or an input it rejected. STP stops at the first error in an SMT-LIB2 script, usually
printing an (error "...") response saying why; answers already given
to earlier (check-sat) commands stand. Read the answers from standard
output, not from the exit status.
Driving STP over a pipe¶
When it reads standard input, stp reads SMT-LIB2 a character at a
time, so a program can write one command, wait for the answer and write
the next:
(set-logic QF_BV)
(declare-fun x () (_ BitVec 4))
(assert (= x #x3))
(check-sat) ; answers sat
(push 1)
(assert (= x #x4))
(check-sat) ; unsat
(pop 1)
(check-sat) ; sat
(exit)
--interactive=false reads standard input in blocks instead, which is
faster when the whole script is already there; --interactive=true
does the reverse for a named file, such as a FIFO. Both are for
SMT-LIB2 only. STP can keep the SAT
solver and the encoding between the checks of a script like this one;
Incremental solving describes when it does, and the
--incremental option that controls it.
Choosing a SAT solver¶
STP translates what its preprocessing leaves into SAT. Which SAT solvers
are available depends on how STP was built (Building STP);
stp --version lists them on the STP SAT solvers line. When more
than one is compiled in, STP uses CryptoMiniSat, then CaDiCaL, then
MiniSat, whichever it finds first. One flag picks another for a run:
Option |
Solver |
|---|---|
|
CaDiCaL |
|
CryptoMiniSat; |
|
MiniSat |
|
MiniSat with its variable elimination |
The flags exclude one another, and --sat-backend names the solver
instead (cryptominisat, cadical, minisat or
simplifying-minisat; auto, the default, is the order above), as the
API’s sat-backend option does. --search-bias unsat tunes the solver
for problems that are expected to be unsatisfiable, such as verification
conditions, and --search-bias sat for the reverse; a solver with no
such setting warns and ignores it.
Limits¶
-k N (--max-time) gives each check N seconds, counted from
its start and so including preprocessing and building the CNF. -g N
(--max-num-confl) gives each call into the SAT solver N conflicts;
a check that refines its encoding makes several calls. A check that runs
out answers unknown. Parsing is not counted, and the deadline is
tested between stages rather than enforced, so a hard wall-clock limit
still needs timeout(1) or similar around stp.
Stack size¶
STP recurses over the formula, and deeply nested inputs can overflow the
8 MB stack most Linux systems give a process by default. The symptom is a
segmentation fault. Raise the limit in the shell that runs stp:
ulimit -s 80000 # about 80 MB
Checking and statistics¶
Option |
Effect |
|---|---|
|
build each satisfying assignment and check it against the input before answering |
|
print the time spent in each stage, and the process’s peak memory, to standard error after each check |
|
trace the solve: node counts after each simplification on standard output, mixed with the answers, and what each pass did on standard error |
|
read the input without solving it: an SMT-LIB2 script’s other
commands still run, but |
Controlling preprocessing¶
STP simplifies the formula at the word level before bit-blasting it. The
Simplifications group of stp --help switches individual passes on
and off. The broad switches are:
Option |
Effect |
|---|---|
|
turn off the word-level simplifications listed with it in the help |
|
turn off the simplifications that can enlarge the formula |
|
turn off the rewriting simplifier |
|
turn off the word-level equation solver |
|
turn off constant bit propagation |
|
turn off equality propagation |
An option that takes a value accepts it either separately or after
= – --flattening 0 and --flattening=false are the same –
except --incremental, whose value must follow =. Contradictory
options are rejected rather than one silently winning:
--disable-simplifications --flattening 1 is an error.
Architecture describes the passes these options control.
Writing CNF¶
--output-CNF writes the CNF STP hands to the SAT solver as DIMACS
files named output_0.cnf, output_1.cnf and so on, one per
check, in the current directory, replacing any a previous run left. Its
variables cannot be mapped back to the input’s. A check that
preprocessing answers on its own reaches no SAT solver and writes no
file, and neither does a check solved incrementally
(Incremental solving). Under lazy array-read refinement or a
bit-vector abstraction the file is not the whole problem, and a warning
says so: --ackermanize completes it for arrays.
--exit-after-CNF exits, with no answer, once the first CNF is built;
the two options together turn a single-check problem into DIMACS.
--cnf-generation-effort trades the time spent minimising the CNF
against its size. --cnf-link-shared-cells makes the new-* rungs
keep a comparator cell propagation-complete when its exclusive-or has
another reader, at the price of a few more clauses.
Other options¶
The Bit-blasting options group (--bb.*) chooses how each
operation is encoded as CNF; it has no page of its own, and
stp --help describes each option. The --cadical-* options in the
SAT Solver options group tune CaDiCaL, and the rest of the
Printing options group are debugging aids. -r
(--ackermanize) expands every array read eagerly, instead of
refining array reads lazily as STP does by default.
Options for particular theories are spread through stp --help; each
theory’s page covers its own:
Page |
Options |
|---|---|
|
|
|
|
|
|
|
|
the |
|
the |
Other programs¶
The other programs under tools/ in the source tree are for working on
STP, and none of them is installed: Developer tools describes them.
