Annotation of OpenXM_contrib/PHC/Ada/Root_Counts/Stalift/drivers_for_lifting_functions.adb, Revision 1.1
1.1 ! maekawa 1: with integer_io; use integer_io;
! 2: with Communications_with_User; use Communications_with_User;
! 3: with Standard_Floating_Numbers_io; use Standard_Floating_Numbers_io;
! 4: with Numbers_io; use Numbers_io;
! 5: with Standard_Random_Numbers; use Standard_Random_Numbers;
! 6: with Standard_Integer_Vectors;
! 7: with Standard_Integer_Vectors_io; use Standard_Integer_Vectors_io;
! 8: with Standard_Floating_Vectors;
! 9: with Standard_Floating_Vectors_io; use Standard_Floating_Vectors_io;
! 10: with Standard_Complex_Poly_Systems_io; use Standard_Complex_Poly_Systems_io;
! 11: with Arrays_of_Integer_Vector_Lists_io; use Arrays_of_Integer_Vector_Lists_io;
! 12: with Integer_Lifting_Functions; use Integer_Lifting_Functions;
! 13: with Integer_Lifting_Utilities; use Integer_Lifting_Utilities;
! 14: with Floating_Lifting_Functions; use Floating_Lifting_Functions;
! 15: with Floating_Lifting_Utilities; use Floating_Lifting_Utilities;
! 16: with Floating_Integer_Convertors; use Floating_Integer_Convertors;
! 17: with Floating_Mixed_Subdivisions_io;
! 18:
! 19: package body Drivers_for_Lifting_Functions is
! 20:
! 21: -- AUXILIARIES :
! 22:
! 23: procedure put ( file : in file_type;
! 24: v : in Standard_Floating_Vectors.Vector;
! 25: fore,aft,exp : in natural ) is
! 26: begin
! 27: for i in v'range loop
! 28: put(file,v(i),fore,aft,exp);
! 29: end loop;
! 30: end put;
! 31:
! 32: procedure put ( v : in Standard_Floating_Vectors.Vector;
! 33: fore,aft,exp : in natural ) is
! 34: begin
! 35: put(Standard_Output,v,fore,aft,exp);
! 36: end put;
! 37:
! 38: procedure Read_Integer_Vector
! 39: ( v : in out Standard_Integer_Vectors.Vector ) is
! 40: begin
! 41: for i in v'range loop
! 42: put("Give integer for component "); put(i,1); put(" : ");
! 43: Read_Integer(v(i));
! 44: end loop;
! 45: end Read_Integer_Vector;
! 46:
! 47: procedure Read_Float_Vector
! 48: ( v : in out Standard_Floating_Vectors.Vector ) is
! 49: begin
! 50: for i in v'range loop
! 51: put("Give float for component "); put(i,1); put(" : ");
! 52: Read_Double_Float(v(i));
! 53: end loop;
! 54: end Read_Float_Vector;
! 55:
! 56: procedure Set_Integer_Bounds
! 57: ( file : in file_type;
! 58: low,upp : in out Standard_Integer_Vectors.Vector ) is
! 59:
! 60: -- DESCRIPTION :
! 61: -- Shows the default values for lower and upper bounds and allows
! 62: -- the user to modify these.
! 63:
! 64: ans : character;
! 65: m : constant natural := low'length;
! 66:
! 67: begin
! 68: loop
! 69: new_line;
! 70: put_line("Current lower and upper bounds on lifting values");
! 71: put(" lower : "); put(low); new_line;
! 72: put(" upper : "); put(upp); new_line;
! 73: put("Do you want to change these values ? (y/n) ");
! 74: Ask_Yes_or_No(ans);
! 75: exit when ans /= 'y';
! 76: put("Reading "); put(m,1); put(" lower bounds ");
! 77: put_line("for the lifting."); Read_Integer_Vector(low);
! 78: put("Reading "); put(m,1); put(" upper bounds ");
! 79: put_line("for the lifting."); Read_Integer_Vector(upp);
! 80: end loop;
! 81: put(file," Lower bounds : "); put(file,low); new_line(file);
! 82: put(file," Upper bounds : "); put(file,upp); new_line(file);
! 83: end Set_Integer_Bounds;
! 84:
! 85: procedure Set_Float_Bounds
! 86: ( file : in file_type;
! 87: low,upp : in out Standard_Floating_Vectors.Vector ) is
! 88:
! 89: -- DESCRIPTION :
! 90: -- Shows the default values for lower and upper bounds and allows
! 91: -- the user to modify these.
! 92:
! 93: ans : character;
! 94: m : constant natural := low'length;
! 95:
! 96: begin
! 97: loop
! 98: new_line;
! 99: put_line("Current lower and upper bounds on lifting values");
! 100: put(" lower : "); put(low,2,3,3); new_line;
! 101: put(" upper : "); put(upp,2,3,3); new_line;
! 102: put("Do you want to change these values ? (y/n) ");
! 103: Ask_Yes_or_No(ans);
! 104: exit when ans /= 'y';
! 105: put("Reading "); put(m,1); put(" lower bounds ");
! 106: put_line("for the lifting."); Read_Float_Vector(low);
! 107: put("Reading "); put(m,1); put(" upper bounds ");
! 108: put_line("for the lifting."); Read_Float_Vector(upp);
! 109: end loop;
! 110: put(file," Lower bounds : "); put(file,low,2,3,3); new_line(file);
! 111: put(file," Upper bounds : "); put(file,upp,2,3,3); new_line(file);
! 112: end Set_Float_Bounds;
! 113:
! 114: function Read_Integer_Lifting
! 115: ( l : Lists_of_Integer_Vectors.List )
! 116: return Lists_of_Integer_Vectors.List is
! 117:
! 118: use Lists_of_Integer_Vectors;
! 119: use Standard_Integer_Vectors;
! 120:
! 121: tmp : List := l;
! 122: res,res_last : List;
! 123:
! 124: begin
! 125: put_line("Give a lifting value for the following points :");
! 126: while not Is_Null(tmp) loop
! 127: declare
! 128: v : constant Vector := Head_Of(tmp).all;
! 129: lv : Vector(v'first..v'last+1);
! 130: begin
! 131: lv(v'range) := v;
! 132: put(v); put(" : "); Read_Integer(lv(lv'last));
! 133: Append(res,res_last,lv);
! 134: end;
! 135: tmp := Tail_Of(tmp);
! 136: end loop;
! 137: return res;
! 138: end Read_Integer_Lifting;
! 139:
! 140: function Read_Float_Lifting
! 141: ( l : Lists_of_Floating_Vectors.List )
! 142: return Lists_of_Floating_Vectors.List is
! 143:
! 144: use Lists_of_Floating_Vectors;
! 145: use Standard_Floating_Vectors;
! 146:
! 147: tmp : List := l;
! 148: res,res_last : List;
! 149:
! 150: begin
! 151: put_line("Give a lifting value for the following points :");
! 152: while not Is_Null(tmp) loop
! 153: declare
! 154: v : constant Vector := Head_Of(tmp).all;
! 155: lv : Vector(v'first..v'last+1);
! 156: begin
! 157: lv(v'range) := v;
! 158: put(v,0,0,0); put(" : "); Read_Double_Float(lv(lv'last));
! 159: Append(res,res_last,lv);
! 160: end;
! 161: tmp := Tail_Of(tmp);
! 162: end loop;
! 163: return res;
! 164: end Read_Float_Lifting;
! 165:
! 166: procedure Integer_Random_Linear_Lifting
! 167: ( file : in file_type; n : in natural;
! 168: points : in Arrays_of_Integer_Vector_Lists.Array_of_Lists;
! 169: lifted : in out Arrays_of_Integer_Vector_Lists.Array_of_Lists;
! 170: lilifu : in out Standard_Integer_VecVecs.Link_to_VecVec ) is
! 171:
! 172: low : Standard_Integer_Vectors.Vector(points'range) := (points'range => 0);
! 173: upp : Standard_Integer_Vectors.Vector(points'range)
! 174: := Adaptive_Lifting(points);
! 175: ranvec : Standard_Integer_Vectors.Vector(1..n);
! 176:
! 177: begin
! 178: Set_Integer_Bounds(file,low,upp);
! 179: lilifu := new Standard_Integer_VecVecs.VecVec(points'range);
! 180: for i in lilifu'range loop
! 181: for j in ranvec'range loop
! 182: ranvec(j) := Random(low(i),upp(i));
! 183: end loop;
! 184: lilifu(i) := new Standard_Integer_Vectors.Vector'(ranvec);
! 185: end loop;
! 186: lifted := Linear_Lift(lilifu.all,points);
! 187: end Integer_Random_Linear_Lifting;
! 188:
! 189: procedure Float_Random_Linear_Lifting
! 190: ( file : in file_type; n : in natural;
! 191: points : in Arrays_of_Floating_Vector_Lists.Array_of_Lists;
! 192: lifted : in out Arrays_of_Floating_Vector_Lists.Array_of_Lists;
! 193: lilifu : in out Standard_Floating_VecVecs.Link_to_VecVec ) is
! 194:
! 195: m : constant natural := points'last;
! 196: low : Standard_Floating_Vectors.Vector(points'range)
! 197: := (points'range => 0.0);
! 198: upp : Standard_Floating_Vectors.Vector(points'range)
! 199: := Adaptive_Lifting(points);
! 200: ranvec : Standard_Floating_Vectors.Vector(1..n);
! 201:
! 202: begin
! 203: Set_Float_Bounds(file,low,upp);
! 204: lilifu := new Standard_Floating_VecVecs.VecVec(points'range);
! 205: for i in lilifu'range loop
! 206: ranvec := Random(m,low(i),upp(i));
! 207: lifted(i) := Linear_Lift(points(i),ranvec);
! 208: lilifu(i) := new Standard_Floating_Vectors.Vector'(ranvec);
! 209: end loop;
! 210: end Float_Random_Linear_Lifting;
! 211:
! 212: procedure Integer_User_Linear_Lifting
! 213: ( file : in file_type; n : in natural;
! 214: points : in Arrays_of_Integer_Vector_Lists.Array_of_Lists;
! 215: lifted : in out Arrays_of_Integer_Vector_Lists.Array_of_Lists;
! 216: lilifu : in out Standard_Integer_VecVecs.Link_to_VecVec ) is
! 217:
! 218: lift : Standard_Integer_VecVecs.VecVec(points'range);
! 219:
! 220: begin
! 221: for k in lift'range loop
! 222: put("Give "); put(n,1); put(" integers for ");
! 223: put("vector "); put(k,1); put(" : "); get(n,lift(k));
! 224: put(file," vector "); put(file,k,1);
! 225: put(file," : "); put(file,lift(k)); new_line(file);
! 226: end loop;
! 227: lifted := Linear_Lift(lift,points);
! 228: lilifu := new Standard_Integer_VecVecs.VecVec'(lift);
! 229: end Integer_User_Linear_Lifting;
! 230:
! 231: procedure Float_User_Linear_Lifting
! 232: ( file : in file_type; n : in natural;
! 233: points : in Arrays_of_Floating_Vector_Lists.Array_of_Lists;
! 234: lifted : in out Arrays_of_Floating_Vector_Lists.Array_of_Lists;
! 235: lilifu : in out Standard_Floating_VecVecs.Link_to_VecVec ) is
! 236:
! 237: lift : Standard_Floating_VecVecs.VecVec(points'range);
! 238:
! 239: begin
! 240: for k in lift'range loop
! 241: put("Give "); put(n,1); put(" floats for ");
! 242: put("vector "); put(k,1); put(" : "); get(n,lift(k));
! 243: put(file," vector "); put(file,k,1);
! 244: put(file," : "); put(file,lift(k)); new_line(file);
! 245: lifted(k) := Linear_Lift(points(k),lift(k).all);
! 246: end loop;
! 247: lilifu := new Standard_Floating_VecVecs.VecVec'(lift);
! 248: end Float_User_Linear_Lifting;
! 249:
! 250: procedure Integer_Polynomial_Lifting
! 251: ( file : in file_type;
! 252: points : in Arrays_of_Integer_Vector_Lists.Array_of_Lists;
! 253: lifted : in out Arrays_of_Integer_Vector_Lists.Array_of_Lists ) is
! 254:
! 255: lift : Link_to_Poly_Sys;
! 256:
! 257: begin
! 258: get(lift);
! 259: put(file,lift.all);
! 260: lifted := Polynomial_Lift(lift.all,points);
! 261: end Integer_Polynomial_Lifting;
! 262:
! 263: procedure Float_Polynomial_Lifting
! 264: ( file : in file_type;
! 265: points : in Arrays_of_Floating_Vector_Lists.Array_of_Lists;
! 266: lifted : in out Arrays_of_Floating_Vector_Lists.Array_of_Lists ) is
! 267:
! 268: lift : Link_to_Poly_Sys;
! 269:
! 270: begin
! 271: get(lift);
! 272: put(file,lift.all);
! 273: lifted := Polynomial_Lift(lift.all,points);
! 274: end Float_Polynomial_Lifting;
! 275:
! 276: procedure Integer_User_Point_Wise_Lifting
! 277: ( file : in file_type;
! 278: points : in Arrays_of_Integer_Vector_Lists.Array_of_Lists;
! 279: lifted : in out Arrays_of_Integer_Vector_Lists.Array_of_Lists ) is
! 280: begin
! 281: for k in points'range loop
! 282: lifted(k) := Read_Integer_Lifting(points(k));
! 283: end loop;
! 284: end Integer_User_Point_Wise_Lifting;
! 285:
! 286: procedure Float_User_Point_Wise_Lifting
! 287: ( file : in file_type;
! 288: points : in Arrays_of_Floating_Vector_Lists.Array_of_Lists;
! 289: lifted : in out Arrays_of_Floating_Vector_Lists.Array_of_Lists ) is
! 290: begin
! 291: for k in points'range loop
! 292: lifted(k) := Read_Float_Lifting(points(k));
! 293: end loop;
! 294: end Float_User_Point_Wise_Lifting;
! 295:
! 296: procedure Integer_Random_Point_Wise_Lifting
! 297: ( file : in file_type;
! 298: points : in Arrays_of_Integer_Vector_Lists.Array_of_Lists;
! 299: lifted : in out Arrays_of_Integer_Vector_Lists.Array_of_Lists ) is
! 300:
! 301: low : Standard_Integer_Vectors.Vector(points'range) := (points'range => 0);
! 302: upp : Standard_Integer_Vectors.Vector(points'range)
! 303: := Adaptive_Lifting(points);
! 304:
! 305: begin
! 306: Set_Integer_Bounds(file,low,upp);
! 307: lifted := Random_Lift(low,upp,points);
! 308: end Integer_Random_Point_Wise_Lifting;
! 309:
! 310: procedure Float_Random_Point_Wise_Lifting
! 311: ( file : in file_type;
! 312: points : in Arrays_of_Floating_Vector_Lists.Array_of_Lists;
! 313: lifted : in out Arrays_of_Floating_Vector_Lists.Array_of_Lists ) is
! 314:
! 315: low : Standard_Floating_Vectors.Vector(points'range)
! 316: := (points'range => 0.0);
! 317: upp : Standard_Floating_Vectors.Vector(points'range)
! 318: := Adaptive_Lifting(points);
! 319:
! 320: begin
! 321: Set_Float_Bounds(file,low,upp);
! 322: lifted := Random_Lift(points,low,upp);
! 323: end Float_Random_Point_Wise_Lifting;
! 324:
! 325: function Menu_for_Lifting_Functions return character is
! 326:
! 327: -- DESCRIPTION :
! 328: -- Displays the menu and returns the selected lifting function.
! 329:
! 330: ans : character;
! 331:
! 332: begin
! 333: put_line("MENU for Lifting Functions :");
! 334: put_line(" Linear : 1. Random linear vectors will be chosen.");
! 335: put_line(" : 2. You can choose the vectors yourself.");
! 336: put_line(" Polynomial : 3. The system to be solved will be used.");
! 337: put_line(" : 4. You can choose the polynomials yourself.");
! 338: put_line(" Point-wise : 5. For each point a random lifting value.");
! 339: put_line(" : 6. You can choose all lifting values yourself.");
! 340: put("Type a number between 1 and 6 to select lifting : ");
! 341: Ask_Alternative(ans,"123456"); return ans;
! 342: end Menu_for_Lifting_Functions;
! 343:
! 344: procedure Dispatch_Integer_Lifting
! 345: ( file : in file_type; p : in Poly_Sys; choice : in character;
! 346: points : in Arrays_of_Integer_Vector_Lists.Array_of_Lists;
! 347: lifted : in out Arrays_of_Integer_Vector_Lists.Array_of_Lists;
! 348: lilifu : in out Standard_Integer_VecVecs.Link_to_VecVec ) is
! 349:
! 350: -- DESCRIPTION :
! 351: -- Calls the appropriate lifting function to perform the lifting.
! 352:
! 353: n : constant natural := p'length;
! 354:
! 355: begin
! 356: new_line(file); put(file,"INTEGER LIFTING FUNCTION : ");
! 357: case choice is
! 358: when '1' => put_line(file,"random linear.");
! 359: Integer_Random_Linear_Lifting(file,n,points,lifted,lilifu);
! 360: when '2' => put_line(file,"linear provided by user.");
! 361: Integer_User_Linear_Lifting(file,n,points,lifted,lilifu);
! 362: when '3' => put_line(file,"polynomial system.");
! 363: lifted := Polynomial_Lift(p,points);
! 364: when '4' => put_line(file,"polynomials provided by user.");
! 365: Integer_Polynomial_Lifting(file,points,lifted);
! 366: when '5' => put_line(file,"random point-wise.");
! 367: Integer_Random_Point_Wise_Lifting(file,points,lifted);
! 368: when '6' => put_line(file,"point-wise provided by user.");
! 369: Integer_User_Point_Wise_Lifting(file,points,lifted);
! 370: when others => null;
! 371: end case;
! 372: new_line(file); put_line(file,"THE LIFTED SUPPORTS :"); new_line(file);
! 373: put(file,lifted);
! 374: end Dispatch_Integer_Lifting;
! 375:
! 376: procedure Dispatch_Float_Lifting
! 377: ( file : in file_type; p : in Poly_Sys; choice : in character;
! 378: points : in Arrays_of_Floating_Vector_Lists.Array_of_Lists;
! 379: lifted : in out Arrays_of_Floating_Vector_Lists.Array_of_Lists;
! 380: lilifu : in out Standard_Floating_VecVecs.Link_to_VecVec ) is
! 381:
! 382: -- DESCRIPTION :
! 383: -- Calls the appropriate lifting function to perform the lifting.
! 384:
! 385: n : constant natural := p'length;
! 386:
! 387: begin
! 388: new_line(file); put(file,"FLOATING-POINT LIFTING FUNCTION : ");
! 389: case choice is
! 390: when '1' => put_line(file,"random linear.");
! 391: Float_Random_Linear_Lifting(file,n,points,lifted,lilifu);
! 392: when '2' => put_line(file,"linear provided by user.");
! 393: Float_User_Linear_Lifting(file,n,points,lifted,lilifu);
! 394: when '3' => put_line(file,"polynomial system.");
! 395: lifted := Polynomial_Lift(p,points);
! 396: when '4' => put_line(file,"polynomials provided by user.");
! 397: Float_Polynomial_Lifting(file,points,lifted);
! 398: when '5' => put_line(file,"random point-wise.");
! 399: Float_Random_Point_Wise_Lifting(file,points,lifted);
! 400: when '6' => put_line(file,"point-wise provided by user.");
! 401: Float_User_Point_Wise_Lifting(file,points,lifted);
! 402: when others => null;
! 403: end case;
! 404: new_line(file); put_line(file,"THE LIFTED SUPPORTS :"); new_line(file);
! 405: Floating_Mixed_Subdivisions_io.put(file,lifted);
! 406: end Dispatch_Float_Lifting;
! 407:
! 408: -- TARGET ROUTINES :
! 409:
! 410: procedure Driver_for_Lifting_Functions
! 411: ( file : in file_type; p : in Poly_Sys;
! 412: points : in Arrays_of_Integer_Vector_Lists.Array_of_Lists;
! 413: lifted : in out Arrays_of_Integer_Vector_Lists.Array_of_Lists;
! 414: lilifu : in out Standard_Integer_VecVecs.Link_to_VecVec ) is
! 415:
! 416: liftfun : character := Menu_for_Lifting_Functions;
! 417:
! 418: begin
! 419: Dispatch_Integer_Lifting(file,p,liftfun,points,lifted,lilifu);
! 420: end Driver_for_Lifting_Functions;
! 421:
! 422: procedure Driver_for_Lifting_Functions
! 423: ( file : in file_type; p : in Poly_Sys;
! 424: points : in Arrays_of_Floating_Vector_Lists.Array_of_Lists;
! 425: lifted : in out Arrays_of_Floating_Vector_Lists.Array_of_Lists;
! 426: lilifu : in out Standard_Floating_VecVecs.Link_to_VecVec ) is
! 427:
! 428: liftfun : character := Menu_for_Lifting_Functions;
! 429:
! 430: begin
! 431: Dispatch_Float_Lifting(file,p,liftfun,points,lifted,lilifu);
! 432: end Driver_for_Lifting_Functions;
! 433:
! 434: procedure Driver_for_Lifting_Functions
! 435: ( file : in file_type; p : in Poly_Sys;
! 436: ipoints : in Arrays_of_Integer_Vector_Lists.Array_of_Lists;
! 437: fltlif : out boolean;
! 438: fpoints : in out Arrays_of_Floating_Vector_Lists.Array_of_Lists;
! 439: ilifted : in out Arrays_of_Integer_Vector_Lists.Array_of_Lists;
! 440: flifted : in out Arrays_of_Floating_Vector_Lists.Array_of_Lists;
! 441: ililifu : in out Standard_Integer_VecVecs.Link_to_VecVec;
! 442: flilifu : in out Standard_Floating_VecVecs.Link_to_VecVec ) is
! 443:
! 444: liftfun : character := Menu_for_Lifting_Functions;
! 445: ans : character;
! 446:
! 447: begin
! 448: put("Type i for integer or f for floating-point lifting : ");
! 449: Ask_Alternative(ans,"if"); fltlif := (ans = 'f');
! 450: if ans = 'i'
! 451: then Dispatch_Integer_Lifting(file,p,liftfun,ipoints,ilifted,ililifu);
! 452: else fpoints := Convert(ipoints);
! 453: Dispatch_Float_Lifting(file,p,liftfun,fpoints,flifted,flilifu);
! 454: end if;
! 455: end Driver_for_Lifting_Functions;
! 456:
! 457: end Drivers_for_Lifting_Functions;
FreeBSD-CVSweb <freebsd-cvsweb@FreeBSD.org>
![[BACK]](/icons/cvsweb/back.gif){kind=icon}
Return to drivers_for_lifting_functions.adb CVS log ![[TXT]](/icons/cvsweb/text.gif){kind=icon}
![[DIR]](/icons/cvsweb/dir.gif){kind=icon}
Up to [local] / OpenXM_contrib / PHC / Ada / Root_Counts / Stalift