The lookahead implementation in opensmt is now in the master branch of the opensmt git. To compile opensmt2, do
$ git clone https://scm.ti-edu.ch/repogit/opensmt2.git
$ mkdir build; cd build; cmake ..; make
The binary will be in ./src/bin/opensmt
Opensmt requires the gmp libary for arbirary precision mathematics, and the readline library to compile.
To run opensmt in lookahead mode, add the line
(set-option :pure-lookahead 1)
to your smtlib2 file. For your convenience, you may also write this line to a separate smtlib2 file, say, la-config.smt2, and then run opensmt on an smtlib2 instance called instance.smt2 by
$ ./src/bin/opensmt la-config.smt2 problem.smt2
OpenSMT supports an experimental feature called lookahead-splitting for constructing partitions that can be solved independetly to decide the satisfiability of an input instance. For the moment the feature is not yet integrated to 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:
$ git clone https://scm.ti-edu.ch/repogit/opensmt2.git
$ git checkout satsolver-reorg
$ 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")