Evaluation algorithm changed to inverted interleaved depth first search

1 files changed, 265 insertions, 421 deletions

diff --git a/src/kompsos-collector.adb b/src/kompsos-collector.adb
index b8fc205..db499f2 100644
--- a/src/kompsos-collector.adb
+++ b/src/kompsos-collector.adb
@@ -5,10 +5,13 @@
 
 --  See license.txt for further details
 
+
 with
 
-    Ada.Assertions,
-    Ada.Unchecked_Deallocation;
+    Ada.Containers,
+    Ada.Unchecked_Deallocation,
+    System.Address_To_Access_Conversions,
+    System.Storage_Elements;
 
 
 package body Kompsos.Collector is
@@ -18,15 +21,22 @@ package body Kompsos.Collector is
     --  Progress State  --
     ----------------------
 
-    Book_Root   : Book_Node_Access := null;
-    Loose_Books : Loose_Book_Vectors.Vector;
+    Conjunct_Goals : Goal_Access_Vectors.Vector;
 
     Global_Var : Variable := Relation.Next_Var;
 
-    Next_Index  : Long_Positive := 1;
-    Next_State  : State;
-    State_Valid : Boolean       := False;
-    Exhausted   : Boolean       := False;
+    Up_Map    : Upwards_Maps.Map;
+    Up_Vector : Upwards_Vectors.Vector;
+
+    Do_Walk      : access procedure;
+    Walk_Trail   : Breadcrumb_Vectors.Vector;
+    Location     : Graph_Component_Access;
+    Local_Cursor : Upwards_Maps.Cursor;
+    Next_Pick    : Positive;
+
+    Result      : State   := Within;
+    State_Valid : Boolean := False;
+    Exhausted   : Boolean := False;
 
 
 
@@ -35,53 +45,84 @@ package body Kompsos.Collector is
     --  Memory Management  --
     -------------------------
 
-    procedure Free is new Ada.Unchecked_Deallocation (Book_Node, Book_Node_Access);
-    procedure Free is new Ada.Unchecked_Deallocation (Cache_Entry, Cache_Entry_Access);
     procedure Free is new Ada.Unchecked_Deallocation (Goal, Goal_Access);
-    procedure Free is new Ada.Unchecked_Deallocation (State, State_Access);
+
 
     procedure Finalize
            (This : in out Collector_Final_Controller) is
     begin
-        Reset (Relation.Graph.Actual, Book_Root);
+        for Ptr of Conjunct_Goals loop
+            Free (Ptr);
+        end loop;
     end Finalize;
 
 
 
 
-    ------------------------
-    --  Internal Helpers  --
-    ------------------------
+    -----------------
+    --  Datatypes  --
+    -----------------
 
-    --  Unification  --
+    function "<"
+           (Left, Right : in Disjuncts_Chosen)
+        return Boolean is
+    begin
+        if Left.Is_Empty then
+            return not Right.Is_Empty;
+        elsif Right.Is_Empty then
+            return False;
+        end if;
+        declare
+            Left_Spot  : Natural := Left.Last_Index;
+            Right_Spot : Natural := Right.Last_Index;
+        begin
+            loop
+                if Left (Left_Spot) < Right (Right_Spot) then
+                    return True;
+                elsif Left (Left_Spot) = Right (Right_Spot) then
+                    Left_Spot := Left_Spot - 1;
+                    Right_Spot := Right_Spot - 1;
+                    if Left_Spot = 0 then
+                        return Right_Spot /= 0;
+                    elsif Right_Spot = 0 then
+                        return False;
+                    end if;
+                else
+                    return False;
+                end if;
+            end loop;
+        end;
+    end "<";
 
-    Use_New_Node : Boolean := False;
 
-    function Append
-           (This  : in State;
-            Key   : in Variable;
-            Value : in Term)
-        return State is
+    function "<"
+           (Left, Right : in Parent_Arrow)
+        return Boolean is
     begin
