LP2BV: Translating Normal/Smodels Programs for SMT (bit vector) solvers

This software has been designed to be used between

  1. the front-end lparse of the smodels system or any compatible grounder such as gringo and
  2. any SMT solver supporting the QF_BV dialect (bit vectors) of the SMT library.

Related Publications

Mai Nguyen, Tomi Janhunen, and Ilkka Niemelš: Translating Answer-Set Programs into Bit-Vector Logic. In the Proceedings of the 19th International Conference on Applications of Declarative Programming and Knowledge Management, 105—116. Vienna, Austria, September 2011.

Ilkka Niemelš: Stable Models and Difference Logic. Annals of Mathematics and Artificial Intelligence, 53 (1—4), 313—329, 2008.


Using the Software

The following example demonstrates the use of our translator with the SMT solver Boolector:

$ lparse program.lp > program.sm
$ lp2bv program.sm > program.bvl
$ boolector --smt2 -m program.bvl > model.out

First, the source code program.lp is grounded using lparse. Then, the resulting ground program is translated into QF_BV format. Last, an SMT solver is invoked to compute a stable model. The given example is merely about checking the existence of a stable model because the transformation implemented by lp2bv does not preserve symbolic names of atoms (they would be interpreted differently under QF_BV anyway).

The actual answer set can be recovered using two additional tools, lpcat and interpret, from the asptools collection. When used with lp2bv, they are invoked roughly as follows.

$ lparse program.lp | lpcat -s=symbols.sm | lp2bv -f > program.bvl
$ boolector --smt2 -m program.bvl > model.out
$ cat model.out | fgrep var_ | egrep " 1$" | interpret symbols.sm

The last command line is specific to boolector and, for simplicity, all pretty printing aspects have been omitted. To this end, you might want to use sed or write a perl script of your own. For futher hints, feel free to consult a sample callscript which uses gringo as a grounder. It also shows how smodels can be used as a preprocessor to lp2bv in order to reduce the input program.


Disclaimer

The software below is provided on "as is" basis, without warranties of any kind or fitness for a particular purpose.

Copyright

The copyright for the binaries is held by Aalto University and Tomi Janhunen.
You may freely use this software for academic and research purposes but not redistribute it.

Download

Linux binaries: lp2bv (version 1.10 / 64 bit)


[TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links]
Latest update: 21 May 2013. Tomi Janhunen