#acl EditorsGroup:read,write,delete,revert,admin All:read

= LP2BV-2 =

== Team ==
 * Tomi	Janhunen (Aalto University)
 * Guohua Liu (Aalto University)
 * Jori Bomanson (Aalto University)
 * Ilkka Niemelä (Aalto University)

== Description ==
A given ASP program is grounded by GRINGO and the ground program is simplified by SMODELS, then the simplified program is normalized using LP2NORMAL2 and translated to bit vectors using LP2BV, and finally, the bit vectors are solved by Z3.

== System Settings ==
The main modules and option flags are as below: 
 * GRINGO 3.0.4 --shift 
 * SMODELS 2.34 -internal -nolookahead
 * LP2NORMAL2 1.1 -wp -wt -wh -wn -wy -cs
 * LP2BV 1.10 -f
 * Z3 4.3.1 --smt2

The input language is Gringo 3.
  
== References ==
 * Participant [[http://research.ics.aalto.fi/software/asp/lp2bv|URL]].
 * 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
 * A paper on LP2NORMAL2 has been submitted.