-        if Use_New_Node or else This.Ctrl.Actual = null or else
-            (This.Ctrl.Actual /= null and then This.Ctrl.Actual.Valid = Valid_Count'Last)
-        then
-            Use_New_Node := False;
-            return (Ctrl => (Ada.Finalization.Controlled with
-                Actual => new State_Component'(
-                    Counter => 1,
-                    Valid   => Valid_Count'First,
-                    Data    => (1 => (Key, Value), others => <>),
-                    Next    => This)));
-        else
-            return Result : constant State := This do
-                Result.Ctrl.Actual.Valid := Result.Ctrl.Actual.Valid + 1;
-                Result.Ctrl.Actual.Data (Result.Ctrl.Actual.Valid) := (Key, Value);
-            end return;
-        end if;
-    end Append;
+        return Left.Order < Right.Order;
+    end "<";
+
+
+    package Graph_Comp_Conv is new System.Address_To_Access_Conversions (Graph_Component);
+
+    function Graph_Component_Access_Hash
+           (Key : in Graph_Component_Access)
+        return Ada.Containers.Hash_Type
+    is
+        use Ada.Containers, Graph_Comp_Conv, System.Storage_Elements;
+    begin
+        return Hash_Type (To_Integer (To_Address (Object_Pointer (Key))) mod Hash_Type'Modulus);
+    end Graph_Component_Access_Hash;
+
+
 
 
+    ------------------------
+    --  Internal Helpers  --
+    ------------------------
+
+    --  Unification  --
+
     procedure Walk
            (This : in     State;
             Item : in out Term)
@@ -95,17 +136,16 @@ package body Kompsos.Collector is
 
 
     function Do_Unify
-           (Potential   : in     State;
-            Left, Right : in     Term'Class;
-            Extended    :    out State)
+           (Subst       : in out State;
+            Left, Right : in     Term'Class)
         return Boolean
     is
         Real_Left  : Term := Term (Left);
         Real_Right : Term := Term (Right);
     begin
         --  Resolve Variable substitution
-        Walk (Potential, Real_Left);
-        Walk (Potential, Real_Right);
+        Walk (Subst, Real_Left);
+        Walk (Subst, Real_Right);
 
         --  Unify equal Variable/Atom/Null Terms
         if (Real_Left.Kind = Var_Term and then
@@ -116,24 +156,23 @@ package body Kompsos.Collector is
             Real_Left = Real_Right) or else
            (Real_Left.Kind = Null_Term and Real_Right.Kind = Null_Term)
         then
-            Extended := Potential;
             return True;
         end if;
 
         --  Unify Variable and other Terms by introducing a new substitution
         if Real_Left.Kind = Var_Term then
-            Extended := Append (Potential, Real_Left.Var, Real_Right);
+            Insert (Subst, Real_Left.Var, Real_Right);
             return True;
         end if;
         if Real_Right.Kind = Var_Term then
-            Extended := Append (Potential, Real_Right.Var, Real_Left);
+            Insert (Subst, Real_Right.Var, Real_Left);
             return True;
         end if;
 
         --  Unify Pair Terms by unifying each corresponding part
         if Real_Left.Kind = Pair_Term and then Real_Right.Kind = Pair_Term then
-            return Do_Unify (Potential, Real_Left.Left, Real_Right.Left, Extended) and then
-                Do_Unify (Extended, Real_Left.Right, Real_Right.Right, Extended);
+            return Do_Unify (Subst, Real_Left.Left, Real_Right.Left) and then
+                Do_Unify (Subst, Real_Left.Right, Real_Right.Right);
         end if;
 
         --  Otherwise unification fails
@@ -142,402 +181,212 @@ package body Kompsos.Collector is
 
 
 
-    --  Result Collection --
+    --  Interleaved Graph Inversion  --
 
-    function Call_Lazy
-           (This : in Goal;
-            Data : in Lazy_Holders.Holder)
-        return Goal
+    function Null_Join
+           (Left, Right : in Graph_Component_Access)
+        return Graph_Component_Access is
+    begin
+        return (if Left = null then Right else Left);
+    end Null_Join;
+
+
+    procedure Sorted_Insert
+           (Quiver : in out Parent_Arrow_Vectors.Vector;
+            Arrow  : in     Parent_Arrow)
     is
-        Ref : constant Lazy_Holders.Constant_Reference_Type := Data.Constant_Reference;
+        Position : Parent_Arrow_Vectors.Extended_Index := Quiver.Last_Index + 1;
     begin
-        case Ref.Kind is
-        when Zero_Arg =>
-            return Ref.ZFunc (This);
-        when One_Arg  =>
-            return Ref.OFunc (This, Ref.OInput);
-        when Many_Arg =>
-            return Ref.MFunc (This, Term_Array_Holders.Constant_Reference (Ref.MInput));
-        end case;
-    end Call_Lazy;
+        while Position > 1 and then Arrow < Quiver (Position - 1) loop
+            Position := Position - 1;
+        end loop;
+        Quiver.Insert (Position, Arrow);
+    end Sorted_Insert;
 
 
-    procedure Do_Reset
-           (Ptr   : in     Graph_Component_Access;
-            Book  : in out Book_Node_Access;
-            Extra : in out Book_Node_Vectors.Vector) is
+    function Connect_Up_Map
+           (Parent, Child : in Graph_Component_Access;
+            Level         : in Disjuncts_Passed;
+            Choices       : in Disjuncts_Chosen)
+        return Boolean
+    is
+        use type Upwards_Maps.Cursor, Parent_Arrow_Vectors.Vector;
+        Index_Cursor : constant Upwards_Maps.Cursor := Up_Map.Find (Child);
     begin
-        if Ptr = null or Book = null then
-            return;
+        if Index_Cursor = Upwards_Maps.No_Element then
+            Up_Vector.Append ((Level, Parent_Arrow_Vectors.Empty_Vector & (Parent, Choices)));
+            Up_Map.Insert (Child, Up_Vector.Last_Index);
+            return True;
+        else
+            Sorted_Insert
+               (Up_Vector (Upwards_Maps.Element (Index_Cursor)).Parents,
+                (Parent, Choices));
+            return False;
         end if;
+    end Connect_Up_Map;
 
-        --  Delete cache
-        if Book.Cache /= null then
-            for Item of Book.Cache.Data loop
-                Free (Item.Data);
-            end loop;
-            Free (Book.Cache);
-        end if;
 
-        --  Delete all bookkeeping for lower nodes
-        case Book.Data.Kind is
+    procedure Build_Up_Map
+           (Top, Bottom : in     Graph_Component_Access;
+            Level       : in     Disjuncts_Passed;
+            Choices     : in out Disjuncts_Chosen) is
+    begin
+        if Top = null then
+            return;
+        end if;
+        case Top.Kind is
         when Unify_Node =>
-            Do_Reset (Ptr.Uni_Goal.Actual, Book.Next1, Extra);
+            if Connect_Up_Map (Top, Null_Join (Top.Uni_Goal.Actual, Bottom), Level, Choices) then
+                Build_Up_Map (Top.Uni_Goal.Actual, Bottom, Level, Choices);
+            end if;
         when Disjunct_Node =>
-            Do_Reset (Ptr.Dis_Goal1.Actual, Book.Next1, Extra);
-            Do_Reset (Ptr.Dis_Goal2.Actual, Book.Next2, Extra);
+            if Connect_Up_Map (Top, Null_Join (Top.Dis_Goal1.Actual, Bottom), Level + 1, Choices)
+            then
+                Build_Up_Map (Top.Dis_Goal1.Actual, Bottom, Level + 1, Choices);
+            end if;
+            Choices.Append (Level + 1);
+            if Connect_Up_Map (Top, Null_Join (Top.Dis_Goal2.Actual, Bottom), Level + 1, Choices)
+            then
+                Build_Up_Map (Top.Dis_Goal2.Actual, Bottom, Level + 1, Choices);
+            end if;
+            Choices.Delete_Last;
         when Conjunct_Node =>
-            Do_Reset (Ptr.Con_Goal.Actual, Book.Next1, Extra);
-            if Book.Data.Con_Part /= null then
-                Reset (Book.Data.Con_Part.Graph.Actual, Book.Next2);
-                Free (Book.Data.Con_Part);
+            if Connect_Up_Map (Top, Null_Join (Top.Con_Goal.Actual, Bottom), Level, Choices) then
+                Build_Up_Map (Top.Con_Goal.Actual, Bottom, Level, Choices);
             end if;
-            Free (Book.Data.Con_Base);
-        when Recurse_Node =>
-            Do_Reset (Ptr.Rec_Goal.Actual, Book.Next1, Extra);
         end case;
-
-        --  Set aside common nodes to be deleted later
-        if Ptr.Counter > 1 then
-            if not Extra.Contains (Book) then
-                Extra.Append (Book);
-            end if;
-        else
-            Free (Book);
-        end if;
-    end Do_Reset;
+    end Build_Up_Map;
 
 
-    procedure Reset
-           (Ptr  : in     Graph_Component_Access;
-            Book : in out Book_Node_Access)
-    is
-        Extra : Book_Node_Vectors.Vector;
-    begin
-        Do_Reset (Ptr, Book, Extra);
-
-        --  Handle common nodes
-        for Item of Extra loop
-            --  Ensure that Book doesn't end up dangling
-            if Item = Book then
-                Free (Book);
-            else
-                Free (Item);
-            end if;
-        end loop;
-    end Reset;
 
+    --  Conjunct Expansion  --
 
-    function New_Book_Factory
-           (Kind : in Node_Kind)
-        return Book_Node_Access is
+    function Call_Lazy
+           (This : in Goal;
+            Data : in Lazy_Data)
+        return Goal is
     begin
-        --  This is needed because Ada does not allow declaring an object using
-        --  a discriminant that is not statically known.
-        case Kind is
-        when Unify_Node =>
-            return new Book_Node'(Data => (Kind => Unify_Node,    others => <>), others => <>);
-        when Disjunct_Node =>
-            return new Book_Node'(Data => (Kind => Disjunct_Node, others => <>), others => <>);
-        when Conjunct_Node =>
-            return new Book_Node'(Data => (Kind => Conjunct_Node, others => <>), others => <>);
-        when Recurse_Node =>
-            return new Book_Node'(Data => (Kind => Recurse_Node,  others => <>), others => <>);
+        case Data.Kind is
+        when Zero_Arg =>
+            return Data.ZFunc (This);
+        when One_Arg  =>
+            return Data.OFunc (This, Data.OInput);
+        when Many_Arg =>
+            return Data.MFunc (This, Data.MInput.all);
         end case;
-    end New_Book_Factory;
+    end Call_Lazy;
 
 
-    function New_Book
-           (Ptr : in Graph_Component_Access)
-        return Book_Node_Access is
+    procedure Expand_Conjunct
+           (Node : in Graph_Component_Access)
+    is
+        Old_Choices : Disjuncts_Chosen :=
+            Up_Vector (Upwards_Maps.Element (Local_Cursor)).Parents (Next_Pick).Order;
     begin
-        pragma Assert (Ptr.Counter /= 0);
-        if Ptr.Counter = 1 or Ptr = Relation.Graph.Actual then
-            return New_Book_Factory (Ptr.Kind);
-        else
-            return Acc : constant Book_Node_Access := New_Book_Factory (Ptr.Kind) do
-                Loose_Books.Append ((1, Ptr, Acc));
-            end return;
-        end if;
-    end New_Book;
-
-
-    function Connect_Loose
-           (Ptr : in Graph_Component_Access)
-        return Book_Node_Access is
+        Up_Vector (Upwards_Maps.Element (Local_Cursor)).Parents.Delete (Next_Pick);
+        Conjunct_Goals.Append (new Goal'(
+            Call_Lazy
+               ((Graph    => (Ada.Finalization.Controlled with Actual => null),
+                 Next_Var => Global_Var),
+                Node.Con_Data.all)));
+        Global_Var := Conjunct_Goals.Last_Element.Next_Var;
+        declare
+            Depth : constant Disjuncts_Passed :=
+                Up_Vector (Upwards_Maps.Element (Local_Cursor)).Depth;
+        begin
+            Build_Up_Map (Conjunct_Goals.Last_Element.Graph.Actual, Location, Depth, Old_Choices);
+        end;
+        Up_Map.Insert (Conjunct_Goals.Last_Element.Graph.Actual, Up_Map.Element (Node));
+    end Expand_Conjunct;
+
+
+
+    --  Upwards Depth First Search  --
+
+    function Choose_Another_Way
+        return Boolean
+    is
+        Marker : Natural := Walk_Trail.Last_Index;
+        Crumb : Breadcrumb;
     begin
-        for Index in Loose_Books.First_Index .. Loose_Books.Last_Index loop
-            if Loose_Books.Element (Index).Ptr = Ptr then
-                return Acc : constant Book_Node_Access := Loose_Books.Element (Index).Book do
-                    Loose_Books (Index).Used := Loose_Books (Index).Used + 1;
-                    if Loose_Books.Element (Index).Used >= Ptr.Counter then
-                        Loose_Books.Delete (Index);
-                    end if;
-                end return;
+        while Marker /= Breadcrumb_Vectors.No_Index loop
+            Crumb := Walk_Trail (Marker);
+            Location := Crumb.Choice_Node;
+            Local_Cursor := Up_Map.Find (Location);
+            if Up_Vector (Upwards_Maps.Element (Local_Cursor)).Parents.Last_Index >=
+                Crumb.Option + 1
+            then
+                Next_Pick := Crumb.Option + 1;
+                Truncate (Result, Crumb.State_Size);
+                Walk_Trail.Set_Length (Ada.Containers.Count_Type (Marker - 1));
+                return True;
+            else
+                Marker := Marker - 1;
             end if;
         end loop;
-        return null;
-    end Connect_Loose;
+        return False;
+    end Choose_Another_Way;
 
 
-    function Do_Get_Next
-           (Ptr    : in     Graph_Component_Access;
-            Book   : in out Book_Node_Access;
-            Base   : in     State;
-            Index  : in     Long_Positive;
-            Result :    out State)
-        return Boolean is
+    procedure Walk_Graph is
+        use type Upwards_Maps.Cursor;
+        Ptr : Graph_Component_Access;
     begin
-        case Ptr.Kind is
-        when Unify_Node =>
-            if Book = null then
-                Book := New_Book (Ptr);
-            end if;
-            while Get_Next
-               (Ptr.Uni_Goal'Unchecked_Access,
-                Book.Next1, Base,
-                Index + Book.Data.Uni_Offset,
-                Result)
-            loop
-                if Do_Unify (Result, Ptr.Uni_Term1, Ptr.Uni_Term2, Result) then
-                    return True;
-                else
-                    Book.Data.Uni_Offset := Book.Data.Uni_Offset + 1;
-                end if;
-            end loop;
-            return False;
-
-        when Disjunct_Node =>
-            if Book = null then
-                Book := New_Book (Ptr);
-            end if;
-            if Book.Data.Dis_Gone1 then
-                if Book.Data.Dis_Gone2 then
-                    return False;
-                elsif Get_Next
-                   (Ptr.Dis_Goal2'Unchecked_Access,
-                    Book.Next2, Base,
-                    Book.Data.Dis_Next2,
-                    Result)
-                then
-                    Book.Data.Dis_Next2 := Book.Data.Dis_Next2 + 1;
-                    return True;
-                else
-                    Book.Data.Dis_Gone2 := True;
-                    return False;
+        loop
+            if Location = null or else Location.Kind /= Unify_Node or else
+                Do_Unify (Result, Location.Uni_Term1, Location.Uni_Term2)
+            then
+                if Local_Cursor = Upwards_Maps.No_Element then
+                    State_Valid := True;
+                    return;
                 end if;
-            elsif Book.Data.Dis_Gone2 then
-                if Get_Next
-                   (Ptr.Dis_Goal1'Unchecked_Access,
-                    Book.Next1, Base,
-                    Book.Data.Dis_Next1,
-                    Result)
-                then
-                    Book.Data.Dis_Next1 := Book.Data.Dis_Next1 + 1;
-                    return True;
-                else
-                    Book.Data.Dis_Gone1 := True;
-                    return False;
+                Ptr := Up_Vector (Upwards_Maps.Element (Local_Cursor)).Parents (Next_Pick).Node;
+                if Ptr.Kind = Conjunct_Node then
+                    Expand_Conjunct (Ptr);
                 end if;
-            elsif Book.Data.Dis_Flag then
-                if Get_Next
-                   (Ptr.Dis_Goal1'Unchecked_Access,
-                    Book.Next1, Base,
-                    Book.Data.Dis_Next1,
-                    Result)
-                then
-                    Book.Data.Dis_Next1 := Book.Data.Dis_Next1 + 1;
-                    Book.Data.Dis_Flag := not Book.Data.Dis_Flag;
-                    return True;
-                else
-                    Book.Data.Dis_Gone1 := True;
-                    if Get_Next
-                       (Ptr.Dis_Goal2'Unchecked_Access,
-                        Book.Next2, Base,
-                        Book.Data.Dis_Next2,
-                        Result)
-                    then
-                        Book.Data.Dis_Next2 := Book.Data.Dis_Next2 + 1;
-                        return True;
-                    else
-                        Book.Data.Dis_Gone2 := True;
-                        return False;
-                    end if;
+                if Up_Vector (Upwards_Maps.Element (Local_Cursor)).Parents.Last_Index > 1 then
+                    Walk_Trail.Append ((Location, Next_Pick, Result.Binds.Last_Index));
                 end if;
+                Location := Up_Vector
+                    (Upwards_Maps.Element (Local_Cursor)).Parents (Next_Pick).Node;
+                Local_Cursor := Up_Map.Find (Location);
+                Next_Pick := 1;
             else
-                if Get_Next
-                   (Ptr.Dis_Goal2'Unchecked_Access,
-                    Book.Next2, Base,
-                    Book.Data.Dis_Next2,
-                    Result)
-                then
-                    Book.Data.Dis_Next2 := Book.Data.Dis_Next2 + 1;
-                    Book.Data.Dis_Flag := not Book.Data.Dis_Flag;
-                    return True;
-                else
-                    Book.Data.Dis_Gone2 := True;
-                    if Get_Next
-                       (Ptr.Dis_Goal1'Unchecked_Access,
-                        Book.Next1, Base,
-                        Book.Data.Dis_Next1,
-                        Result)
-                    then
-                        Book.Data.Dis_Next1 := Book.Data.Dis_Next1 + 1;
-                        return True;
-                    else
-                        Book.Data.Dis_Gone1 := True;
-                        return False;
-                    end if;
-                end if;
-            end if;
-
-        when Conjunct_Node =>
-            if Book = null then
-                Book := New_Book (Ptr);
-                if not Get_Next (Ptr.Con_Goal'Unchecked_Access, Book.Next1, Base, 1, Result) then
-                    Book.Data.Con_Gone := True;
-                else
-                    Book.Data.Con_Base := new State'(Result);
-                    Book.Data.Con_Part := new Goal'(
-                        Call_Lazy
-                           ((Graph    => (Ada.Finalization.Controlled with Actual => null),
-                             Next_Var => Global_Var),
-                            Ptr.Con_Data));
-                    Global_Var := Book.Data.Con_Part.Next_Var;
-                end if;
-            end if;
-            if Book.Data.Con_Gone then
-                return False;
-            end if;
-            while not Get_Next
-               (Constant_Graph_Access'(Book.Data.Con_Part.Graph'Access),
-                Book.Next2, Book.Data.Con_Base.all,
-                Book.Data.Con_Next,
-                Result)
-            loop
-                Reset (Book.Data.Con_Part.Graph.Actual, Book.Next2);
-                Book.Data.Con_From := Book.Data.Con_From + 1;
-                if Get_Next
-                   (Ptr.Con_Goal'Unchecked_Access,
-                    Book.Next1, Base,
-                    Book.Data.Con_From,
-                    Result)
-                then
-                    Book.Data.Con_Base.all := Result;
-                    Book.Data.Con_Next := 1;
-                else
-                    Book.Data.Con_Gone := True;
-                    Free (Book.Data.Con_Part);
-                    Free (Book.Data.Con_Base);
-                    return False;
+                if not Choose_Another_Way then
+                    State_Valid := False;
+                    Exhausted := True;
+                    return;
                 end if;
