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

NAME

6       mobical - manual page for mobical 1.5.2
7

DESCRIPTION

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       Otherwise if no '<mode>' is specified the default is to generate random
95       traces internally until the execution of a trace fails, which means  it
96       produces  a  non-zero  exit code.  Then the trace is rerun and shrunken
97       through delta-debugging to produce a smaller trace.  The shrunken fail‐
98       ing  trace  is written as 'red-<seed>.trace' to the current working di‐
99       rectory.
100
101       The following options disable certain parts of the shrinking algorithm:
102
103       --do-not-shrink[-at-all]
104
105       --do-not-add-options[-before-shrinking]
106
107       --do-not-shrink-phases
108
109       --do-not-shrink-clauses
110
111       --do-not-shrink-literals
112
113       --do-not-shrink-basic[-calls]
114
115       --do-not-disable[-options]
116
117       --do-not-reduce[[-option]-values]
118
119       --do-not-shrink-variables
120
121       --do-not-shrink-options
122
123       The standard mode of using the model based tester is  to  start  it  in
124       random  testing mode without '<input>', '<seed>' nor '<output>' option.
125       If a failing trace is found it will be shrunken and the resulting trace
126       written  to the current working directory.  Then the model based tester
127       can be interrupted and then called  again  with  the  produced  failing
128       trace  as  single  argument.   This  invocation  will execute the trace
129       within the same process and thus can directly be  investigated  with  a
130       symbolic  debugger  such as 'gdb' or maybe first checked for memory is‐
131       sues with 'valgrind' or recompilation  with  memory  checking  '-fsani‐
132       tize=address'.
133
134
135
136mobical 1.5.2                    October 2021                       MOBICAL(1)