Evaluation algorithm changed to inverted interleaved depth first search

5 files changed, 421 insertions, 671 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;
 
 
diff --git a/src/kompsos-collector.ads b/src/kompsos-collector.ads
index ac451c2..da3c592 100644
--- a/src/kompsos-collector.ads
+++ b/src/kompsos-collector.ads
@@ -8,6 +8,7 @@
 
 private with
 
+    Ada.Containers.Hashed_Maps,
     Ada.Containers.Vectors,
     Ada.Finalization;
 
@@ -31,108 +32,80 @@ package Kompsos.Collector is
            (Default : in State)
         return State;
 
-    procedure Reset;
-
 
 private
 
 
-    type Goal_Access is access all Goal;
-    type Constant_Goal_Access is access constant Goal;
-
-    type Graph_Access is access all Goal_Graph;
-    type Constant_Graph_Access is access constant Goal_Graph;
-
-
-
-    type Eval_Data (Kind : Node_Kind := Unify_Node) is record
-        case Kind is
-        when Unify_Node =>
-            Uni_Offset : Long_Natural  := 0;
-        when Disjunct_Node =>
-            Dis_Flag   : Boolean       := True;
-            Dis_Next1  : Long_Positive := 1;
-            Dis_Next2  : Long_Positive := 1;
-            Dis_Gone1  : Boolean       := False;
-            Dis_Gone2  : Boolean       := False;
-        when Conjunct_Node =>
-            Con_From   : Long_Positive := 1;
-            Con_Base   : State_Access  := null;
-            Con_Part   : Goal_Access   := null;
-            Con_Next   : Long_Positive := 1;
-            Con_Gone   : Boolean       := False;
-        when Recurse_Node =>
-            Rec_Next   : Long_Positive := 1;
-            Rec_Gone   : Boolean       := False;
-        end case;
-    end record;
+    --  Interleaved Graph Inversion  --
 
+    package Positive_Vectors is new Ada.Containers.Vectors
+       (Index_Type   => Positive,
+        Element_Type => Positive);
 
+    subtype Disjuncts_Chosen is Positive_Vectors.Vector;
 
-    type Cached_State is record
-        Used : Positive     := 1;
-        Data : State_Access := null;
-    end record;
-
-    package State_Vectors is new Ada.Containers.Vectors
-       (Index_Type   => Long_Positive,
-        Element_Type => Cached_State);
+    function "<"
+           (Left, Right : in Disjuncts_Chosen)
+        return Boolean;
 
-    type Cache_Entry is record
-        Keep : Boolean              := False;
-        Data : State_Vectors.Vector := State_Vectors.Empty_Vector;
+    type Parent_Arrow is record
+        Node  : Graph_Component_Access;
+        Order : Disjuncts_Chosen;
     end record;
 
-    type Cache_Entry_Access is access Cache_Entry;
-
-
+    function "<"
+           (Left, Right : in Parent_Arrow)
+        return Boolean;
 
-    type Book_Node;
+    package Parent_Arrow_Vectors is new Ada.Containers.Vectors
+       (Index_Type   => Positive,
+        Element_Type => Parent_Arrow);
 
-    type Book_Node_Access is access Book_Node;
+    subtype Disjuncts_Passed is Natural;
 
-    type Book_Node is record
-        Data  : Eval_Data;
-        Cache : Cache_Entry_Access := null;
-        Next1 : Book_Node_Access   := null;
-        Next2 : Book_Node_Access   := null;
+    type Node_Upwards is record
+        Depth   : Disjuncts_Passed;
+        Parents : Parent_Arrow_Vectors.Vector;
     end record;
 
+    package Upwards_Vectors is new Ada.Containers.Vectors
+       (Index_Type   => Positive,
+        Element_Type => Node_Upwards);
 
+    function Graph_Component_Access_Hash
+           (Key : in Graph_Component_Access)
+        return Ada.Containers.Hash_Type;
 
-    --  Used to keep track of and connect up bookkeeping nodes corresponding to
-    --  graph nodes with more than one parent, so as to avoid ending up with an
-    --  exponential tree instead of the desired directed acyclic graph.
+    package Upwards_Maps is new Ada.Containers.Hashed_Maps
+       (Key_Type        => Graph_Component_Access,
+        Element_Type    => Positive,
+        Hash            => Graph_Component_Access_Hash,
+        Equivalent_Keys => "=");
 
