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