Unrolled linked lists for StateHEADmaster

5 files changed, 87 insertions, 50 deletions

diff --git a/src/kompsos-collector.adb b/src/kompsos-collector.adb
index 4654dc7..2c52160 100644
--- a/src/kompsos-collector.adb
+++ b/src/kompsos-collector.adb
@@ -55,6 +55,33 @@ package body Kompsos.Collector is
 
     --  Unification  --
 
+    Use_New_Node : Boolean := False;
+
+    function Append
+           (This  : in State;
+            Key   : in Variable;
+            Value : in Term)
+        return State 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;
+
+
     procedure Walk
            (This : in     State;
             Item : in out Term)
@@ -95,21 +122,11 @@ package body Kompsos.Collector is
 
         --  Unify Variable and other Terms by introducing a new substitution
         if Real_Left.Kind = Var_Term then
-            Extended := (Ctrl => (Ada.Finalization.Controlled with
-                Actual => new State_Component'(
-                    Counter => 1,
-                    Key     => Real_Left.Var,
-                    Value   => Real_Right,
-                    Next    => Potential)));
+            Extended := Append (Potential, Real_Left.Var, Real_Right);
             return True;
         end if;
         if Real_Right.Kind = Var_Term then
-            Extended := (Ctrl => (Ada.Finalization.Controlled with
-                Actual => new State_Component'(
-                    Counter => 1,
-                    Key     => Real_Right.Var,
-                    Value   => Real_Left,
-                    Next    => Potential)));
+            Extended := Append (Potential, Real_Right.Var, Real_Left);
             return True;
         end if;
 
@@ -205,7 +222,7 @@ package body Kompsos.Collector is
     end Reset;
 
 
-    function Raw_New_Book
+    function New_Book_Factory
            (Kind : in Node_Kind)
         return Book_Node_Access is
     begin
@@ -219,7 +236,7 @@ package body Kompsos.Collector is
         when Recurse_Node =>
             return new Book_Node'(Data => (Kind => Recurse_Node,  others => <>), others => <>);
         end case;
-    end Raw_New_Book;
+    end New_Book_Factory;
 
 
     function New_Book
@@ -228,9 +245,9 @@ package body Kompsos.Collector is
     begin
         pragma Assert (Ptr.Counter /= 0);
         if Ptr.Counter = 1 or Ptr = Relation.Graph.Actual then
-            return Raw_New_Book (Ptr.Kind);
+            return New_Book_Factory (Ptr.Kind);
         else
-            return Acc : constant Book_Node_Access := Raw_New_Book (Ptr.Kind) do
+            return Acc : constant Book_Node_Access := New_Book_Factory (Ptr.Kind) do
                 Loose_Books.Append ((1, Ptr, Acc));
             end return;
         end if;
@@ -414,12 +431,10 @@ package body Kompsos.Collector is
             if Book = null then
                 Book := New_Book (Ptr);
             end if;
-            if Ptr.Rec_Goal.Actual = null then
-                Book.Data.Rec_Cache := False;
-            elsif Book.Next1 = null then
+            if Book.Next1 = null then
                 Book.Next1 := Connect_Loose (Ptr.Rec_Goal.Actual);
             end if;
-            if Book.Data.Rec_Cache then
+            if Ptr.Rec_Goal.Actual /= null then
                 if Book.Next1 = null then
                     Book.Next1 := New_Book (Ptr.Rec_Goal.Actual);
                     Book.Next1.Cache := new Cache_Entry'(True, State_Vectors.Empty_Vector);
@@ -443,12 +458,8 @@ package body Kompsos.Collector is
                     return False;
                 else
                     Book.Data.Rec_Next := 1;
-                    Book.Data.Rec_Cache := False;
                 end if;
             end loop;
