Return to integer_lifting_functions.ads CVS log

Up to [local] / OpenXM_contrib / PHC / Ada / Root_Counts / Stalift

Annotation of OpenXM_contrib/PHC/Ada/Root_Counts/Stalift/integer_lifting_functions.ads, Revision 1.1.1.1

1.1       maekawa     1: with Standard_Integer_Vectors;           use Standard_Integer_Vectors;
                      2: with Standard_Integer_VecVecs;           use Standard_Integer_VecVecs;
                      3: with Lists_of_Integer_Vectors;           use Lists_of_Integer_Vectors;
                      4: with Arrays_of_Integer_Vector_Lists;     use Arrays_of_Integer_Vector_Lists;
                      5: with Standard_Complex_Polynomials;       use Standard_Complex_Polynomials;
                      6: with Standard_Complex_Poly_Functions;    use Standard_Complex_Poly_Functions;
                      7: with Standard_Complex_Poly_Systems;      use Standard_Complex_Poly_Systems;
                      8: with Standard_Complex_Poly_SysFun;       use Standard_Complex_Poly_SysFun;
                      9:
                     10: package Integer_Lifting_Functions is
                     11:
                     12: -- DESCRIPTION :
                     13: --   This package offers three different types of integer-valued
                     14: --   lifting functions: linear, polynomial, and point-wise.
                     15:
                     16: -- LINEAR LIFTING :
                     17:
                     18:   function Linear_Lift ( lf,v : Vector ) return Vector;
                     19:   function Linear_Lift ( lf : Vector; l : List ) return List;
                     20:   function Linear_Lift ( lf : VecVec;
                     21:                          l : Array_of_Lists ) return Array_of_Lists;
                     22:
                     23:   -- DESCRIPTION :
                     24:   --   The last entry of the enlarged vector on return equals <lf,v>,
                     25:   --   for every vector v in the lists.
                     26:
                     27:   -- REQUIRED : lf'range = v'range.
                     28:
                     29: -- POLYNOMIAL LIFTING :
                     30:
                     31:   function Polynomial_Lift ( lf : Poly; v : Vector ) return Vector;
                     32:   function Polynomial_Lift ( lf : Eval_Poly; v : Vector ) return Vector;
                     33:   function Polynomial_Lift ( lf : Poly; l : List ) return List;
                     34:   function Polynomial_Lift ( lf : Eval_Poly; l : List ) return List;
                     35:   function Polynomial_Lift ( lf : Poly_Sys; l : Array_of_Lists )
                     36:                            return Array_of_Lists;
                     37:   function Polynomial_Lift ( lf : Eval_Poly_Sys; l : Array_of_Lists )
                     38:                            return Array_of_Lists;
                     39:
                     40:   -- DESCRIPTION :
                     41:   --   As lf is complex valued, the rounded real part is used as lifting.
                     42:
                     43: -- RANDOM LIFTING :
                     44:
                     45:   function Random_Lift ( lflow,lfupp : integer; v : Vector ) return Vector;
                     46:   function Random_Lift ( lflow,lfupp : integer; l : List ) return List;
                     47:   function Random_Lift ( lflow,lfupp : Vector; l : Array_of_Lists )
                     48:                        return Array_of_Lists;
                     49:
                     50:   -- DESCRIPTION :
                     51:   --   The lifting values are random integers between lflow and lfupp.
                     52:
                     53: -- RANDOM LINEAR LIFTING :
                     54:
                     55:   function Random_Linear_Lift ( lflow,lfupp : integer; v : Vector )
                     56:                               return Vector;
                     57:   function Random_Linear_Lift ( lflow,lfupp : integer; l : List ) return List;
                     58:   function Random_Linear_Lift ( lflow,lfupp : Vector; l : Array_of_Lists )
                     59:                               return Array_of_Lists;
                     60:
                     61:   -- DESCRIPTION :
                     62:   --   Linear lifting with random vectors of integers between lflow and lfupp.
                     63:
                     64: -- POINT-WISE LIFTING :
                     65:
                     66:   function Point_Lift ( lf : integer; v : Vector ) return Vector;
                     67:   function Point_Lift ( lf : Vector; l : List ) return List;
                     68:   function Point_Lift ( lf : VecVec;
                     69:                         l : Array_of_Lists ) return Array_of_Lists;
                     70:
                     71:   -- DESCRIPTION :
                     72:   --   The enlarged vector on return has as last component the lifting lf(k),
                     73:   --   where k is the position of the vector v in the lists.
                     74:
                     75:   -- REQUIRED : Length_Of(l) = lf'length.
                     76:
                     77: end Integer_Lifting_Functions;