-    type Loose_Book is record
-        Used : Positive               := 1;
-        Ptr  : Graph_Component_Access := null;
-        Book : Book_Node_Access       := null;
-    end record;
 
-    package Loose_Book_Vectors is new Ada.Containers.Vectors
-       (Index_Type   => Long_Positive,
-        Element_Type => Loose_Book);
+    --  Conjunct Expansion  --
 
-    package Book_Node_Vectors is new Ada.Containers.Vectors
-       (Index_Type   => Long_Positive,
-        Element_Type => Book_Node_Access);
+    type Goal_Access is access all Goal;
 
+    package Goal_Access_Vectors is new Ada.Containers.Vectors
+       (Index_Type   => Positive,
+        Element_Type => Goal_Access);
 
 
-    procedure Reset
-           (Ptr  : in     Graph_Component_Access;
-            Book : in out Book_Node_Access);
+    --  Upwards Depth First Search  --
 
-    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;
+    type Breadcrumb is record
+        Choice_Node : Graph_Component_Access;
+        Option      : Positive;
+        State_Size  : Long_Natural;
+    end record;
+
+    package Breadcrumb_Vectors is new Ada.Containers.Vectors
+       (Index_Type   => Positive,
+        Element_Type => Breadcrumb);
 
 
+    --  Cleanup  --
 
     type Collector_Final_Controller is new Ada.Finalization.Limited_Controlled with null record;
 
diff --git a/src/kompsos-pretty_print.adb b/src/kompsos-pretty_print.adb
index 2befe6d..328f467 100644
--- a/src/kompsos-pretty_print.adb
+++ b/src/kompsos-pretty_print.adb
@@ -112,21 +112,14 @@ package body Kompsos.Pretty_Print is
     is
         Result : SU.Unbounded_String;
     begin
-        if Item.Ctrl.Actual = null then
+        if Item.Binds.Is_Empty then
             SU.Append (Result, Latin.HT & "N/A" & Latin.LF);
         else
-            declare
-                Marker : State_Component_Access := Item.Ctrl.Actual;
-            begin
-                while Marker /= null loop
-                    for Index in Valid_Count range Valid_Count'First .. Marker.Valid loop
-                        SU.Append (Result, Latin.HT &
-                            Image (Marker.Data (Index).Key) & " => " &
-                            Image (Marker.Data (Index).Value) & Latin.LF);
-                    end loop;
-                    Marker := Marker.Next.Ctrl.Actual;
-                end loop;
-            end;
+            for Bind of Item.Binds loop
+                SU.Append (Result, Latin.HT &
+                    Image (Bind.Key) & " => " &
+                    Image (Bind.Value) & Latin.LF);
+            end loop;
         end if;
         return SU.To_String (Result);
     end Image;
@@ -224,15 +217,6 @@ package body Kompsos.Pretty_Print is
                     "n" & Image (Nodes.Element (This.Actual)) & " -> " &
                     "n" & Image (Nodes.Element (This.Actual.Con_Goal.Actual)) & ";" & Latin.LF);
             end if;
-        when Recurse_Node =>
-            SU.Append (Result, Latin.HT &
-                "n" & Image (Nodes.Element (This.Actual)) & " [label=""recurse""];" & Latin.LF);
-            Do_Structure_DOT (This.Actual.Rec_Goal, Nodes, Next, Result);
-            if Nodes.Contains (This.Actual.Rec_Goal.Actual) then
-                SU.Append (Result, Latin.HT &
-                    "n" & Image (Nodes.Element (This.Actual)) & " -> " &
-                    "n" & Image (Nodes.Element (This.Actual.Rec_Goal.Actual)) & ";" & Latin.LF);
-            end if;
         end case;
     end Do_Structure_DOT;
 
diff --git a/src/kompsos.adb b/src/kompsos.adb
index 4513706..b12e1fb 100644
--- a/src/kompsos.adb
+++ b/src/kompsos.adb
@@ -53,43 +53,11 @@ package body Kompsos is
 
 
 