-            if Book.Data.Rec_Cache and Ptr.Rec_Goal.Actual.Counter = 1 then
-                Book.Next1.Cache.Data.Append ((1, new State'(Result)));
-            end if;
             Book.Data.Rec_Next := Book.Data.Rec_Next + 1;
             return True;
         end case;
@@ -468,6 +479,7 @@ package body Kompsos.Collector is
         elsif Ptr.Actual = null then
             if Index = 1 then
                 Result := Base;
+                Use_New_Node := True;
                 return True;
             else
                 return False;
@@ -483,17 +495,24 @@ package body Kompsos.Collector is
             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;
         else
             return Found : constant Boolean :=
                 Do_Get_Next (Ptr.Actual, Book, Base, Index, Result)
             do
-                if Found and Ptr.Actual.Counter > 1 and Ptr.Actual /= Relation.Graph.Actual then
-                    if Book.Cache = null then
+                if Found then
+                    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;
-                    pragma Assert (Index = Book.Cache.Data.Last_Index + 1);
-                    Book.Cache.Data.Append ((1, new State'(Result)));
+                    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 if;
diff --git a/src/kompsos-collector.ads b/src/kompsos-collector.ads
index f03e1e6..93fd6d4 100644
--- a/src/kompsos-collector.ads
+++ b/src/kompsos-collector.ads
@@ -64,7 +64,6 @@ private
         when Recurse_Node =>
             Rec_Next   : Long_Positive := 1;
             Rec_Gone   : Boolean       := False;
-            Rec_Cache  : Boolean       := True;
         end case;
     end record;
 
diff --git a/src/kompsos-pretty_print.adb b/src/kompsos-pretty_print.adb
index 216ceec..2befe6d 100644
--- a/src/kompsos-pretty_print.adb
+++ b/src/kompsos-pretty_print.adb
@@ -119,9 +119,11 @@ package body Kompsos.Pretty_Print is
                 Marker : State_Component_Access := Item.Ctrl.Actual;
             begin
                 while Marker /= null loop
-                    SU.Append (Result, Latin.HT &
-                        Image (Marker.Key) & " => " &
-                        Image (Marker.Value) & Latin.LF);
+                    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;
diff --git a/src/kompsos.adb b/src/kompsos.adb
index 2efa69b..97e8ce6 100644
--- a/src/kompsos.adb
+++ b/src/kompsos.adb
@@ -252,10 +252,12 @@ package body Kompsos is
         Ptr : State_Component_Access := This.Ctrl.Actual;
     begin
         while Ptr /= null loop
-            if Ptr.Key = Key then
-                Value := Term'Class (Ptr.Value);
-                return True;
-            end if;
+            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;
         return False;
@@ -608,20 +610,23 @@ package body Kompsos is
     begin
         if Subst.Ctrl.Actual = null then
             return Empty_Term;
-        else
-            declare
-                Min_Pos : State_Component_Access := Subst.Ctrl.Actual;
-                Marker  : State_Component_Access := Min_Pos.Next.Ctrl.Actual;
-            begin
-                while Marker /= null loop
-                    if Marker.Key < Min_Pos.Key then
+        end if;
+        declare
+            Min_Pos : State_Component_Access := Subst.Ctrl.Actual;
+            Min_Ind : Valid_Count            := Valid_Count'First;
+            Marker  : State_Component_Access := Min_Pos;
+        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;
-                    Marker := Marker.Next.Ctrl.Actual;
                 end loop;
-                return Min_Pos.Value.Resolve (Subst);
-            end;
-        end if;
+                Marker := Marker.Next.Ctrl.Actual;
+            end loop;
+            return Min_Pos.Data (Min_Ind).Value.Resolve (Subst);
+        end;
     end Resolve_First;
 
 
diff --git a/src/kompsos.ads b/src/kompsos.ads
index d1e19be..b8629fb 100644
--- a/src/kompsos.ads
+++ b/src/kompsos.ads
@@ -459,11 +459,23 @@ private
 
 
 
+    type Binding is record
+        Key   : Variable;
+        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;
-        Key     : Variable;
-        Value   : Term;
-        Next    : aliased State;
+        Valid   : Valid_Count;
+        Data    : Binding_Array (Valid_Count'Range);
+        Next    : State;
     end record;
 
     type State_Component_Access is access State_Component;