lookahead

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") 

 

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".