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