with Standard_Integer_Vectors; use Standard_Integer_Vectors; with Standard_Integer_VecVecs; use Standard_Integer_VecVecs; with Lists_of_Integer_Vectors; use Lists_of_Integer_Vectors; with Arrays_of_Integer_Vector_Lists; use Arrays_of_Integer_Vector_Lists; with Standard_Complex_Polynomials; use Standard_Complex_Polynomials; with Standard_Complex_Poly_Functions; use Standard_Complex_Poly_Functions; with Standard_Complex_Poly_Systems; use Standard_Complex_Poly_Systems; with Standard_Complex_Poly_SysFun; use Standard_Complex_Poly_SysFun; package Integer_Lifting_Functions is -- DESCRIPTION : -- This package offers three different types of integer-valued -- lifting functions: linear, polynomial, and point-wise. -- LINEAR LIFTING : function Linear_Lift ( lf,v : Vector ) return Vector; function Linear_Lift ( lf : Vector; l : List ) return List; function Linear_Lift ( lf : VecVec; l : Array_of_Lists ) return Array_of_Lists; -- DESCRIPTION : -- The last entry of the enlarged vector on return equals , -- for every vector v in the lists. -- REQUIRED : lf'range = v'range. -- POLYNOMIAL LIFTING : function Polynomial_Lift ( lf : Poly; v : Vector ) return Vector; function Polynomial_Lift ( lf : Eval_Poly; v : Vector ) return Vector; function Polynomial_Lift ( lf : Poly; l : List ) return List; function Polynomial_Lift ( lf : Eval_Poly; l : List ) return List; function Polynomial_Lift ( lf : Poly_Sys; l : Array_of_Lists ) return Array_of_Lists; function Polynomial_Lift ( lf : Eval_Poly_Sys; l : Array_of_Lists ) return Array_of_Lists; -- DESCRIPTION : -- As lf is complex valued, the rounded real part is used as lifting. -- RANDOM LIFTING : function Random_Lift ( lflow,lfupp : integer; v : Vector ) return Vector; function Random_Lift ( lflow,lfupp : integer; l : List ) return List; function Random_Lift ( lflow,lfupp : Vector; l : Array_of_Lists ) return Array_of_Lists; -- DESCRIPTION : -- The lifting values are random integers between lflow and lfupp. -- RANDOM LINEAR LIFTING : function Random_Linear_Lift ( lflow,lfupp : integer; v : Vector ) return Vector; function Random_Linear_Lift ( lflow,lfupp : integer; l : List ) return List; function Random_Linear_Lift ( lflow,lfupp : Vector; l : Array_of_Lists ) return Array_of_Lists; -- DESCRIPTION : -- Linear lifting with random vectors of integers between lflow and lfupp. -- POINT-WISE LIFTING : function Point_Lift ( lf : integer; v : Vector ) return Vector; function Point_Lift ( lf : Vector; l : List ) return List; function Point_Lift ( lf : VecVec; l : Array_of_Lists ) return Array_of_Lists; -- DESCRIPTION : -- The enlarged vector on return has as last component the lifting lf(k), -- where k is the position of the vector v in the lists. -- REQUIRED : Length_Of(l) = lf'length. end Integer_Lifting_Functions;