-            end loop;
-            Book.Data.Con_Next := Book.Data.Con_Next + 1;
-            return True;
-
-        when Recurse_Node =>
-            if Book = null then
-                Book := New_Book (Ptr);
             end if;
-            if Book.Next1 = null then
-                Book.Next1 := Connect_Loose (Ptr.Rec_Goal.Actual);
-            end if;
-            if Ptr.Rec_Goal.Actual /= null then
-                --  Reach forwards to ensure the next node has cached results
-                --  even if it normally wouldn't have and that those results
-                --  are not discarded, so we can loop through them as needed.
-                if Book.Next1 = null then
-                    Book.Next1 := New_Book (Ptr.Rec_Goal.Actual);
-                    Book.Next1.Cache := new Cache_Entry'(True, State_Vectors.Empty_Vector);
-                elsif Book.Next1.Cache = null then
-                    Book.Next1.Cache := new Cache_Entry'(True, State_Vectors.Empty_Vector);
-                else
-                    Book.Next1.Cache.Keep := True;
-                end if;
-            end if;
-            if Book.Data.Rec_Gone then
-                return False;
-            end if;
-            while not Get_Next
-               (Ptr.Rec_Goal'Unchecked_Access,
-                Book.Next1, Base,
-                Book.Data.Rec_Next,
-                Result)
-            loop
-                if Book.Data.Rec_Next = 1 then
-                    Book.Data.Rec_Gone := True;
-                    return False;
-                else
-                    Book.Data.Rec_Next := 1;
-                end if;
-            end loop;
-            Book.Data.Rec_Next := Book.Data.Rec_Next + 1;
-            return True;
-        end case;
-    end Do_Get_Next;
+        end loop;
+    end Walk_Graph;
 
 
-    function Get_Next
-           (Ptr    : in     Constant_Graph_Access;
-            Book   : in out Book_Node_Access;
-            Base   : in     State;
-            Index  : in     Long_Positive;
-            Result :    out State)
-        return Boolean is
+    procedure Continue_Walk is
     begin
