File: [local] / OpenXM_contrib / PHC / Ada / Root_Counts / Stalift / drivers_for_lifting_functions.adb (download)
Revision 1.1.1.1 (vendor branch), Sun Oct 29 17:45:29 2000 UTC (23 years, 9 months ago) by maekawa
Branch: PHC, MAIN
CVS Tags: v2, maekawa-ipv6, RELEASE_1_2_3, RELEASE_1_2_2_KNOPPIX_b, RELEASE_1_2_2_KNOPPIX, RELEASE_1_2_2, RELEASE_1_2_1, HEAD Changes since 1.1: +0 -0
lines
Import the second public release of PHCpack.
OKed by Jan Verschelde.
|
with integer_io; use integer_io;
with Communications_with_User; use Communications_with_User;
with Standard_Floating_Numbers_io; use Standard_Floating_Numbers_io;
with Numbers_io; use Numbers_io;
with Standard_Random_Numbers; use Standard_Random_Numbers;
with Standard_Integer_Vectors;
with Standard_Integer_Vectors_io; use Standard_Integer_Vectors_io;
with Standard_Floating_Vectors;
with Standard_Floating_Vectors_io; use Standard_Floating_Vectors_io;
with Standard_Complex_Poly_Systems_io; use Standard_Complex_Poly_Systems_io;
with Arrays_of_Integer_Vector_Lists_io; use Arrays_of_Integer_Vector_Lists_io;
with Integer_Lifting_Functions; use Integer_Lifting_Functions;
with Integer_Lifting_Utilities; use Integer_Lifting_Utilities;
with Floating_Lifting_Functions; use Floating_Lifting_Functions;
with Floating_Lifting_Utilities; use Floating_Lifting_Utilities;
with Floating_Integer_Convertors; use Floating_Integer_Convertors;
with Floating_Mixed_Subdivisions_io;
package body Drivers_for_Lifting_Functions is
-- AUXILIARIES :
procedure put ( file : in file_type;
v : in Standard_Floating_Vectors.Vector;
fore,aft,exp : in natural ) is
begin
for i in v'range loop
put(file,v(i),fore,aft,exp);
end loop;
end put;
procedure put ( v : in Standard_Floating_Vectors.Vector;
fore,aft,exp : in natural ) is
begin
put(Standard_Output,v,fore,aft,exp);
end put;
procedure Read_Integer_Vector
( v : in out Standard_Integer_Vectors.Vector ) is
begin
for i in v'range loop
put("Give integer for component "); put(i,1); put(" : ");
Read_Integer(v(i));
end loop;
end Read_Integer_Vector;
procedure Read_Float_Vector
( v : in out Standard_Floating_Vectors.Vector ) is
begin
for i in v'range loop
put("Give float for component "); put(i,1); put(" : ");
Read_Double_Float(v(i));
end loop;
end Read_Float_Vector;
procedure Set_Integer_Bounds
( file : in file_type;
low,upp : in out Standard_Integer_Vectors.Vector ) is
-- DESCRIPTION :
-- Shows the default values for lower and upper bounds and allows
-- the user to modify these.
ans : character;
m : constant natural := low'length;
begin
loop
new_line;
put_line("Current lower and upper bounds on lifting values");
put(" lower : "); put(low); new_line;
put(" upper : "); put(upp); new_line;
put("Do you want to change these values ? (y/n) ");
Ask_Yes_or_No(ans);
exit when ans /= 'y';
put("Reading "); put(m,1); put(" lower bounds ");
put_line("for the lifting."); Read_Integer_Vector(low);
put("Reading "); put(m,1); put(" upper bounds ");
put_line("for the lifting."); Read_Integer_Vector(upp);
end loop;
put(file," Lower bounds : "); put(file,low); new_line(file);
put(file," Upper bounds : "); put(file,upp); new_line(file);
end Set_Integer_Bounds;
procedure Set_Float_Bounds
( file : in file_type;
low,upp : in out Standard_Floating_Vectors.Vector ) is
-- DESCRIPTION :
-- Shows the default values for lower and upper bounds and allows
-- the user to modify these.
ans : character;
m : constant natural := low'length;
begin
loop
new_line;
put_line("Current lower and upper bounds on lifting values");
put(" lower : "); put(low,2,3,3); new_line;
put(" upper : "); put(upp,2,3,3); new_line;
put("Do you want to change these values ? (y/n) ");
Ask_Yes_or_No(ans);
exit when ans /= 'y';
put("Reading "); put(m,1); put(" lower bounds ");
put_line("for the lifting."); Read_Float_Vector(low);
put("Reading "); put(m,1); put(" upper bounds ");
put_line("for the lifting."); Read_Float_Vector(upp);
end loop;
put(file," Lower bounds : "); put(file,low,2,3,3); new_line(file);
put(file," Upper bounds : "); put(file,upp,2,3,3); new_line(file);
end Set_Float_Bounds;
function Read_Integer_Lifting
( l : Lists_of_Integer_Vectors.List )
return Lists_of_Integer_Vectors.List is
use Lists_of_Integer_Vectors;
use Standard_Integer_Vectors;
tmp : List := l;
res,res_last : List;
begin
put_line("Give a lifting value for the following points :");
while not Is_Null(tmp) loop
declare
v : constant Vector := Head_Of(tmp).all;
lv : Vector(v'first..v'last+1);
begin
lv(v'range) := v;
put(v); put(" : "); Read_Integer(lv(lv'last));
Append(res,res_last,lv);
end;
tmp := Tail_Of(tmp);
end loop;
return res;
end Read_Integer_Lifting;
function Read_Float_Lifting
( l : Lists_of_Floating_Vectors.List )
return Lists_of_Floating_Vectors.List is
use Lists_of_Floating_Vectors;
use Standard_Floating_Vectors;
tmp : List := l;
res,res_last : List;
begin
put_line("Give a lifting value for the following points :");
while not Is_Null(tmp) loop
declare
v : constant Vector := Head_Of(tmp).all;
lv : Vector(v'first..v'last+1);
begin
lv(v'range) := v;
put(v,0,0,0); put(" : "); Read_Double_Float(lv(lv'last));
Append(res,res_last,lv);
end;
tmp := Tail_Of(tmp);
end loop;
return res;
end Read_Float_Lifting;
procedure Integer_Random_Linear_Lifting
( file : in file_type; n : in natural;
points : in Arrays_of_Integer_Vector_Lists.Array_of_Lists;
lifted : in out Arrays_of_Integer_Vector_Lists.Array_of_Lists;
lilifu : in out Standard_Integer_VecVecs.Link_to_VecVec ) is
low : Standard_Integer_Vectors.Vector(points'range) := (points'range => 0);
upp : Standard_Integer_Vectors.Vector(points'range)
:= Adaptive_Lifting(points);
ranvec : Standard_Integer_Vectors.Vector(1..n);
begin
Set_Integer_Bounds(file,low,upp);
lilifu := new Standard_Integer_VecVecs.VecVec(points'range);
for i in lilifu'range loop
for j in ranvec'range loop
ranvec(j) := Random(low(i),upp(i));
end loop;
lilifu(i) := new Standard_Integer_Vectors.Vector'(ranvec);
end loop;
lifted := Linear_Lift(lilifu.all,points);
end Integer_Random_Linear_Lifting;
procedure Float_Random_Linear_Lifting
( file : in file_type; n : in natural;
points : in Arrays_of_Floating_Vector_Lists.Array_of_Lists;
lifted : in out Arrays_of_Floating_Vector_Lists.Array_of_Lists;
lilifu : in out Standard_Floating_VecVecs.Link_to_VecVec ) is
m : constant natural := points'last;
low : Standard_Floating_Vectors.Vector(points'range)
:= (points'range => 0.0);
upp : Standard_Floating_Vectors.Vector(points'range)
:= Adaptive_Lifting(points);
ranvec : Standard_Floating_Vectors.Vector(1..n);
begin
Set_Float_Bounds(file,low,upp);
lilifu := new Standard_Floating_VecVecs.VecVec(points'range);
for i in lilifu'range loop
ranvec := Random(m,low(i),upp(i));
lifted(i) := Linear_Lift(points(i),ranvec);
lilifu(i) := new Standard_Floating_Vectors.Vector'(ranvec);
end loop;
end Float_Random_Linear_Lifting;
procedure Integer_User_Linear_Lifting
( file : in file_type; n : in natural;
points : in Arrays_of_Integer_Vector_Lists.Array_of_Lists;
lifted : in out Arrays_of_Integer_Vector_Lists.Array_of_Lists;
lilifu : in out Standard_Integer_VecVecs.Link_to_VecVec ) is
lift : Standard_Integer_VecVecs.VecVec(points'range);
begin
for k in lift'range loop
put("Give "); put(n,1); put(" integers for ");
put("vector "); put(k,1); put(" : "); get(n,lift(k));
put(file," vector "); put(file,k,1);
put(file," : "); put(file,lift(k)); new_line(file);
end loop;
lifted := Linear_Lift(lift,points);
lilifu := new Standard_Integer_VecVecs.VecVec'(lift);
end Integer_User_Linear_Lifting;
procedure Float_User_Linear_Lifting
( file : in file_type; n : in natural;
points : in Arrays_of_Floating_Vector_Lists.Array_of_Lists;
lifted : in out Arrays_of_Floating_Vector_Lists.Array_of_Lists;
lilifu : in out Standard_Floating_VecVecs.Link_to_VecVec ) is
lift : Standard_Floating_VecVecs.VecVec(points'range);
begin
for k in lift'range loop
put("Give "); put(n,1); put(" floats for ");
put("vector "); put(k,1); put(" : "); get(n,lift(k));
put(file," vector "); put(file,k,1);
put(file," : "); put(file,lift(k)); new_line(file);
lifted(k) := Linear_Lift(points(k),lift(k).all);
end loop;
lilifu := new Standard_Floating_VecVecs.VecVec'(lift);
end Float_User_Linear_Lifting;
procedure Integer_Polynomial_Lifting
( file : in file_type;
points : in Arrays_of_Integer_Vector_Lists.Array_of_Lists;
lifted : in out Arrays_of_Integer_Vector_Lists.Array_of_Lists ) is
lift : Link_to_Poly_Sys;
begin
get(lift);
put(file,lift.all);
lifted := Polynomial_Lift(lift.all,points);
end Integer_Polynomial_Lifting;
procedure Float_Polynomial_Lifting
( file : in file_type;
points : in Arrays_of_Floating_Vector_Lists.Array_of_Lists;
lifted : in out Arrays_of_Floating_Vector_Lists.Array_of_Lists ) is
lift : Link_to_Poly_Sys;
begin
get(lift);
put(file,lift.all);
lifted := Polynomial_Lift(lift.all,points);
end Float_Polynomial_Lifting;
procedure Integer_User_Point_Wise_Lifting
( file : in file_type;
points : in Arrays_of_Integer_Vector_Lists.Array_of_Lists;
lifted : in out Arrays_of_Integer_Vector_Lists.Array_of_Lists ) is
begin
for k in points'range loop
lifted(k) := Read_Integer_Lifting(points(k));
end loop;
end Integer_User_Point_Wise_Lifting;
procedure Float_User_Point_Wise_Lifting
( file : in file_type;
points : in Arrays_of_Floating_Vector_Lists.Array_of_Lists;
lifted : in out Arrays_of_Floating_Vector_Lists.Array_of_Lists ) is
begin
for k in points'range loop
lifted(k) := Read_Float_Lifting(points(k));
end loop;
end Float_User_Point_Wise_Lifting;
procedure Integer_Random_Point_Wise_Lifting
( file : in file_type;
points : in Arrays_of_Integer_Vector_Lists.Array_of_Lists;
lifted : in out Arrays_of_Integer_Vector_Lists.Array_of_Lists ) is
low : Standard_Integer_Vectors.Vector(points'range) := (points'range => 0);
upp : Standard_Integer_Vectors.Vector(points'range)
:= Adaptive_Lifting(points);
begin
Set_Integer_Bounds(file,low,upp);
lifted := Random_Lift(low,upp,points);
end Integer_Random_Point_Wise_Lifting;
procedure Float_Random_Point_Wise_Lifting
( file : in file_type;
points : in Arrays_of_Floating_Vector_Lists.Array_of_Lists;
lifted : in out Arrays_of_Floating_Vector_Lists.Array_of_Lists ) is
low : Standard_Floating_Vectors.Vector(points'range)
:= (points'range => 0.0);
upp : Standard_Floating_Vectors.Vector(points'range)
:= Adaptive_Lifting(points);
begin
Set_Float_Bounds(file,low,upp);
lifted := Random_Lift(points,low,upp);
end Float_Random_Point_Wise_Lifting;
function Menu_for_Lifting_Functions return character is
-- DESCRIPTION :
-- Displays the menu and returns the selected lifting function.
ans : character;
begin
put_line("MENU for Lifting Functions :");
put_line(" Linear : 1. Random linear vectors will be chosen.");
put_line(" : 2. You can choose the vectors yourself.");
put_line(" Polynomial : 3. The system to be solved will be used.");
put_line(" : 4. You can choose the polynomials yourself.");
put_line(" Point-wise : 5. For each point a random lifting value.");
put_line(" : 6. You can choose all lifting values yourself.");
put("Type a number between 1 and 6 to select lifting : ");
Ask_Alternative(ans,"123456"); return ans;
end Menu_for_Lifting_Functions;
procedure Dispatch_Integer_Lifting
( file : in file_type; p : in Poly_Sys; choice : in character;
points : in Arrays_of_Integer_Vector_Lists.Array_of_Lists;
lifted : in out Arrays_of_Integer_Vector_Lists.Array_of_Lists;
lilifu : in out Standard_Integer_VecVecs.Link_to_VecVec ) is
-- DESCRIPTION :
-- Calls the appropriate lifting function to perform the lifting.
n : constant natural := p'length;
begin
new_line(file); put(file,"INTEGER LIFTING FUNCTION : ");
case choice is
when '1' => put_line(file,"random linear.");
Integer_Random_Linear_Lifting(file,n,points,lifted,lilifu);
when '2' => put_line(file,"linear provided by user.");
Integer_User_Linear_Lifting(file,n,points,lifted,lilifu);
when '3' => put_line(file,"polynomial system.");
lifted := Polynomial_Lift(p,points);
when '4' => put_line(file,"polynomials provided by user.");
Integer_Polynomial_Lifting(file,points,lifted);
when '5' => put_line(file,"random point-wise.");
Integer_Random_Point_Wise_Lifting(file,points,lifted);
when '6' => put_line(file,"point-wise provided by user.");
Integer_User_Point_Wise_Lifting(file,points,lifted);
when others => null;
end case;
new_line(file); put_line(file,"THE LIFTED SUPPORTS :"); new_line(file);
put(file,lifted);
end Dispatch_Integer_Lifting;
procedure Dispatch_Float_Lifting
( file : in file_type; p : in Poly_Sys; choice : in character;
points : in Arrays_of_Floating_Vector_Lists.Array_of_Lists;
lifted : in out Arrays_of_Floating_Vector_Lists.Array_of_Lists;
lilifu : in out Standard_Floating_VecVecs.Link_to_VecVec ) is
-- DESCRIPTION :
-- Calls the appropriate lifting function to perform the lifting.
n : constant natural := p'length;
begin
new_line(file); put(file,"FLOATING-POINT LIFTING FUNCTION : ");
case choice is
when '1' => put_line(file,"random linear.");
Float_Random_Linear_Lifting(file,n,points,lifted,lilifu);
when '2' => put_line(file,"linear provided by user.");
Float_User_Linear_Lifting(file,n,points,lifted,lilifu);
when '3' => put_line(file,"polynomial system.");
lifted := Polynomial_Lift(p,points);
when '4' => put_line(file,"polynomials provided by user.");
Float_Polynomial_Lifting(file,points,lifted);
when '5' => put_line(file,"random point-wise.");
Float_Random_Point_Wise_Lifting(file,points,lifted);
when '6' => put_line(file,"point-wise provided by user.");
Float_User_Point_Wise_Lifting(file,points,lifted);
when others => null;
end case;
new_line(file); put_line(file,"THE LIFTED SUPPORTS :"); new_line(file);
Floating_Mixed_Subdivisions_io.put(file,lifted);
end Dispatch_Float_Lifting;
-- TARGET ROUTINES :
procedure Driver_for_Lifting_Functions
( file : in file_type; p : in Poly_Sys;
points : in Arrays_of_Integer_Vector_Lists.Array_of_Lists;
lifted : in out Arrays_of_Integer_Vector_Lists.Array_of_Lists;
lilifu : in out Standard_Integer_VecVecs.Link_to_VecVec ) is
liftfun : character := Menu_for_Lifting_Functions;
begin
Dispatch_Integer_Lifting(file,p,liftfun,points,lifted,lilifu);
end Driver_for_Lifting_Functions;
procedure Driver_for_Lifting_Functions
( file : in file_type; p : in Poly_Sys;
points : in Arrays_of_Floating_Vector_Lists.Array_of_Lists;
lifted : in out Arrays_of_Floating_Vector_Lists.Array_of_Lists;
lilifu : in out Standard_Floating_VecVecs.Link_to_VecVec ) is
liftfun : character := Menu_for_Lifting_Functions;
begin
Dispatch_Float_Lifting(file,p,liftfun,points,lifted,lilifu);
end Driver_for_Lifting_Functions;
procedure Driver_for_Lifting_Functions
( file : in file_type; p : in Poly_Sys;
ipoints : in Arrays_of_Integer_Vector_Lists.Array_of_Lists;
fltlif : out boolean;
fpoints : in out Arrays_of_Floating_Vector_Lists.Array_of_Lists;
ilifted : in out Arrays_of_Integer_Vector_Lists.Array_of_Lists;
flifted : in out Arrays_of_Floating_Vector_Lists.Array_of_Lists;
ililifu : in out Standard_Integer_VecVecs.Link_to_VecVec;
flilifu : in out Standard_Floating_VecVecs.Link_to_VecVec ) is
liftfun : character := Menu_for_Lifting_Functions;
ans : character;
begin
put("Type i for integer or f for floating-point lifting : ");
Ask_Alternative(ans,"if"); fltlif := (ans = 'f');
if ans = 'i'
then Dispatch_Integer_Lifting(file,p,liftfun,ipoints,ilifted,ililifu);
else fpoints := Convert(ipoints);
Dispatch_Float_Lifting(file,p,liftfun,fpoints,flifted,flilifu);
end if;
end Driver_for_Lifting_Functions;
end Drivers_for_Lifting_Functions;