-    --  States  --
-
-    procedure Free is new Ada.Unchecked_Deallocation (State_Component, State_Component_Access);
-
-
-    procedure Initialize
-           (This : in out State_Control) is
-    begin
-        This.Actual := null;
-    end Initialize;
-
-
-    procedure Adjust
-           (This : in out State_Control) is
-    begin
-        if This.Actual /= null then
-            This.Actual.Counter := This.Actual.Counter + 1;
-        end if;
-    end Adjust;
-
-
-    procedure Finalize
-           (This : in out State_Control) is
-    begin
-        if This.Actual /= null then
-            This.Actual.Counter := This.Actual.Counter - 1;
-            if This.Actual.Counter = 0 then
-                Free (This.Actual);
-            end if;
-        end if;
-    end Finalize;
-
-
-
     --  Goal Graphs  --
 
     procedure Free is new Ada.Unchecked_Deallocation (Graph_Component, Graph_Component_Access);
+    procedure Free is new Ada.Unchecked_Deallocation (Term_Array, Term_Array_Access);
+    procedure Free is new Ada.Unchecked_Deallocation (Lazy_Data, Lazy_Data_Access);
 
 
     procedure Initialize
@@ -114,6 +82,14 @@ package body Kompsos is
         if This.Actual /= null then
             This.Actual.Counter := This.Actual.Counter - 1;
             if This.Actual.Counter = 0 then
+                if This.Actual.Kind = Conjunct_Node then
+                    if This.Actual.Con_Data /= null and then
+                        This.Actual.Con_Data.Kind = Many_Arg
+                    then
+                        Free (This.Actual.Con_Data.MInput);
+                    end if;
+                    Free (This.Actual.Con_Data);
+                end if;
                 Free (This.Actual);
             end if;
         end if;
@@ -243,27 +219,54 @@ package body Kompsos is
 
     --  States  --
 
+    function Variable_Index_Hash
+           (Key : in Variable)
+        return Ada.Containers.Hash_Type is
+    begin
+        return Ada.Containers.Hash_Type (Key mod Ada.Containers.Hash_Type'Modulus);
+    end Variable_Index_Hash;
+
+
+    procedure Insert
+           (This  : in out State;
+            Key   : in     Variable;
+            Value : in     Term'Class) is
+    begin
+        This.Binds.Append ((Key, Term (Value)));
+        This.Refs.Insert (Key, This.Binds.Last_Index);
+    end Insert;
+
+
     function Lookup
            (This  : in     State;
             Key   : in     Variable;
             Value :    out Term'Class)
         return Boolean
     is
-        Ptr : State_Component_Access := This.Ctrl.Actual;
+        use type Variable_Index_Maps.Cursor;
+        Result : constant Variable_Index_Maps.Cursor := This.Refs.Find (Key);
     begin
-        while Ptr /= null loop
-            for Index in Valid_Count range Valid_Count'First .. Ptr.Valid loop
-                if Ptr.Data (Index).Key = Key then
-                    Value := Term'Class (Ptr.Data (Index).Value);
-                    return True;
-                end if;
-            end loop;
-            Ptr := Ptr.Next.Ctrl.Actual;
-        end loop;
+        if Result /= Variable_Index_Maps.No_Element then
+            Value := This.Binds (Variable_Index_Maps.Element (Result)).Value;
+            return True;
+        end if;
         return False;
     end Lookup;
 
 
+    procedure Truncate
+           (This   : in out State;
+            Length : in     Long_Natural) is
+    begin
+        if This.Binds.Last_Index > Length then
+            for Index in Long_Positive range Length + 1 .. This.Binds.Last_Index loop
+                This.Refs.Exclude (This.Binds (Index).Key);
+            end loop;
+            This.Binds.Set_Length (Ada.Containers.Count_Type (Length));
+        end if;
+    end Truncate;
+
+
 
 
     -------------------
@@ -413,7 +416,7 @@ package body Kompsos is
                    (Kind     => Conjunct_Node,
                     Counter  => 1,
                     Con_Goal => This.Graph,
-                    Con_Data => Lazy_Holders.To_Holder ((Kind => Zero_Arg, ZFunc => Func))))),
+                    Con_Data => new Lazy_Data'((Kind => Zero_Arg, ZFunc => Func))))),
             Next_Var => This.Next_Var);
     end Conjunct;
 
@@ -438,10 +441,10 @@ package body Kompsos is
                    (Kind     => Conjunct_Node,
                     Counter  => 1,
                     Con_Goal => This.Graph,
-                    Con_Data => Lazy_Holders.To_Holder
-                       ((Kind   => One_Arg,
-                         OFunc  => Func,
-                         OInput => Term (Input)))))),
+                    Con_Data => new Lazy_Data'(
+                       (Kind   => One_Arg,
+                        OFunc  => Func,
+                        OInput => Term (Input)))))),
             Next_Var => This.Next_Var);
     end Conjunct;
 
