1MOBICAL(1) User Commands MOBICAL(1)
2
3
4
6 mobical - manual page for mobical 1.7.3
7
9 usage: mobical [ <option> ... ] [ <mode> ]
10
11 where '<option>' can be one of the following:
12
13 --help | -h print this command line option summary and exit
14
15 --version
16 print CaDiCaL's three character version and exit
17
18 --build
19 print build configuration
20
21 -v increase verbosity
22
23 --colors
24 force colors for both '<stdout>' and '<stderr>'
25
26 --no-colors
27 disable colors if '<stderr>' is connected to terminal
28
29 --no-terminal
30 assume '<stderr>' is not connected to terminal
31
32 --no-seeds
33 do not print seeds in random mode
34
35 -<n> specify the number of solving phases explicitly
36
37 --time <seconds>
38 set time limit per trace (none=0, default=10)
39
40 --space <MB>
41 set space limit (none=0, default=1024)
42
43 --do-not-ignore-resource-limits
44 consider out-of-time or memory as error
45
46 --small
47 generate small formulas only
48
49 --medium
50 generate medium sized formulas only
51
52 --big generate big formulas only
53
54 Then '<mode>' is one of these
55
56 <seed> generate and execute trace for given 64-bit seed
57
58 <seed> <output> generate trace, shrink and write it to file
59
60 <input> <output>
61 read trace, shrink and write it to output file
62
63 <input>
64 read and replay the specified input trace
65
66 The output trace is not shrunken if it is not failing. However, before
67 it is written it is executed, unless '--do-not-execute' is specified:
68
69 --do-not-execute
70 just write to '<output>' without execution
71
72 In order to check memory issues or collect coverage you can force exe‐
73 cution within the main process, which however also means that the model
74 based tester aborts as soon a test fails
75
76 --do-not-fork
77 execute all tests in main process directly
78
79 In order to replay a trace which violates an API contract use
80
81 --do-not-enforce-contracts
82
83 To read from '<stdin>' use '-' as '<input>' and also '-' instead of
84 '<output>' to write to '<stdout>'.
85
86 Implicitly add 'dump' and 'stats' calls to traces:
87
88 --dump
89 | -d force dumping the CNF before every 'solve'
90
91 --stats | -s
92 force printing statistics after every 'solve'
93
94 Implicitly add 'configure plain' after setting options:
95
96 --plain | -p
97
98 Otherwise if no '<mode>' is specified the default is to generate random
99 traces internally until the execution of a trace fails, which means it
100 produces a non-zero exit code. Then the trace is rerun and shrunken
101 through delta-debugging to produce a smaller trace. The shrunken fail‐
102 ing trace is written as 'red-<seed>.trace' to the current working di‐
103 rectory.
104
105 The following options disable certain parts of the shrinking algorithm:
106
107 --do-not-shrink[-at-all]
108
109 --do-not-add-options[-before-shrinking]
110
111 --do-not-shrink-phases
112
113 --do-not-shrink-clauses
114
115 --do-not-shrink-literals
116
117 --do-not-shrink-basic[-calls]
118
119 --do-not-disable[-options]
120
121 --do-not-reduce[[-option]-values]
122
123 --do-not-shrink-variables
124
125 --do-not-shrink-options
126
127 The standard mode of using the model based tester is to start it in
128 random testing mode without '<input>', '<seed>' nor '<output>' option.
129 If a failing trace is found it will be shrunken and the resulting trace
130 written to the current working directory. Then the model based tester
131 can be interrupted and then called again with the produced failing
132 trace as single argument. This invocation will execute the trace
133 within the same process and thus can directly be investigated with a
134 symbolic debugger such as 'gdb' or maybe first checked for memory is‐
135 sues with 'valgrind' or recompilation with memory checking '-fsani‐
136 tize=address'.
137
138
139
140mobical 1.7.3 September 2023 MOBICAL(1)