1--  PSL - Small QM reduction
2--  Copyright (C) 2002-2016 Tristan Gingold
3--
4--  This program is free software: you can redistribute it and/or modify
5--  it under the terms of the GNU General Public License as published by
6--  the Free Software Foundation, either version 2 of the License, or
7--  (at your option) any later version.
8--
9--  This program is distributed in the hope that it will be useful,
10--  but WITHOUT ANY WARRANTY; without even the implied warranty of
11--  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
12--  GNU General Public License for more details.
13--
14--  You should have received a copy of the GNU General Public License
15--  along with this program.  If not, see <gnu.org/licenses>.
16
17with PSL.Nodes; use PSL.Nodes;
18with Interfaces; use Interfaces;
19
20package PSL.QM is
21   type Primes_Set (<>) is private;
22
23   function Build_Primes (N : Node) return Primes_Set;
24
25   function Build_Node (Ps : Primes_Set) return Node;
26
27   function Reduce (N : Node) return Node;
28
29   --  The maximum number of terms that this package can handle.
30   --  The algorithm is in O(2**n)
31   Max_Terms : constant Natural := 12;
32
33   type Term_Assoc_Type is array (1 .. Max_Terms) of Node;
34   Term_Assoc : Term_Assoc_Type := (others => Null_Node);
35   Nbr_Terms : Natural := 0;
36
37   procedure Reset;
38
39   procedure Disp_Primes_Set (Ps : Primes_Set);
40private
41   --  Scalar type used to represent a vector of booleans for terms.
42   subtype Vector_Type is Unsigned_16;
43   pragma Assert (Vector_Type'Modulus >= 2 ** Max_Terms);
44
45   --  States of a vector of term.
46   --  If SET is 0, this is a don't care: the term has no influence.
47   --  If SET is 1, the value of the term is in VAL.
48   type Prime_Type is record
49      Val : Unsigned_16;
50      Set : Unsigned_16;
51   end record;
52
53   subtype Len_Type is Natural range 0 .. 2 ** Max_Terms;
54
55   type Set_Type is array (Natural range <>) of Prime_Type;
56
57   --  A set of primes is a collection of at most MAX prime.
58   type Primes_Set (Max : Len_Type) is record
59      Nbr : Len_Type := 0;
60      Set : Set_Type (1 .. Max);
61   end record;
62end PSL.QM;
63