Annotation of OpenXM_contrib/PHC/Ada/Root_Counts/Stalift/drivers_for_lifting_functions.adb, Revision 1.1.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