stp(1) - f32

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