--with text_io,integer_io;               use text_io,integer_io;

with Greatest_Common_Divisor;          use Greatest_Common_Divisor;
with Integer_Vectors;                  use Integer_Vectors;
with Integer_Matrices;                 use Integer_Matrices;
with Integer_Linear_System_Solvers;    use Integer_Linear_System_Solvers;

with Integer_Farkas_Lemma;             use Integer_Farkas_Lemma;

with Lists_of_Integer_Vectors;         use Lists_of_Integer_Vectors;
with Arrays_of_Integer_Vector_Lists;   use Arrays_of_Integer_Vector_Lists;
with Face_Enumerators;                 use Face_Enumerators;
with Face_Enumerators_Utilities;       use Face_Enumerators_Utilities;

package body Face_Enumerator_of_Sum is

-- IMPLEMENTATION :
--   First all faces of the requested type are generated of the individual
--   polytopes. These faces are stored and used in the generation of the
--   face of the sum.

-- GENERATE THE FACES :

  function Generate_Faces
                 ( k : natural; pts : Integer_Vectors_of_Vectors.Vector )
                 return List is

  -- DESCRIPTION :
  --   Returns a list of k-faces generated by the points in pts.

  -- NOTE :
  --   An auxiliary vector wrkpts is needed,
  --   because Farkas_Lemma does not work entirely with relative entries.

    len : constant natural := pts'length;
    offset : constant natural := pts'first - 1;
    wrkpts : Integer_Vectors_of_Vectors.Vector(1..len);
    res : List;

    procedure Update ( face : in Vector ) is
      newface : Link_to_Vector := new Integer_Vectors.Vector'(face);
    begin
      for i in newface'range loop
        newface(i) := newface(i) + offset;
      end loop;
      Construct(newface,res);
    end Update;

    procedure Collect_Vertex ( i : in integer; cont : out boolean ) is
      face : Vector(0..0);
    begin
      face(0) := i; Update(face); cont := true;
    end Collect_Vertex;
    procedure Collect_Vertices is new Enumerate_Vertices(Collect_Vertex);

    procedure Collect_Edge ( i,j : in integer; cont : out boolean ) is
      face : Vector(0..1);
    begin
      face(0) := i;  face(1) := j;
      Update(face);  cont := true;
    end Collect_Edge;
    procedure Collect_Edges is new Enumerate_Edges(Collect_Edge);

    procedure Collect_Face ( face : in Vector; cont : out boolean ) is
    begin
      Update(face); cont := true;
    end Collect_Face;
    procedure Collect_Faces is new Enumerate_Faces(Collect_Face);

  begin
    wrkpts(1..len) := pts(pts'range);
    case k is
      when 0      => Collect_Vertices(wrkpts);
      when 1      => Collect_Edges(wrkpts);
      when others => Collect_Faces(k,wrkpts);
    end case;
    return res;
  end Generate_Faces;

  function Generate_Faces
                 ( typ,ind : vector; pts : Integer_Vectors_of_Vectors.Vector )
                 return Array_of_Lists is

  -- DESCRIPTION :
  --   Returns an array of lists, which contains the typ(i)-faces of the
  --   polytope generated by pts(ind(i)..ind(i+1)-1).

    res : Array_of_Lists(typ'range);

  begin
    for i in res'range loop
      if i < ind'last
       then res(i) := Generate_Faces(typ(i),pts(ind(i)..ind(i+1)-1));
       else res(i) := Generate_Faces(typ(i),pts(ind(i)..pts'last));
      end if;
    end loop;
    return res;
  end Generate_Faces;

-- ELIMINATORS :

  procedure Eliminate ( pivot : in integer; elim : in Integer_Vectors.Vector;
                        target : in out Integer_Vectors.Vector ) is

  -- DESCRIPTION :
  --   Makes target(pivot) = 0 by means of making a linear
  --   combination of the vectors target and elim.

  -- REQUIRED ON ENTRY :
  --   target(pivot) /= 0 and elim(pivot) /= 0

    a,b,lcmab,faca,facb : integer;

  begin
    a := elim(pivot); b := target(pivot);
    lcmab := lcm(a,b);
    if lcmab < 0 then lcmab := -lcmab; end if;
    faca := lcmab/a;  facb := lcmab/b;
    if facb < 0
     then facb := -facb; faca := -faca;
    end if;
    for j in target'range loop
      target(j) := facb*target(j) - faca*elim(j);
    end loop;
    Scale(target);
  end Eliminate;

  procedure Eliminate ( l : in natural; pivots : in Integer_Vectors.Vector;
                        elim : in Integer_Vectors_of_Vectors.Vector;
                        target : in out Integer_Vectors.Vector ) is

  -- DESCRIPTION :
  --   Makes target(pivots(i)) = 0 by means of making a linear
  --   combination of the vectors target and elim(i), for i in 1..l.

  -- REQUIRED ON ENTRY :
  --   elim(i)(pivots(i)) /= 0

  begin
    for i in 1..l loop
      if target(pivots(i)) /= 0
       then Eliminate(pivots(i),elim(i).all,target);
      end if;
    end loop;
  end Eliminate;

  function Pivot_after_Elimination
             ( l,k : in natural; point,face,pivots : in Integer_Vectors.Vector;
               elim : in Integer_Vectors_of_Vectors.Vector ) return natural is

  -- DESCRIPTION :
  --   Returns the first nonzero element of the given point after elimination
  --   w.r.t. the entries in the face with lower index.

    work : Integer_Vectors.Vector(point'range) := point - elim(1-k).all;
    pivot : integer;

  begin
    for i in (face'first+1)..face'last loop
      if (face(i) < l) and then (work(pivots(i)) /= 0)
       then Eliminate(pivots(i),elim(i).all,work);
      end if;
      exit when (face(i) > l);
    end loop;
    pivot := 0;
    for i in work'range loop
      if work(pivots(i)) /= 0
       then pivot := i;
      end if;
      exit when (pivot /= 0);
    end loop;
    return pivot;
  end Pivot_after_Elimination;

  procedure Update_Pivots
               ( point : in Integer_Vectors.Vector; l : in natural;
                 pivots : in out Integer_Vectors.Vector;
                 pivot : out natural ) is

  -- DESCRIPTION :
  --   Searches in the point(l..point'last) for the first nonzero entry
  --   and updates the pivoting information.

    temp,piv : integer;

  begin
    piv := 0;
    for i in l..point'last loop
      if point(pivots(i)) /= 0
       then piv := i;
      end if;
      exit when (piv /= 0);
    end loop;
    if piv /= 0 and then (piv /= l)
     then temp := pivots(l);
          pivots(l) := pivots(piv);
          pivots(piv) := temp;
    end if;
    pivot := piv;
  end Update_Pivots;

  procedure Update_Eliminator_for_Sum
               ( elim : in out Integer_Vectors_of_Vectors.Vector;
                 l : in natural; pivots : in out Integer_Vectors.Vector;
                 point : in Integer_Vectors.Vector; index : in natural;
                 pivot : out natural ) is

  -- DESCRIPTION :
  --   Updates the vector of eliminators, by adding the lth elimination
  --   equation.  This procedure ensures the invariant condition on the
  --   eliminator, which has to be upper triangular.  If this cannot be
  --   achieved, degeneracy is indicated by pivot = 0.

  -- ON ENTRY :
  --   elim      vector of elimination equations: elim(i)(pivots(i)) /= 0
  --             and for j in 1..(i-1) : elim(i)(pivots(j)) = 0,
  --             for i in 1..(l-1), elim(1-index) contains the basis point;
  --   l         index of current elimination equation to be made;
  --   pivots    contains the pivoting information;
  --   point     new point to make the equation `point - elim(1-index) = 0';
  --   index     indicates the current polytope.

  -- ON RETURN :
  --   elim      if not degen, then elim(l)(pivots(l)) /= 0 and
  --             for i in 1..(l-1): elim(l)(pivots(i)) = 0;
  --   pivots    updated pivot information;
  --   piv       the pivot that has been used for elim(l)(pivots(l)) /= 0;
  --             piv = 0 when the new elimination equation elim(l)
  --             became entirely zero after ensuring the invariant condition.

  begin
    elim(l) := new Integer_Vectors.Vector'(point - elim(1-index).all);
    Eliminate(l-1,pivots,elim,elim(l).all);
    Update_Pivots(elim(l).all,l,pivots,pivot);
  end Update_Eliminator_for_Sum;

  procedure Create_Tableau_for_Faces_of_Sum
               ( k,n,i,r : in natural; ind,pivots : in Integer_Vectors.Vector;
                 pts,elim,face : in Integer_Vectors_of_Vectors.Vector;
                 tab : out matrix; lastcol : out integer;
                 degenerate : out boolean ) is

  -- DESCRIPTION :
  --   Creates the table of inequalities for determining whether the given
  --   candidate face spans a face of the sum polytope.

  -- ON ENTRY :
  --   k         dimension of the face on the sum;
  --   n         dimension of the points;
  --   i         current polytope;
  --   r         number of polytopes;
  --   ind       indicate the beginning vector in pts of each polytope;
  --   etc...

    column : integer := 1;
    ineq : Integer_Vectors.Vector(1..n);
    last : integer;

  begin
    degenerate := false;
    for l1 in face'first..i loop
      if l1 = r
       then last := pts'last;
       else last := ind(l1+1)-1;
      end if;
      for l2 in ind(l1)..last loop
        if not Is_In(l2,face(l1).all)
         then
           ineq := pts(l2).all - elim(1-l1).all;  -- new inequality
           Eliminate(k,pivots,elim,ineq);     -- ineq(pivots(i)) = 0, i=1,2,..k
           if Is_Zero(ineq)
            then
              if not In_Face(face(l1)'length-1,face(l1).all,pts(l2).all,pts)
                and then face(l1)(face(l1)'first) <= l2
                and then l2 < face(l1)(face(l1)'last)
                                              -- lexicographic enumeration
                and then (Pivot_after_Elimination
                             (l2,l1,pts(l2).all,face(l1).all,pivots,elim) /= 0)
               then degenerate := true; return;
              end if;
            else
              for ll in (k+1)..n loop                 -- fill in the column
                tab(ll-k,column) := ineq(pivots(ll));
              end loop;
              tab(tab'last(1),column) := 1;
              column := column + 1;
           end if;
        end if;
      end loop;
    end loop;
    for l in tab'first(1)..(tab'last(1)-1) loop  -- right hand side
      tab(l,tab'last(2)) := 0;
    end loop;
    tab(tab'last(1),tab'last(2)) := 1;
    lastcol := column-1;
  end Create_Tableau_for_Faces_of_Sum;

  function Is_Face_of_Sum
                ( k,n,m,i,r : natural;
                  elim,pts,face : Integer_Vectors_of_Vectors.Vector;
                  ind,pivots : Integer_Vectors.Vector ) return boolean is

  -- DESCRIPTION :
  --   Applies Complementary Slackness to determine whether the given
  --   candidate face is a face of the polytope.

  -- ON ENTRY :
  --   k          dimension of the candidate face;
  --   n          dimension of the vector space;
  --   m          number of total points which span the polytope;
  --   i          current polytope;
  --   r          number of different polytopes;
  --   elim       elimination equations in upper triangular form;
  --   pts        the points which span the polytope;
  --   face       entries of the points which span the candidate face;
  --   ind        indicates the starting vector in pts of each polytope;
  --   pivots     pivoting information for the elimination equations.

    nn : constant natural := n-k+1;
    tab : matrix(1..nn,1..(m-k));
    deg,feasible : boolean;
    lst : integer;

  begin
    if m - k <= 1
     then return true;
     else
       Create_Tableau_for_Faces_of_Sum
             (k,n,i,r,ind,pivots,pts,elim,face,tab,lst,deg);
      -- put_line("The tableau of inequalities : "); put(tab);
       if deg
        then --put_line("Tableau is degenerate: no solution :");
             return false;
        elsif lst = 0
            then return true;
            else Integer_Complementary_Slackness(tab,lst,feasible);
                 --if feasible
                 -- then put_line(" is feasible");
                 -- else put_line(" is not feasible");
                 --end if;
                 return not feasible;
       end if;
    end if;
  end Is_Face_of_Sum;

-- TARGET ROUTINE :

  procedure Enumerate_Faces_of_Sum
                  ( ind,typ : in vector; k : in natural;
                    pts : in Integer_Vectors_of_Vectors.Vector ) is

    m : constant natural := pts'length;             -- number of points
    n : constant natural := pts(pts'first)'length;  -- dimension of vectors
    r : constant natural := ind'length;             -- number of polytopes
    faces : Array_of_Lists(typ'range);                    -- all typ(i)-faces
    candidates : Integer_Vectors_of_Vectors.Vector(1..r); -- current tuple
    elim : Integer_Vectors_of_Vectors.Vector(1-r..k);     -- elimination vector
    continue : boolean := true;
    last,sum,piv : natural;

    procedure Candidate_Faces_of_Sum
                   ( ipvt : in Integer_Vectors.Vector; i : in integer ) is

    -- DESCRIPTION :
    --   Enumerates all typ(i)-faces of the given type in the sum,
    --   i indicates the current polytope.

      tmp : List := faces(i);
      pivots : Integer_Vectors.Vector(1..n);

    begin
      if i = r                                  -- initialization
       then last := m;
       else last := ind(i+1)-1;
      end if;
      sum := sum + typ(i);
      while not Is_Null(tmp) loop               -- enumerate all typ(i)-faces
        candidates(i) := Head_Of(tmp);
        elim(1-i) := pts(candidates(i)(0));     -- update the eliminator
        pivots := ipvt;  piv := 1;
        for j in candidates(i)'first+1..candidates(i)'last loop
          Update_Eliminator_for_Sum(elim,sum-typ(i)+j,pivots,
                                    pts(candidates(i)(j)).all,i,piv);
          exit when (piv = 0);
        end loop;
        if (piv /= 0)                           -- decide to proceed
          and then ((typ(i) = last-ind(i)+1)
          or else Is_Face_of_Sum(sum,n,last-i+1,i,r,elim,pts(pts'first..last),
                                 candidates,ind,pivots))
         then if i = r
               then Process(candidates,continue);
               else Candidate_Faces_of_Sum(pivots,i+1);
              end if;
        end if;
        for j in candidates(i)'first+1..candidates(i)'last loop    -- restore
          Clear(elim(sum-typ(i)+j));
        end loop;
        tmp := Tail_Of(tmp);                   -- take next candidate
      end loop;
      sum := sum - typ(i);
    end Candidate_Faces_of_Sum;

  begin
    faces := Generate_Faces(typ,ind,pts);
   -- put("The cardinality of the faces : ");
   -- for i in faces'range loop
   --   put(Length_Of(faces(i)),1); put(" ");
   -- end loop;
   -- new_line;
    declare
      ipvt : Integer_Vectors.Vector(1..n);
    begin
      for i in ipvt'range loop
        ipvt(i) := i;
      end loop;
      sum := 0;
      Candidate_Faces_of_Sum(ipvt,1);
    end;
    Deep_Clear(faces);
  end Enumerate_Faces_of_Sum;

end Face_Enumerator_of_Sum;
