This software has been designed to be used between
lparse of the smodels
system or any compatible grounder
such as
gringo and
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.
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.
Linux binaries: lp2bv (version 1.10 / 64 bit)