stp - Man Page

print this help

print version number

disable all simplifications

switch off wordlevel solver

disable rewriting simplifier

disable constant bit propagation

disable equality propagation

size reducing simplifications only

Unconstrained variables are eliminated.

Iterations of AIG rewriting to perform

Enable sharing-aware flattening of >2 arity nodes

Enable sharing-aware rewriting

Create new variables for some extracts

Use what is known to be true in an if-then-else node to simplify the true or false branches

Simplify the propositional core with AIGs

Simplify with interval analysis

Pure literals are replaced.

Nodes that are always true (e.g. asserted) are replaced through out the problem by true

Uses simple boolean algebra rules to combine conjuncts at the top level

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.

If the number of non-leaf nodes is fewer than this number, run size-reducing simplifications to a fixed-point. -1 means always.

potentially size increasing suite that transform nodes to constants

Undo size increasing simplifications if they haven't made the problem simpler

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)

unsigned division encoding variant 1

unsigned division encoding variant 2

unsigned division encoding variant 3

addition encoding variant 1

addition encoding variant 2

comparison encoding variant 1

unsigned multiplication variant

unsigned multiplication variant 2

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

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

Number of seconds after which the SAT solver gives up. -1 means never.

construct counterexample and check it

input file