@@ -467,10 +470,10 @@ package body Kompsos is
                    (Kind     => Conjunct_Node,
                     Counter  => 1,
                     Con_Goal => This.Graph,
-                    Con_Data => Lazy_Holders.To_Holder
-                       ((Kind   => Many_Arg,
-                         MFunc  => Func,
-                         MInput => Term_Array_Holders.To_Holder (Inputs)))))),
+                    Con_Data => new Lazy_Data'(
+                       (Kind   => Many_Arg,
+                        MFunc  => Func,
+                        MInput => new Term_Array'(Inputs)))))),
             Next_Var => This.Next_Var);
     end Conjunct;
 
@@ -490,30 +493,6 @@ package body Kompsos is
     --  Auxiliary Helpers  --
     -------------------------
 
-    --  Infinite State Loops  --
-
-    function Recurse
-           (This : in Goal)
-        return Goal is
-    begin
-        return Result : constant Goal :=
-           (Graph    => (Ada.Finalization.Controlled with
-                Actual => new Graph_Component'(
-                   (Kind     => Recurse_Node,
-                    Counter  => 1,
-                    Rec_Goal => This.Graph))),
-            Next_Var => This.Next_Var);
-    end Recurse;
-
-
-    procedure Recurse
-           (This : in out Goal) is
-    begin
-        This := This.Recurse;
-    end Recurse;
-
-
-
     --  Evaluation  --
 
     function Run
@@ -599,24 +578,22 @@ package body Kompsos is
            (Subst : in State)
         return Term is
     begin
-        if Subst.Ctrl.Actual = null then
+        if Subst.Binds.Is_Empty then
             return Empty_Term;
         end if;
         declare
-            Min_Pos : State_Component_Access := Subst.Ctrl.Actual;
-            Min_Ind : Valid_Count            := Valid_Count'First;
-            Marker  : State_Component_Access := Min_Pos;
+            Min_Index : Long_Positive := 1;
+            Min_Var   : Variable      := Subst.Binds.First_Element.Key;
         begin
-            while Marker /= null loop
-                for Index in Valid_Count range Valid_Count'First .. Marker.Valid loop
-                    if Marker.Data (Index).Key < Min_Pos.Data (Min_Ind).Key then
-                        Min_Pos := Marker;
-                        Min_Ind := Index;
-                    end if;
-                end loop;
-                Marker := Marker.Next.Ctrl.Actual;
+            for Index in Long_Positive range
+                Subst.Binds.First_Index + 1 .. Subst.Binds.Last_Index
+            loop
+                if Subst.Binds (Index).Key < Min_Var then
+                    Min_Index := Index;
+                    Min_Var   := Subst.Binds (Index).Key;
+                end if;
             end loop;
-            return Min_Pos.Data (Min_Ind).Value.Resolve (Subst);
+            return Subst.Binds (Min_Index).Value.Resolve (Subst);
         end;
     end Resolve_First;
 
diff --git a/src/kompsos.ads b/src/kompsos.ads
index dc9341f..ab50a08 100644
--- a/src/kompsos.ads
+++ b/src/kompsos.ads
@@ -8,7 +8,8 @@
 
 private with
 
-    Ada.Containers.Indefinite_Holders,
+    Ada.Containers.Hashed_Maps,
+    Ada.Containers.Vectors,
     Ada.Finalization;
 
 
@@ -212,16 +213,6 @@ package Kompsos is
     --  Auxiliary Helpers  --
     -------------------------
 
-    --  Infinite State Loops  --
-
-    function Recurse
-           (This : in Goal)
-        return Goal;
-
-    procedure Recurse
-           (This : in out Goal);
-
-
     --  Evaluation  --
 
     function Run
@@ -393,16 +384,8 @@ package Kompsos is
     with Pre => Inputs'Length = 3;
 
 
-    --  anyo  --
-    --  Skipped due to Recurse doing the same thing
-
-
-    --  nevero  --
-    --  Skipped since it just creates a failed Goal
-
-
-    --  alwayso  --
-    --  Skipped due to Recurse doing the same thing
+    --  anyo, nevero, alwayso  --
+    --  Skipped since these seem to be artifacts of conde, which isn't used here
 
 
 private
