OpenSMT supports an experimental feature called lookahead-splitting for constructing partitions that can be solved independently to decide the satisfiability of an input instance. For the moment the feature is not yet integrated into the main branch, but instead lies in a branch called satsolver-reorg.
To experiment with the code, please fetch the opensmt repository and switch to the correct branch before compiling:
$ https://github.com/usi-verification-and-security/opensmt$ mkdir build; cd build; cmake ..; make
The feature can be enabled directly by setting options in the .smt2 file. For example
(set-option :lookahead-split)
(set-option :split-num 4)
(set-option :split-format smt2)
(set-option :split-format-length "brief")
(set-option :output-dir "foo")
will instruct opensmt to run in the lookahead-split mode, produce four splits, using the smt2 file format for the output splits, to produce an assert containing only the partitioning constraints, and not the full instance, in the output, that will be placed in the directory "foo".
