stp(1) - f36

1STP(1)                           User Commands                          STP(1)
2
3
4

NAME

6       stp - Simple Theorem Prover SMT solver
7

DESCRIPTION

9       USAGE: stp [options] <input-file>
10
11              where  input  is  SMTLIB1/2 or CVC depending on options and file
12              extension
13
14   Most important options:
15       -h [ --help ]
16              print this help
17
18       --version
19              print version number
20
21   Simplifications:
22       --disable-simplifications
23              disable all simplifications
24
25       -w [ --switch-word ]
26              switch off wordlevel solver
27
28       -a [ --disable-opt-inc ]
29              disable potentially size-increasing optimisations
30
31       --disable-cbitp
32              disable constant bit propagation
33
34       --disable-equality
35              disable equality propagation
36
37   SAT Solver options:
38       --cryptominisat
39              use cryptominisat as the solver. Only use CryptoMiniSat  5.0  or
40              above (default).
41
42       --threads arg (=1)
43              Number of threads for cryptominisat
44
45       --simplifying-minisat
46              use installed simplifying minisat version as the solver
47
48       --minisat
49              use installed minisat version as the solver
50
51   Refinement options:
52       -r [ --ackermanize ]
53              eagerly encode array-read axioms (Ackermannistaion)
54
55   Printing options:
56       -b [ --print-stpinput ]
57              print STP input back to cout
58
59       --print-back-CVC
60              print input in CVC format, then exit
61
62       --print-back-SMTLIB2
63              print input in SMT-LIB2 format, then exit
64
65       --print-back-SMTLIB1
66              print input in SMT-LIB1 format, then exit
67
68       --print-back-GDL
69              print AiSee's graph format, then exit
70
71       --print-back-dot
72              print dotty/neato's graph format, then exit
73
74       -p [ --print-counterex ]
75              print counterexample
76
77       -y [ --print-counterexbin ]
78              print counterexample in binary
79
80       -q [ --print-arrayval ]
81              print arrayval declared order
82
83       -s [ --print-functionstat ]
84              print function statistics
85
86       -t [ --print-quickstat ]
87              print quick statistics
88
89       -v [ --print-nodes ]
90              print nodes
91
92       -n [ --print-output ]
93              Print output
94
95   Input options:
96       -m [ --SMTLIB1 ]
97              use the SMT-LIB1 format parser
98
99       --SMTLIB2
100              use the SMT-LIB2 format parser
101
102       --CVC  use the CVC format parser
103
104   Output options:
105       --output-CNF
106              Save  the  CNF into output_[0..n].cnf. NOTE: variables cannot be
107              mapped back, and problems solved by the preprocessing simplifier
108              alone  will  not generate any CNF as the SAT solver is never in‐
109              voked
110
111       --output-bench
112              save in ABC's bench format to output.bench
113
114   Output options:
115       --exit-after-CNF
116              exit after the CNF has been generated
117
118       -g [ --timeout ] arg
119              Number of conflicts after which the  SAT  solver  gives  up.  -1
120              means never (default)
121
122       -d [ --check-sanity ]
123              construct counterexample and check it
124
125   Hidden options:
126       --file arg
127              input file
128

NAME

DESCRIPTION

SEE ALSO