NAME¶

mobical - CaDiCaL Simplified Satisfiability Solver

DESCRIPTION¶

usage: mobical [ <option> ... ] [ <mode> ]

where '<option>' can be one of the following:

--help

| -h print this command line option summary and exit

--version

print CaDiCaL's three character version and exit

--build

print build configuration

-v

increase verbosity

--colors

force colors for both '<stdout>' and '<stderr>'

--no-colors

disable colors if '<stderr>' is connected to terminal

--no-terminal

assume '<stderr>' is not connected to terminal

--no-seeds

do not print seeds in random mode

-<n>

specify the number of solving phases explicitly

--time <seconds>

set time limit per trace (none=0, default=10)

--space <MB>

set space limit (none=0, default=1024)

--do-not-ignore-resource-limits

consider out-of-time or memory as error

--small

generate small formulas only

--medium

generate medium sized formulas only

--big

generate big formulas only

Then '<mode>' is one of these

<seed>

generate and execute trace for given 64-bit seed

<seed>

<output> generate trace, shrink and write it to file

<input> <output>

read trace, shrink and write it to output file

<input>

read and replay the specified input trace

The output trace is not shrunken if it is not failing. However, before it is written it is executed, unless '--do-not-execute' is specified:

--do-not-execute

just write to '<output>' without execution

In order to check memory issues or collect coverage you can force execution within the main process, which however also means that the model based tester aborts as soon a test fails

--do-not-fork

execute all tests in main process directly

In order to replay a trace which violates an API contract use

--do-not-enforce-contracts

To read from '<stdin>' use '-' as '<input>' and also '-' instead of '<output>' to write to '<stdout>'.

Implicitly add 'dump' and 'stats' calls to traces:

--dump

| -d force dumping the CNF before every 'solve'

--stats | -s

force printing statistics after every 'solve'

Implicitly add 'configure plain' after setting options:

--plain | -p

Otherwise if no '<mode>' is specified the default is to generate random traces internally until the execution of a trace fails, which means it produces a non-zero exit code. Then the trace is rerun and shrunken through delta-debugging to produce a smaller trace. The shrunken failing trace is written as 'red-<seed>.trace' to the current working directory.

The following options disable certain parts of the shrinking algorithm:

--do-not-shrink[-at-all]

--do-not-add-options[-before-shrinking]

--do-not-shrink-phases

--do-not-shrink-clauses

--do-not-shrink-literals

--do-not-shrink-basic[-calls]

--do-not-disable[-options]

--do-not-reduce[[-option]-values]

--do-not-shrink-variables

--do-not-shrink-options

The standard mode of using the model based tester is to start it in random testing mode without '<input>', '<seed>' nor '<output>' option. If a failing trace is found it will be shrunken and the resulting trace written to the current working directory. Then the model based tester can be interrupted and then called again with the produced failing trace as single argument. This invocation will execute the trace within the same process and thus can directly be investigated with a symbolic debugger such as 'gdb' or maybe first checked for memory issues with 'valgrind' or recompilation with memory checking '-fsanitize=address'.