Annotation of OpenXM_contrib/PHC/Ada/Math_Lib/Supports/floating_linear_inequality_solvers.ads, Revision 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>