@@ -411,7 +394,7 @@ private
     --  Variables  --
     --  Around 2^31 possible Variables per Goal should be enough for anybody, right?
     subtype Long_Natural  is Long_Integer range 0 .. Long_Integer'Last;
-    subtype Long_Positive is Long_Integer range 1 .. Long_Integer'Last;
+    subtype Long_Positive is Long_Integer range 1 .. Long_Natural'Last;
 
     type Variable is new Long_Natural;
 
@@ -460,7 +443,7 @@ private
 
     Empty_Term : constant Term := (Ada.Finalization.Controlled with Actual => null);
 
-    package Term_Array_Holders is new Ada.Containers.Indefinite_Holders (Term_Array);
+    type Term_Array_Access is access Term_Array;
 
 
     --  States  --
@@ -470,40 +453,29 @@ private
         Value : Term;
     end record;
 
-    type Binding_Array is array (Positive range <>) of Binding;
-
-    --  Values of 2, 3, 4 here are honestly fairly similar, but of those, 4 seems to work best
-    Unroll_Max : constant Integer := 4;
-
-    subtype Valid_Count is Integer range 1 .. Unroll_Max;
-
-    type State_Component is limited record
-        Counter : Natural;
-        Valid   : Valid_Count;
-        Data    : Binding_Array (Valid_Count'Range);
-        Next    : State;
-    end record;
-
-    type State_Component_Access is access State_Component;
-
-    type State_Control is new Ada.Finalization.Controlled with record
-        Actual : State_Component_Access := null;
-    end record;
-
-    overriding procedure Initialize
-           (This : in out State_Control);
+    package Binding_Vectors is new Ada.Containers.Vectors
+       (Index_Type   => Long_Positive,
+        Element_Type => Binding);
 
-    overriding procedure Adjust
-           (This : in out State_Control);
+    function Variable_Index_Hash
+           (Key : in Variable)
+        return Ada.Containers.Hash_Type;
 
-    overriding procedure Finalize
-           (This : in out State_Control);
+    package Variable_Index_Maps is new Ada.Containers.Hashed_Maps
+       (Key_Type        => Variable,
+        Element_Type    => Long_Positive,
+        Hash            => Variable_Index_Hash,
+        Equivalent_Keys => "=");
 
     type State is record
-        Ctrl : State_Control := (Ada.Finalization.Controlled with Actual => null);
+        Binds : Binding_Vectors.Vector;
+        Refs  : Variable_Index_Maps.Map;
     end record;
 
-    type State_Access is access State;
+    procedure Insert
+           (This  : in out State;
+            Key   : in     Variable;
+            Value : in     Term'Class);
 
     function Lookup
            (This  : in     State;
@@ -511,7 +483,13 @@ private
             Value :    out Term'Class)
         return Boolean;
 
-    Empty_State : constant State := (Ctrl => (Ada.Finalization.Controlled with Actual => null));
+    procedure Truncate
+           (This   : in out State;
+            Length : in     Long_Natural);
+
+    Empty_State : constant State :=
+       (Binds => Binding_Vectors.Empty_Vector,
+        Refs  => Variable_Index_Maps.Empty_Map);
 
 
     --  Goals  --
@@ -544,17 +522,13 @@ private
             OInput : Term;
         when Many_Arg =>
             MFunc  : Junction_Many_Func;
-            MInput : Term_Array_Holders.Holder;
+            MInput : Term_Array_Access;
         end case;
     end record;
 
-    package Lazy_Holders is new Ada.Containers.Indefinite_Holders (Lazy_Data);
+    type Lazy_Data_Access is access Lazy_Data;
 
-    type Node_Kind is
-       (Unify_Node,
-        Disjunct_Node,
-        Conjunct_Node,
-        Recurse_Node);
+    type Node_Kind is (Unify_Node, Disjunct_Node, Conjunct_Node);
 
     type Graph_Component (Kind : Node_Kind) is limited record
         Counter : Natural;
@@ -568,9 +542,7 @@ private
             Dis_Goal2 : aliased Goal_Graph;
         when Conjunct_Node =>
             Con_Goal  : aliased Goal_Graph;
-            Con_Data  : Lazy_Holders.Holder;
-        when Recurse_Node =>
-            Rec_Goal  : aliased Goal_Graph;
+            Con_Data  : Lazy_Data_Access;
         end case;
     end record;