-        if Ptr = null then
-            return False;
-        end if;
-
-        --  Lowest node in the graph always returns the Base State
-        if Ptr.Actual = null then
-            if Index = 1 then
-                Result := Base;
-                Use_New_Node := True;
-                return True;
-            else
-                return False;
-            end if;
+        if Choose_Another_Way then
+            Walk_Graph;
+        else
+            State_Valid := False;
+            Exhausted := True;
         end if;
+    end Continue_Walk;
 
-        --  Attempt to connect common bookkeeping branches
-        if Book = null then
-            Book := Connect_Loose (Ptr.Actual);
-        end if;
 
-        --  If cached results exist, use those
-        if Book /= null and then Book.Cache /= null and then
-            Index <= Book.Cache.Data.Last_Index
-        then
-            Result := Book.Cache.Data (Index).Data.all;
-            Book.Cache.Data (Index).Used := Book.Cache.Data (Index).Used + 1;
-            if not Book.Cache.Keep and then Book.Cache.Data (Index).Used >= Ptr.Actual.Counter then
-                Free (Book.Cache.Data (Index).Data);
-            end if;
-            Use_New_Node := True;
-            return True;
+    procedure Start_Walk is
+        use type Upwards_Maps.Cursor;
+    begin
+        Location := null;
+        Local_Cursor := Up_Map.Find (Location);
+        if Local_Cursor = Upwards_Maps.No_Element then
+            State_Valid := True;
+            Exhausted := True;
+        else
+            Do_Walk := Continue_Walk'Access;
+            Next_Pick := 1;
+            Walk_Graph;
         end if;
