with Standard_Floating_Numbers; use Standard_Floating_Numbers;
with Standard_Integer_Vectors;
with Standard_Floating_Vectors; use Standard_Floating_Vectors;
with Standard_Floating_Matrices; use Standard_Floating_Matrices;
package Floating_Linear_Inequality_Solvers is
-- DESCRIPTION :
-- This package provides an incremental solving procedure for systems of
-- linear inequalities with floating point entries.
-- FORMAT OF INEQUALITIES :
-- A system of linear inequalities is represented by a matrix of
-- dimensions (1..n+1,1..m). Each column contains one inequality,
-- for j in m'range(2), the jth inequality is given by
-- m(1,j)*x(1) + m(2,j)*x(2) + .. + m(m'last(1)-1,j)*x(x'last)
-- >= m(m'last(1),j),
-- where x is any vector of range m'first(1)..m'last(1)-1.
-- OPERATIONS :
-- We distinguish three types :
-- selectors : extracting feasibility information;
-- modifiers : modifying the inequalities;
-- solvers : solving means either to compute a solution
-- or to provide an inconsistency proof.
-- SELECTORS :
function Evaluate ( m : Matrix; i : integer; x : Vector )
return double_float;
-- REQUIRED : x'first = m'first(1) and x'last = m'last(1)-1.
-- DESCRIPTION :
-- Returns the evaluation of the vector x at the ith inequality, i.e.:
-- m(1,j)*x(1) + m(2,i)*x(2) + .. + m(m'last(1)-1,i)*x(x'last).
function Satisfies ( m : Matrix; i : integer; x : Vector; tol : double_float )
return boolean;
function Satisfies ( m : Matrix; x : Vector; tol : double_float )
return boolean;
function Satisfies ( m : Matrix; fst,lst : integer;
x : Vector; tol : double_float ) return boolean;
-- REQUIRED : x'first = m'first(1) and x'last = m'last(1)-1.
-- DESCRIPTION :
-- Returns true if the given vector x is a feasible solution to the
-- system of linear inequalities, defined in the columns of the matrix m.
-- When the index i is provided, then only for the ith inequality the
-- feasibility of the solution is checked.
-- If fst and lst are provided then only the columns between fst and lst
-- will be investigated.
function First_Violated ( m : Matrix; x : Vector; tol : double_float )
return integer;
function First_Violated ( m : Matrix; fst,lst : integer;
x : Vector; tol : double_float ) return integer;
-- DESCRIPTION :
-- Returns the index of the first column that contains an inequality
-- not satisfied by x. If Satisfies(m,x), then m'last(2)+1 is returned.
-- If fst and lst are provided then only the columns between fst and lst
-- will be investigated, if Satisfies(m,fst,lst,x), then lst+1 is returned.
-- INCONSISTENCY CHECKS :
function Inconsistent ( m : Matrix; i : integer; tol : double_float )
return boolean;
-- DESCRIPTION :
-- Returns true if the ith inequality represents an inconsistent
-- inequality like 0 >= c > 0, otherwise false is returned.
function Inconsistent ( m : Matrix; cols : Standard_Integer_Vectors.Vector;
x : Vector; tol : double_float ) return boolean;
-- DESCRIPTION :
-- Checks the inconsistency proof of the system of inequalities.
-- The sum of x(i)*m(*,cols(i)), for i in x'range=cols'range, yields
-- an inconsistent inequality, i.e.: the jth component of the sum
-- is in absolute value smaller than tol and the last component is
-- a positive number larger than tol.
function Inconsistent ( m : Matrix; i : integer;
cols : Standard_Integer_Vectors.Vector; x : Vector;
tol : double_float ) return boolean;
-- DESCRIPTION :
-- The inconsistency is here due to the addition of the ith inequality
-- to the linear inequality system defined by m.
-- The corresponding coefficient in the positive combination of the
-- inequalities equals 1.0 and is not contained in the vector x.
-- Note that this is the format of the proof as delivered by the solvers.
-- CONSTRUCTORS :
procedure Scale ( m : in out Matrix; i : in integer; tol : in double_float );
procedure Scale ( m : in out Matrix; tol : in double_float );
-- DESCRIPTION :
-- Scales the ith inequality or the whole system, by dividing to
-- the square root of the inner product of the normal vector.
procedure Center ( m : in out Matrix; x : in Vector );
function Center ( m : Matrix; x : Vector ) return Matrix;
-- DESCRIPTION :
-- Centers the inequalities in the system, so that the origin lies at x.
procedure Intersect2D ( m : in Matrix; i,j : in integer;
tol : in double_float;
x : out Vector; sing : out boolean );
-- REQUIRED : x'length = 2 = m'last(1)-1.
-- DESCRIPTION :
-- Computes the intersection of the ith with the jth hyperplane.
-- If sing, then both hyperplanes are (close to being) parallel,
-- otherwise, the solution is equal to the vector x.
-- SOLVERS FOR THE INEQUALITY SYSTEMS :
procedure Solve ( m : in Matrix; i : in integer; tol : in double_float;
x : in out Vector; fail : out boolean;
cols : out Standard_Integer_Vectors.Vector );
-- REQUIRED : i = First_Violated(m,x) <= m'last(2), x'range = cols'range.
-- DESCRIPTION :
-- Solves the inequality system, starting at the ith inequality.
-- ON ENTRY :
-- m a matrix representation of an inequality system;
-- i first inequality that is not satisfied;
-- tol tolerance on the rounding errors;
-- x start solution.
-- ON RETURN :
-- x solution to the first i inequalities in m,
-- when not fail, then Satisfies(m(*,1..i),x);
-- when fail, then x contains the coefficients for the
-- inconsistency proof;
-- fail if false, then x satisfies the first i inequalities,
-- otherwise, the system is inconsistent;
-- cols if fail, then cols indicates the columns of m to construct
-- the inconsistency proof, otherwise cols has no meaning.
procedure Solve ( m : in Matrix; tol : in double_float; x : in out Vector;
k : out integer;
cols : out Standard_Integer_Vectors.Vector );
-- DESCRIPTION :
-- Solves the inequality system by succesively applying the Solve above.
-- When the parameter k > m'last(2), then the vector x is a solution,
-- otherwise, k is the first inequality that makes the system inconsistent.
generic
with procedure Report ( x : in Vector; i : in integer; cont : out boolean );
-- DESCRIPTION :
-- x = current solution of the first i inequalities;
-- when cont is set to false, the computations will be stopped,
-- otherwise, the solver will continue.
procedure Iterated_Solve ( m : in Matrix; tol : in double_float;
x : in out Vector; k : out integer;
cols : out Standard_Integer_Vectors.Vector );
-- DESCRIPTION :
-- Solves the inequality system by a succesive application of the
-- incremental solver. After each new value of the solution, the procedure
-- Report is called. This enables to trace the flow of the computations
-- and to stop then, whenever necessary.
end Floating_Linear_Inequality_Solvers;