{"id":20,"date":"2017-02-17T10:55:47","date_gmt":"2017-02-17T09:55:47","guid":{"rendered":"https:\/\/tapas.labri.fr\/wp\/?page_id=20"},"modified":"2017-02-22T11:27:44","modified_gmt":"2017-02-22T10:27:44","slug":"the-alambic-library-and-the-distiller-tool","status":"publish","type":"page","link":"https:\/\/tapas.labri.fr\/wp\/?page_id=20","title":{"rendered":"The Alambic library and the Distiller tool"},"content":{"rendered":"<h1>Alambic<\/h1>\n<p>The Alambic library is used to compile <a class=\"wiki\" href=\"https:\/\/tapas.labri.fr\/wp\/?page_id=17\">Armoise<\/a> formulas into calls to <a class=\"wiki\" href=\"https:\/\/tapas.labri.fr\/wp\/?page_id=13\">GENEPI<\/a> functions. The <a class=\"wiki\" href=\"https:\/\/tapas.labri.fr\/wp\/?page_id=17\">Armoise<\/a> language allows to specify sets that are not definable into the Presburger arithmetics (e.g. <tt>nat*nat<\/tt>). Furthermore, even if an <a class=\"wiki\" href=\"https:\/\/tapas.labri.fr\/wp\/?page_id=17\">Armoise<\/a> formula defines a Presburger arithmetics it can be solved using the underlying <a class=\"wiki\" href=\"https:\/\/tapas.labri.fr\/wp\/?page_id=13\">GENEPI<\/a> plugin (e.g. <a class=\"wiki\" href=\"https:\/\/tapas.labri.fr\/wp\/?page_id=14\">PresTAF<\/a> does not support negative integers).<\/p>\n<p>The purpose of Alambic is to apply several rewriting rules on <a class=\"wiki\" href=\"https:\/\/tapas.labri.fr\/wp\/?page_id=17\">Armoise<\/a> formulas to eliminate syntactic sugar and to make the best effort to check that a given formula is computable using <a class=\"wiki\" href=\"https:\/\/tapas.labri.fr\/wp\/?page_id=13\">GENEPI<\/a>.<\/p>\n<h1>Distiller<\/h1>\n<p>Distiller is a tool that gathers <a class=\"wiki\" href=\"https:\/\/tapas.labri.fr\/wp\/?page_id=13\">GENEPI<\/a>, <a class=\"wiki\" href=\"https:\/\/tapas.labri.fr\/wp\/?page_id=17\">Armoise<\/a> and <a class=\"wiki\" href=\"https:\/\/tapas.labri.fr\/wp\/?page_id=20\">Alambic<\/a> in a command-line solver. Distiller is distributed within the <a class=\"wiki\" href=\"https:\/\/tapas.labri.fr\/wp\/\">TaPAS<\/a> package. Distiller possesses several useful options that can be obtained using the <tt>--help<\/tt>:<\/p>\n<pre class=\"wiki\">  $ distiller --help\r\n  USAGE:distiller [options] [armoise input filenames]\r\n  with options:\r\n  -n, --normal-forms    \tdisplay normalized formulas (default=false).\r\n  -s, --solutions       \tdisplay all solutions (default=false).\r\n  -d, --data-structures \tdisplay the data structure used to encode the set of\r\n  \t\t\tsolutions (default=false).\r\n  -z, --sizes           \tdisplay the size of the internal data structure used to encode the set of\r\n  \t\t\tsolutions (default=false).\r\n  -k, --types           \tdisplay the type of the formulas (default=false).\r\n  -v, --domains         \tdisplay the domains of variables (default=false).\r\n  --debug=&lt;n&gt;           \tset the CCL debug level (default=-1).\r\n  -e, --emptyness       \tcheck the emptyness of computed sets (default=false).\r\n  -q, --quiet           \tdisplay no message when checking for the emptyness of sets (default=false).\r\n  -x, --solver-type     \treturns the minimal solver type required to solve\r\n  \t\t\tpredicates (default=false).\r\n  --one-solution        \treturns one element of the computed set (if not empty) (default=false).\r\n  --plugin=&lt;string&gt;     \tspecify which GENEPI plugin to use (default=prestaf).\r\n  --dump=&lt;string&gt;       \tspecify a file containing a serialized genepi set. (default=(null)).\r\n  -t                    \tdisplay execution times for each genepi operation. (default=false).\r\n  -m, --monoid          \tcomputes the monoid (default=false).\r\n  --solvers             \tdisplay solvers that are currently installed. (default=false).\r\n  -h, --help            \tthis help message.\r\n  \r\n  Available GENEPI plugins are: prestaf-no-among, prestaf, ppl, lash-lsdf, lira, genz, mona, lash-msdf, omega, rva\r\n<\/pre>\n<p>The help message terminates with the list of currently installed <a class=\"wiki\" href=\"https:\/\/tapas.labri.fr\/wp\/?page_id=13\">GENEPI<\/a> plugins.<\/p>\n<h1>Benchmarks<\/h1>\n<p>The table below compares execution times of distiller w.r.t. plugins. Times are given in seconds measured with the <tt>time <\/tt>command of the <tt>bash<\/tt> shell. d<em>istiller<\/em> is queried to check the emptyness of the <a class=\"wiki\" href=\"https:\/\/tapas.labri.fr\/wp\/?page_id=17\">Armoise<\/a> formula in the file <tt>bench-XX<\/tt> (each such file can be found within the <a class=\"wiki\" href=\"https:\/\/tapas.labri.fr\/wp\/?page_id=98\">TaPAS<\/a> tarball).<\/p>\n<p>Each Distiller process was allocated (using <tt>ulimit<\/tt>) a budget of 4.5 GB and 5 minutes of CPU times. ERR` indicates an abnormal termination of <em>distiller<\/em> due to an internal error (e.g. the use of two many variables in <a href=\"https:\/\/tapas.labri.fr\/wp\/?page_id=13#Plugins\">Omega<\/a>) or due to the consumption of its memory or time limit.<\/p>\n<p>The benchmarks was executed on a 64 bits machine equipped with an Intel\u00ae Xeon\u00ae 2.33 GHz CPU and 8 GB of memory.<\/p>\n<p>Not surprisingly, the <a href=\"https:\/\/tapas.labri.fr\/wp\/?page_id=13#Plugins\">Omega plugin<\/a> that represents sets as formulas outperforms all others plugins (based on binary automata representation of sets) to check the emptyness of sets.<\/p>\n<p>Several <tt>ERR<\/tt> occur :<\/p>\n<ul>\n<li>For the <a class=\"wiki\" href=\"https:\/\/tapas.labri.fr\/wp\/?page_id=13#Plugins\">LASH<\/a> based plugins &#8212; <tt>lash-lsdf<\/tt>, <tt>lash-msdf<\/tt> and <tt>rva<\/tt> &#8212; the process ran out of time.<\/li>\n<li>For the <a class=\"wiki\" href=\"https:\/\/tapas.labri.fr\/wp\/?page_id=13#Plugins\">LIRA<\/a> plugin, the process ran out of time for <tt>bench-07<\/tt> or terminated with a <tt>Segmentation Fault<\/tt> due to a stack overflow.<\/li>\n<li>For the <a class=\"wiki\" href=\"https:\/\/tapas.labri.fr\/wp\/?page_id=13#Plugins\">Mona<\/a> plugin, the process terminates because the plugin had been consumed its budget of BDD nodes, for <tt>bench-03<\/tt> and <tt>bench-09<\/tt>, or it exhausted its memory space for <tt>bench-04<\/tt>.<\/li>\n<\/ul>\n<table class=\"wiki\">\n<tbody>\n<tr>\n<th><strong>File<\/strong><\/th>\n<th><strong>lash-lsdf<\/strong><\/th>\n<th><strong>lash-msdf<\/strong><\/th>\n<th><strong>lira<\/strong><\/th>\n<th><strong>mona<\/strong><\/th>\n<th><strong>omega<\/strong><\/th>\n<th><strong>prestaf<\/strong><\/th>\n<th><strong>prestaf-no-among<\/strong><\/th>\n<th><strong>rva<\/strong><\/th>\n<\/tr>\n<tr>\n<td><a class=\"missing source\">bench-01<\/a><\/td>\n<td>0.09<\/td>\n<td>0.08<\/td>\n<td>0.03<\/td>\n<td>0.01<\/td>\n<td>0.00<\/td>\n<td>0.20<\/td>\n<td>0.21<\/td>\n<td>0.68<\/td>\n<\/tr>\n<tr>\n<td><a class=\"missing source\">bench-02<\/a><\/td>\n<td>1.72<\/td>\n<td>0.27<\/td>\n<td>0.53<\/td>\n<td>0.26<\/td>\n<td>0.00<\/td>\n<td>1.02<\/td>\n<td>1.00<\/td>\n<td>1.33<\/td>\n<\/tr>\n<tr>\n<td><a class=\"missing source\">bench-03<\/a><\/td>\n<td>0.84<\/td>\n<td>20.15<\/td>\n<td>0.46<\/td>\n<td>ERR<\/td>\n<td>0.00<\/td>\n<td>0.23<\/td>\n<td>0.23<\/td>\n<td>243.13<\/td>\n<\/tr>\n<tr>\n<td><a class=\"missing source\">bench-04<\/a><\/td>\n<td>2.94<\/td>\n<td>ERR<\/td>\n<td>ERR<\/td>\n<td>ERR<\/td>\n<td>0.00<\/td>\n<td>0.37<\/td>\n<td>0.39<\/td>\n<td>ERR<\/td>\n<\/tr>\n<tr>\n<td><a class=\"missing source\">bench-05<\/a><\/td>\n<td>3.41<\/td>\n<td>4.61<\/td>\n<td>0.15<\/td>\n<td>10.70<\/td>\n<td>0.00<\/td>\n<td>1.15<\/td>\n<td>1.18<\/td>\n<td>19.24<\/td>\n<\/tr>\n<tr>\n<td><a class=\"missing source\">bench-06<\/a><\/td>\n<td>ERR<\/td>\n<td>164.81<\/td>\n<td>ERR<\/td>\n<td>0.77<\/td>\n<td>0.00<\/td>\n<td>1.57<\/td>\n<td>1.56<\/td>\n<td>ERR<\/td>\n<\/tr>\n<tr>\n<td><a class=\"missing source\">bench-07<\/a><\/td>\n<td>23.92<\/td>\n<td>33.20<\/td>\n<td>ERR<\/td>\n<td>0.35<\/td>\n<td>0.02<\/td>\n<td>0.23<\/td>\n<td>0.25<\/td>\n<td>ERR<\/td>\n<\/tr>\n<tr>\n<td><a class=\"missing source\">bench-08<\/a><\/td>\n<td>1.17<\/td>\n<td>ERR<\/td>\n<td>ERR<\/td>\n<td>18.15<\/td>\n<td>0.00<\/td>\n<td>0.99<\/td>\n<td>0.99<\/td>\n<td>ERR<\/td>\n<\/tr>\n<tr>\n<td><a class=\"missing source\">bench-09<\/a><\/td>\n<td>10.33<\/td>\n<td>ERR<\/td>\n<td>ERR<\/td>\n<td>ERR<\/td>\n<td>0.00<\/td>\n<td>0.42<\/td>\n<td>0.38<\/td>\n<td>ERR<\/td>\n<\/tr>\n<tr>\n<td><a class=\"missing source\">bench-10<\/a><\/td>\n<td>0.00<\/td>\n<td>0.00<\/td>\n<td>0.00<\/td>\n<td>0.00<\/td>\n<td>0.00<\/td>\n<td>0.18<\/td>\n<td>0.20<\/td>\n<td>0.01<\/td>\n<\/tr>\n<tr>\n<td><a class=\"missing source\">bench-11<\/a><\/td>\n<td>0.00<\/td>\n<td>0.00<\/td>\n<td>0.00<\/td>\n<td>0.00<\/td>\n<td>0.00<\/td>\n<td>0.20<\/td>\n<td>0.18<\/td>\n<td>0.00<\/td>\n<\/tr>\n<tr>\n<td><a class=\"missing source\">bench-12<\/a><\/td>\n<td>0.00<\/td>\n<td>0.00<\/td>\n<td>0.00<\/td>\n<td>0.00<\/td>\n<td>0.00<\/td>\n<td>0.19<\/td>\n<td>0.20<\/td>\n<td>0.00<\/td>\n<\/tr>\n<tr>\n<td><a class=\"missing source\">bench-13<\/a><\/td>\n<td>0.01<\/td>\n<td>0.01<\/td>\n<td>0.01<\/td>\n<td>0.00<\/td>\n<td>0.00<\/td>\n<td>0.19<\/td>\n<td>0.19<\/td>\n<td>0.03<\/td>\n<\/tr>\n<tr>\n<td><a class=\"missing source\">bench-14<\/a><\/td>\n<td>0.01<\/td>\n<td>0.01<\/td>\n<td>0.02<\/td>\n<td>0.01<\/td>\n<td>0.00<\/td>\n<td>0.19<\/td>\n<td>0.18<\/td>\n<td>0.04<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n","protected":false},"excerpt":{"rendered":"<p>Alambic The Alambic library is used to compile Armoise formulas into calls to GENEPI functions. The Armoise language allows to specify sets that are not definable into the Presburger arithmetics (e.g. nat*nat). Furthermore, even if an Armoise formula defines a &hellip; <a href=\"https:\/\/tapas.labri.fr\/wp\/?page_id=20\">Continue reading <span class=\"meta-nav\">&rarr;<\/span><\/a><\/p>\n","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-20","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/tapas.labri.fr\/wp\/index.php?rest_route=\/wp\/v2\/pages\/20","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/tapas.labri.fr\/wp\/index.php?rest_route=\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/tapas.labri.fr\/wp\/index.php?rest_route=\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/tapas.labri.fr\/wp\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/tapas.labri.fr\/wp\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=20"}],"version-history":[{"count":5,"href":"https:\/\/tapas.labri.fr\/wp\/index.php?rest_route=\/wp\/v2\/pages\/20\/revisions"}],"predecessor-version":[{"id":117,"href":"https:\/\/tapas.labri.fr\/wp\/index.php?rest_route=\/wp\/v2\/pages\/20\/revisions\/117"}],"wp:attachment":[{"href":"https:\/\/tapas.labri.fr\/wp\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=20"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}