-
-        --  Otherwise, actual result calculation
-        return Found : constant Boolean :=
-            Do_Get_Next (Ptr.Actual, Book, Base, Index, Result)
-        do
-            if Found then
-                --  Cache results as needed
-                if Ptr.Actual.Counter > 1 and then
-                    Ptr.Actual /= Relation.Graph.Actual and then
-                    Book.Cache = null
-                then
-                    Book.Cache := new Cache_Entry'(False, State_Vectors.Empty_Vector);
-                end if;
-                if Book.Cache /= null then
-                    pragma Assert (Index = Book.Cache.Data.Last_Index + 1);
-                    Book.Cache.Data.Append ((1, new State'(Result)));
-                    Use_New_Node := True;
-                end if;
-            end if;
-        end return;
-    end Get_Next;
+    end Start_Walk;
 
 
 
@@ -547,21 +396,14 @@ package body Kompsos.Collector is
     -----------------------
 
     function Has_Next
-        return Boolean
-    is
-        Ptr : constant Constant_Graph_Access := Relation.Graph'Access;
+        return Boolean is
     begin
         if State_Valid then
             return True;
         elsif Exhausted then
             return False;
         else
-            State_Valid := Get_Next (Ptr, Book_Root, Within, Next_Index, Next_State);
-            if not State_Valid then
-                Exhausted := True;
-            else
-                Next_Index := Next_Index + 1;
-            end if;
+            Do_Walk.all;
             return State_Valid;
         end if;
     end Has_Next;
@@ -572,7 +414,7 @@ package body Kompsos.Collector is
     begin
         if Has_Next then
             State_Valid := False;
-            return Next_State;
+            return Result;
         else
             raise State_Not_Found_Error;
         end if;
@@ -585,22 +427,24 @@ package body Kompsos.Collector is
     begin
         if Has_Next then
             State_Valid := False;
-            return Next_State;
+            return Result;
         else
             return Default;
         end if;
     end Next;
 
 
-    procedure Reset is
-    begin
-        Reset (Relation.Graph.Actual, Book_Root);
-        Next_Index  := 1;
-        State_Valid := False;
-        Exhausted   := False;
-    end Reset;
 
 
+begin
+
+    declare
+        Temp : Positive_Vectors.Vector := Positive_Vectors.Empty_Vector;
+    begin
+        Build_Up_Map (Relation.Graph.Actual, null, 0, Temp);
+    end;
+    Do_Walk := Start_Walk'Access;
+
 end Kompsos.Collector;