parker/README

   1 The files contained here implement the method for counting solutions to
   2 Presburger formulas described by Parker & Chatterjee in "An
   3 Automata-Theoretic Algorithm for Counting Solutions to Presburger Formulas"
   4 (Compiler Construction 2004).
   5
   6 The method has essentially two phases.  It first takes a Presburger formula
   7 and represents it as a deterministic finite automaton (DFA), and then
   8 counts the number of accepting paths in the DFA to reveal the number of
   9 solutions to the original formula.
  10
  11 This implementation uses two pre-existing tools.
  12   1.  It uses the automata-construction algorithms of Bartzis & Bultan to
  13       construct DFA representations of linear equality and inequality
  14       constraints.  The code for DFA construction is graciously provided by
  15       Constantinos Bartzis in the file construction.c.  Please contact him
  16       (bar@cs.uscb.edu) with any questions or comments regarding this code.
  17   2.  It also uses the DFA Library of the MONA tool.  Please see
  18       http://www.brics.dk/mona to download MONA.
  19
  20
  21 Description of files:
  22   generate_code.pl -- A Perl script that takes a Presburger formula as input
  23                       and generates the C source code for building a DFA
  24                       representation of the formula and subsequently
  25                       counting the number of accepting paths in the DFA to
  26                       reveal the number of solutions to the original formula.
  27   count_solutions.h -- A header file containing declarations of the
  28                        following functions called by the generated code:
  29                        build_DFA_eq(), build_DFA_ineq(), count_accepting_paths().
  30   construction.c -- Contains function definitions for build_DFA_eq() and
  31                     build_DFA_ineq() (code provided by Bartzis).
  32   count_paths.c -- Contains function definition for count_accepting_paths().
  33
  34
  35 Example 1:
  36   The file example1.formula contains the representation of an example
  37   Presburger formula with 4 free variables.  To count the number of
  38   solutions to the formula, execute the following commands.
  39
  40             generate_code.pl 4 < example1.formula > example1.c
  41             make in=example1
  42             count
  43
  44   The output should be
  45             DFA: 12 states, 17 accepting paths, length of all accepting paths is 4.
  46
  47
  48 Example 2:
  49   The file example2.formula contains the representation of an example
  50   Presburger formula with 2 free variables.  To count the number of
  51   solutions to the formula, execute the following commands.
  52
  53             generate_code.pl 2 < example2.formula > example2.c
  54             make in=example2
  55             count
  56
  57   The output should be
  58             DFA: 76 states, 16000 accepting paths, length of all accepting paths is 9.
  59
  60
  61 Direct any questions or comments to Erin Parker (parker@cs.unc.edu).
  62
  63 PLEASE NOTE:  The input formula is assumed to be written in the style of
  64 the Omega Library (see http://www.cs.umd.edu/projects/omega for more on
  65 the Omega Library).  The code contained here is certainly not guaranteed
  66 to be bug-free.  It really is designed to process the sort of representations
  67 I typically see when using the Omega Library for the expression and
  68 manipulation of Presburger formulas of interest to me.  ---Erin
  69
  70