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 Presburger arithmetics it can be solved using the underlying GENEPI plugin (e.g. PresTAF does not support negative integers).

The purpose of Alambic is to apply several rewriting rules on Armoise formulas to eliminate syntactic sugar and to make the best effort to check that a given formula is computable using GENEPI.

Distiller

Distiller is a tool that gathers GENEPI, Armoise and Alambic in a command-line solver. Distiller is distributed within the TaPAS package. Distiller possesses several useful options that can be obtained using the --help:

  $ distiller --help
  USAGE:distiller [options] [armoise input filenames]
  with options:
  -n, --normal-forms    	display normalized formulas (default=false).
  -s, --solutions       	display all solutions (default=false).
  -d, --data-structures 	display the data structure used to encode the set of
  			solutions (default=false).
  -z, --sizes           	display the size of the internal data structure used to encode the set of
  			solutions (default=false).
  -k, --types           	display the type of the formulas (default=false).
  -v, --domains         	display the domains of variables (default=false).
  --debug=<n>           	set the CCL debug level (default=-1).
  -e, --emptyness       	check the emptyness of computed sets (default=false).
  -q, --quiet           	display no message when checking for the emptyness of sets (default=false).
  -x, --solver-type     	returns the minimal solver type required to solve
  			predicates (default=false).
  --one-solution        	returns one element of the computed set (if not empty) (default=false).
  --plugin=<string>     	specify which GENEPI plugin to use (default=prestaf).
  --dump=<string>       	specify a file containing a serialized genepi set. (default=(null)).
  -t                    	display execution times for each genepi operation. (default=false).
  -m, --monoid          	computes the monoid (default=false).
  --solvers             	display solvers that are currently installed. (default=false).
  -h, --help            	this help message.
  
  Available GENEPI plugins are: prestaf-no-among, prestaf, ppl, lash-lsdf, lira, genz, mona, lash-msdf, omega, rva

The help message terminates with the list of currently installed GENEPI plugins.

Benchmarks

The table below compares execution times of distiller w.r.t. plugins. Times are given in seconds measured with the time command of the bash shell. distiller is queried to check the emptyness of the Armoise formula in the file bench-XX (each such file can be found within the TaPAS tarball).

Each Distiller process was allocated (using ulimit) a budget of 4.5 GB and 5 minutes of CPU times. ERR` indicates an abnormal termination of distiller due to an internal error (e.g. the use of two many variables in Omega) or due to the consumption of its memory or time limit.

The benchmarks was executed on a 64 bits machine equipped with an Intel® Xeon® 2.33 GHz CPU and 8 GB of memory.

Not surprisingly, the Omega plugin that represents sets as formulas outperforms all others plugins (based on binary automata representation of sets) to check the emptyness of sets.

Several ERR occur :

• For the LASH based plugins — lash-lsdf, lash-msdf and rva — the process ran out of time.
• For the LIRA plugin, the process ran out of time for bench-07 or terminated with a Segmentation Fault due to a stack overflow.
• For the Mona plugin, the process terminates because the plugin had been consumed its budget of BDD nodes, for bench-03 and bench-09, or it exhausted its memory space for bench-04.