isl_pw_qpolynomial_sum: handle existentials in wrapped domains
[barvinok.git] / parker / README
blob73d790c607f3f3db0d6cfbe064976e00161be80f
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).
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.
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.
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().
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.
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.
61 Direct any questions or comments to Erin Parker (parker@cs.unc.edu).
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