Annotation of OpenXM_contrib/PHC/Ada/Root_Counts/Stalift/integer_lifting_functions.adb, Revision 1.1.1.1
1.1 maekawa 1: with Standard_Floating_Numbers; use Standard_Floating_Numbers;
2: with Standard_Complex_Numbers; use Standard_Complex_Numbers;
3: with Standard_Complex_Vectors;
4: with Standard_Random_Numbers;
5:
6: package body Integer_Lifting_Functions is
7:
8: -- AUXILIARIES :
9:
10: function Convert ( v : Standard_Integer_Vectors.Vector )
11: return Standard_Complex_Vectors.Vector is
12:
13: -- DESCRIPTION :
14: -- Converts the given vector into a vector with complex entries.
15:
16: res : Standard_Complex_Vectors.Vector(v'range);
17:
18: begin
19: for i in v'range loop
20: res(i) := Create(double_float(v(i)));
21: end loop;
22: return res;
23: end Convert;
24:
25: function Random_Vector ( m : natural; low,upp : integer ) return Vector is
26:
27: -- DESCRIPTION :
28: -- Returns a random vector of range 1..m of randomly generated integer
29: -- values between low and upp.
30:
31: res : Vector(1..m);
32:
33: begin
34: for k in res'range loop
35: res(k) := Standard_Random_Numbers.Random(low,upp);
36: end loop;
37: return res;
38: end Random_Vector;
39:
40: function Random ( vec : Standard_Integer_Vectors.Vector ) return integer is
41:
42: -- DESCRIPTION :
43: -- Returns a random number from the given vector.
44:
45: index : integer := Standard_Random_Numbers.Random(vec'first,vec'last);
46:
47: begin
48: return vec(index);
49: end Random;
50:
51: -- LINEAR LIFTING :
52:
53: function Linear_Lift ( lf,v : Vector ) return Vector is
54:
55: res : Vector(v'first..v'last+1);
56:
57: begin
58: res(v'range) := v;
59: res(res'last) := lf*v;
60: return res;
61: end Linear_Lift;
62:
63: function Linear_Lift ( lf : Vector; l : List ) return List is
64:
65: res,res_last : List;
66: tmp : List := l;
67:
68: begin
69: while not Is_Null(tmp) loop
70: Append(res,res_last,Linear_Lift(lf,Head_Of(tmp).all));
71: tmp := Tail_Of(tmp);
72: end loop;
73: return res;
74: end Linear_Lift;
75:
76: function Linear_Lift ( lf : VecVec;
77: l : Array_of_Lists ) return Array_of_Lists is
78:
79: res : Array_of_Lists(l'range);
80:
81: begin
82: for i in res'range loop
83: res(i) := Linear_Lift(lf(i).all,l(i));
84: end loop;
85: return res;
86: end Linear_Lift;
87:
88: -- POLYNOMIAL LIFTING :
89:
90: function Polynomial_Lift ( lf : Poly; v : Vector ) return Vector is
91:
92: res : Vector(v'first..v'last+1);
93:
94: begin
95: res(v'range) := v;
96: res(res'last) := integer(REAL_PART(Eval(lf,Convert(v))));
97: return res;
98: end Polynomial_Lift;
99:
100: function Polynomial_Lift ( lf : Eval_Poly; v : Vector ) return Vector is
101:
102: res : Vector(v'first..v'last+1);
103:
104: begin
105: res(v'range) := v;
106: res(res'last) := integer(REAL_PART(Eval(lf,Convert(v))));
107: return res;
108: end Polynomial_Lift;
109:
110: function Polynomial_Lift ( lf : Poly; l : List ) return List is
111:
112: res : List;
113: elf : Eval_Poly := Create(lf);
114:
115: begin
116: res := Polynomial_Lift(elf,l);
117: Clear(elf);
118: return res;
119: end Polynomial_Lift;
120:
121: function Polynomial_Lift ( lf : Eval_Poly; l : List ) return List is
122:
123: res,res_last : List;
124: tmp : List := l;
125:
126: begin
127: while not Is_Null(tmp) loop
128: Append(res,res_last,Polynomial_Lift(lf,Head_Of(tmp).all));
129: tmp := Tail_Of(tmp);
130: end loop;
131: return res;
132: end Polynomial_Lift;
133:
134: function Polynomial_Lift ( lf : Poly_Sys; l : Array_of_Lists )
135: return Array_of_Lists is
136:
137: res : Array_of_Lists(l'range);
138: elf : Eval_Poly_Sys(lf'range) := Create(lf);
139:
140: begin
141: res := Polynomial_Lift(elf,l);
142: Clear(elf);
143: return res;
144: end Polynomial_Lift;
145:
146: function Polynomial_Lift ( lf : Eval_Poly_Sys; l : Array_of_Lists )
147: return Array_of_Lists is
148:
149: res : Array_of_Lists(l'range);
150:
151: begin
152: for i in res'range loop
153: res(i) := Polynomial_Lift(lf(i),l(i));
154: end loop;
155: return res;
156: end Polynomial_Lift;
157:
158: -- RANDOM LIFTING :
159:
160: function Random_Lift ( lflow,lfupp : integer; v : Vector ) return Vector is
161:
162: res : Vector(v'first..v'last+1);
163:
164: begin
165: res(v'range) := v;
166: res(res'last) := Standard_Random_Numbers.Random(lflow,lfupp);
167: return res;
168: end Random_Lift;
169:
170: function Random_Lift ( lflow,lfupp : integer; l : List ) return List is
171:
172: res,res_last : List;
173: tmp : List := l;
174:
175: begin
176: while not Is_Null(tmp) loop
177: Append(res,res_last,Random_Lift(lflow,lfupp,Head_Of(tmp).all));
178: tmp := Tail_Of(tmp);
179: end loop;
180: return res;
181: end Random_Lift;
182:
183: function Random_Lift ( lflow,lfupp : Vector; l : Array_of_Lists )
184: return Array_of_Lists is
185:
186: res : Array_of_Lists(l'range);
187:
188: begin
189: for i in res'range loop
190: res(i) := Random_Lift(lflow(i),lfupp(i),l(i));
191: end loop;
192: return res;
193: end Random_Lift;
194:
195: -- RANDOM LINEAR LIFTING :
196:
197: function Random_Linear_Lift ( lflow,lfupp : integer; v : Vector )
198: return Vector is
199:
200: lf : Vector(v'range) := Random_Vector(v'last,lflow,lfupp);
201:
202: begin
203: return Linear_Lift(lf,v);
204: end Random_Linear_Lift;
205:
206: function Random_Linear_Lift ( lflow,lfupp : integer; l : List )
207: return List is
208: begin
209: if Is_Null(l)
210: then return l;
211: else declare
212: n : constant natural := Head_Of(l)'length;
213: lf : Vector(Head_Of(l)'range) := Random_Vector(n,lflow,lfupp);
214: begin
215: return Linear_Lift(lf,l);
216: end;
217: end if;
218: end Random_Linear_Lift;
219:
220: function Random_Linear_Lift ( lflow,lfupp : Vector; l : Array_of_Lists )
221: return Array_of_Lists is
222:
223: res : Array_of_Lists(l'range);
224:
225: begin
226: for i in res'range loop
227: res(i) := Random_Linear_Lift(lflow(i),lfupp(i),l(i));
228: end loop;
229: return res;
230: end Random_Linear_Lift;
231:
232: -- POINT-WISE LIFTING :
233:
234: function Point_Lift ( lf : integer; v : Vector ) return Vector is
235:
236: res : Vector(v'first..v'last+1);
237:
238: begin
239: res(v'range) := v;
240: res(res'last) := lf;
241: return res;
242: end Point_Lift;
243:
244: function Point_Lift ( lf : Vector; l : List ) return List is
245:
246: res,res_last : List;
247: tmp : List := l;
248: ind : integer := lf'first;
249:
250: begin
251: while not Is_Null(tmp) loop
252: Append(res,res_last,Point_Lift(lf(ind),Head_Of(tmp).all));
253: ind := ind + 1;
254: tmp := Tail_Of(tmp);
255: end loop;
256: return res;
257: end Point_Lift;
258:
259: function Point_Lift ( lf : VecVec;
260: l : Array_of_Lists ) return Array_of_Lists is
261:
262: res : Array_of_Lists(l'range);
263:
264: begin
265: for i in res'range loop
266: res(i) := Point_Lift(lf(i).all,l(i));
267: end loop;
268: return res;
269: end Point_Lift;
270:
271: end Integer_Lifting_Functions;
FreeBSD-CVSweb <freebsd-cvsweb@FreeBSD.org>