Annotation of OpenXM_contrib/PHC/Ada/Math_Lib/Supports/floating_linear_inequality_solvers.ads, Revision 1.1.1.1
1.1 maekawa 1: with Standard_Floating_Numbers; use Standard_Floating_Numbers;
2: with Standard_Integer_Vectors;
3: with Standard_Floating_Vectors; use Standard_Floating_Vectors;
4: with Standard_Floating_Matrices; use Standard_Floating_Matrices;
5:
6: package Floating_Linear_Inequality_Solvers is
7:
8: -- DESCRIPTION :
9: -- This package provides an incremental solving procedure for systems of
10: -- linear inequalities with floating point entries.
11:
12: -- FORMAT OF INEQUALITIES :
13: -- A system of linear inequalities is represented by a matrix of
14: -- dimensions (1..n+1,1..m). Each column contains one inequality,
15: -- for j in m'range(2), the jth inequality is given by
16: -- m(1,j)*x(1) + m(2,j)*x(2) + .. + m(m'last(1)-1,j)*x(x'last)
17: -- >= m(m'last(1),j),
18: -- where x is any vector of range m'first(1)..m'last(1)-1.
19:
20: -- OPERATIONS :
21: -- We distinguish three types :
22: -- selectors : extracting feasibility information;
23: -- modifiers : modifying the inequalities;
24: -- solvers : solving means either to compute a solution
25: -- or to provide an inconsistency proof.
26:
27: -- SELECTORS :
28:
29: function Evaluate ( m : Matrix; i : integer; x : Vector )
30: return double_float;
31:
32: -- REQUIRED : x'first = m'first(1) and x'last = m'last(1)-1.
33:
34: -- DESCRIPTION :
35: -- Returns the evaluation of the vector x at the ith inequality, i.e.:
36: -- m(1,j)*x(1) + m(2,i)*x(2) + .. + m(m'last(1)-1,i)*x(x'last).
37:
38: function Satisfies ( m : Matrix; i : integer; x : Vector; tol : double_float )
39: return boolean;
40: function Satisfies ( m : Matrix; x : Vector; tol : double_float )
41: return boolean;
42: function Satisfies ( m : Matrix; fst,lst : integer;
43: x : Vector; tol : double_float ) return boolean;
44:
45: -- REQUIRED : x'first = m'first(1) and x'last = m'last(1)-1.
46:
47: -- DESCRIPTION :
48: -- Returns true if the given vector x is a feasible solution to the
49: -- system of linear inequalities, defined in the columns of the matrix m.
50: -- When the index i is provided, then only for the ith inequality the
51: -- feasibility of the solution is checked.
52: -- If fst and lst are provided then only the columns between fst and lst
53: -- will be investigated.
54:
55: function First_Violated ( m : Matrix; x : Vector; tol : double_float )
56: return integer;
57: function First_Violated ( m : Matrix; fst,lst : integer;
58: x : Vector; tol : double_float ) return integer;
59:
60: -- DESCRIPTION :
61: -- Returns the index of the first column that contains an inequality
62: -- not satisfied by x. If Satisfies(m,x), then m'last(2)+1 is returned.
63: -- If fst and lst are provided then only the columns between fst and lst
64: -- will be investigated, if Satisfies(m,fst,lst,x), then lst+1 is returned.
65:
66: -- INCONSISTENCY CHECKS :
67:
68: function Inconsistent ( m : Matrix; i : integer; tol : double_float )
69: return boolean;
70:
71: -- DESCRIPTION :
72: -- Returns true if the ith inequality represents an inconsistent
73: -- inequality like 0 >= c > 0, otherwise false is returned.
74:
75: function Inconsistent ( m : Matrix; cols : Standard_Integer_Vectors.Vector;
76: x : Vector; tol : double_float ) return boolean;
77:
78: -- DESCRIPTION :
79: -- Checks the inconsistency proof of the system of inequalities.
80: -- The sum of x(i)*m(*,cols(i)), for i in x'range=cols'range, yields
81: -- an inconsistent inequality, i.e.: the jth component of the sum
82: -- is in absolute value smaller than tol and the last component is
83: -- a positive number larger than tol.
84:
85: function Inconsistent ( m : Matrix; i : integer;
86: cols : Standard_Integer_Vectors.Vector; x : Vector;
87: tol : double_float ) return boolean;
88:
89: -- DESCRIPTION :
90: -- The inconsistency is here due to the addition of the ith inequality
91: -- to the linear inequality system defined by m.
92: -- The corresponding coefficient in the positive combination of the
93: -- inequalities equals 1.0 and is not contained in the vector x.
94: -- Note that this is the format of the proof as delivered by the solvers.
95:
96: -- CONSTRUCTORS :
97:
98: procedure Scale ( m : in out Matrix; i : in integer; tol : in double_float );
99: procedure Scale ( m : in out Matrix; tol : in double_float );
100:
101: -- DESCRIPTION :
102: -- Scales the ith inequality or the whole system, by dividing to
103: -- the square root of the inner product of the normal vector.
104:
105: procedure Center ( m : in out Matrix; x : in Vector );
106: function Center ( m : Matrix; x : Vector ) return Matrix;
107:
108: -- DESCRIPTION :
109: -- Centers the inequalities in the system, so that the origin lies at x.
110:
111: procedure Intersect2D ( m : in Matrix; i,j : in integer;
112: tol : in double_float;
113: x : out Vector; sing : out boolean );
114:
115: -- REQUIRED : x'length = 2 = m'last(1)-1.
116:
117: -- DESCRIPTION :
118: -- Computes the intersection of the ith with the jth hyperplane.
119: -- If sing, then both hyperplanes are (close to being) parallel,
120: -- otherwise, the solution is equal to the vector x.
121:
122: -- SOLVERS FOR THE INEQUALITY SYSTEMS :
123:
124: procedure Solve ( m : in Matrix; i : in integer; tol : in double_float;
125: x : in out Vector; fail : out boolean;
126: cols : out Standard_Integer_Vectors.Vector );
127:
128: -- REQUIRED : i = First_Violated(m,x) <= m'last(2), x'range = cols'range.
129:
130: -- DESCRIPTION :
131: -- Solves the inequality system, starting at the ith inequality.
132:
133: -- ON ENTRY :
134: -- m a matrix representation of an inequality system;
135: -- i first inequality that is not satisfied;
136: -- tol tolerance on the rounding errors;
137: -- x start solution.
138:
139: -- ON RETURN :
140: -- x solution to the first i inequalities in m,
141: -- when not fail, then Satisfies(m(*,1..i),x);
142: -- when fail, then x contains the coefficients for the
143: -- inconsistency proof;
144: -- fail if false, then x satisfies the first i inequalities,
145: -- otherwise, the system is inconsistent;
146: -- cols if fail, then cols indicates the columns of m to construct
147: -- the inconsistency proof, otherwise cols has no meaning.
148:
149: procedure Solve ( m : in Matrix; tol : in double_float; x : in out Vector;
150: k : out integer;
151: cols : out Standard_Integer_Vectors.Vector );
152:
153: -- DESCRIPTION :
154: -- Solves the inequality system by succesively applying the Solve above.
155: -- When the parameter k > m'last(2), then the vector x is a solution,
156: -- otherwise, k is the first inequality that makes the system inconsistent.
157:
158: generic
159:
160: with procedure Report ( x : in Vector; i : in integer; cont : out boolean );
161:
162: -- DESCRIPTION :
163: -- x = current solution of the first i inequalities;
164: -- when cont is set to false, the computations will be stopped,
165: -- otherwise, the solver will continue.
166:
167: procedure Iterated_Solve ( m : in Matrix; tol : in double_float;
168: x : in out Vector; k : out integer;
169: cols : out Standard_Integer_Vectors.Vector );
170:
171: -- DESCRIPTION :
172: -- Solves the inequality system by a succesive application of the
173: -- incremental solver. After each new value of the solution, the procedure
174: -- Report is called. This enables to trace the flow of the computations
175: -- and to stop then, whenever necessary.
176:
177: end Floating_Linear_Inequality_Solvers;
FreeBSD-CVSweb <freebsd-cvsweb@FreeBSD.org>
![[BACK]](/icons/cvsweb/back.gif){kind=icon}
Return to floating_linear_inequality_solvers.ads CVS log ![[TXT]](/icons/cvsweb/text.gif){kind=icon}
![[DIR]](/icons/cvsweb/dir.gif){kind=icon}
Up to [local] / OpenXM_contrib / PHC / Ada / Math_Lib / Supports