stp1

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.

--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

--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

--search-bias arg

tune the SAT search towards one answer: 'unsat' (best for unsatisfiable / verification workloads), 'sat', or 'none' (the default, leaving the solver at its own settings). Solvers with no such setting ignore it

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:

--cnf-generation-effort arg (=medium) effort spent minimising the CNF:

very-low, low, medium, high, very-high. Higher is slower to generate but yields a smaller CNF

--exit-after-CNF

exit after the CNF has been generated

--parse-only

exit after parsing the input, without solving

--interactive arg

read the input a character at a time, as needed when driving stp interactively over a pipe. Off reads in blocks, which is faster. Default: on when reading from stdin, off when reading from a file. SMT-LIB2 only.

-g [ --max-num-confl ] arg (=-1)

Number of conflicts after which the SAT solver gives up. -1 means never, 0 means give up without searching.

-k [ --max-time ] arg (=-1)

Number of seconds after which the SAT solver gives up. The budget is for the whole query, not for each call into the SAT solver. -1 means never, 0 means give up without searching.

-d [ --check-sanity ]

construct counterexample and check it

Hidden options:

--file arg

input file