From 2f622510f4feecee552c43a31bd592d1c7f6617f Mon Sep 17 00:00:00 2001 From: Jedidiah Barber Date: Wed, 21 Jan 2026 15:31:35 +1300 Subject: Refactor of evaluation using custom bookkeeping datatype instead of Maps --- src/kompsos-collector.adb | 334 +++++++++++++++++++++++++++------------------- src/kompsos-collector.ads | 78 +++++++---- src/kompsos.ads | 7 +- 3 files changed, 249 insertions(+), 170 deletions(-) (limited to 'src') diff --git a/src/kompsos-collector.adb b/src/kompsos-collector.adb index e3c760e..c8333cf 100644 --- a/src/kompsos-collector.adb +++ b/src/kompsos-collector.adb @@ -18,8 +18,8 @@ package body Kompsos.Collector is -- Progress State -- ---------------------- - Cache : Cache_Maps.Map; - Book : Eval_Maps.Map; + Book_Root : Book_Node_Access := null; + Loose_Books : Loose_Book_Vectors.Vector; Global_Var : Variable := Relation.Next_Var; @@ -35,23 +35,15 @@ 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 - for Memo of Cache loop - for Line of Memo.Data loop - Free (Line.Data); - end loop; - end loop; - for Datum of Book loop - if Datum.Kind = Conjunct_Data then - Free (Datum.Con_Base); - Free (Datum.Con_Part); - end if; - end loop; + Reset (Relation.Graph.Actual, Book_Root); end Finalize; @@ -145,68 +137,119 @@ package body Kompsos.Collector is end Call_Lazy; - procedure Reset - (Ptr : in Constant_Goal_Access); - - procedure Do_Reset - (Ptr : in Constant_Graph_Access) is + (Ptr : in Graph_Component_Access; + Book : in out Book_Node_Access; + Extra : in out Book_Node_Vectors.Vector) is begin - if Ptr = null or else Ptr.Actual = null then + if Ptr = null or Book = null then return; end if; - if Cache.Contains (Ptr.Actual) then - for Line of Cache (Ptr.Actual).Data loop - Free (Line.Data); + if Book.Cache /= null then + for Item of Book.Cache.Data loop + Free (Item.Data); end loop; - Cache.Delete (Ptr.Actual); + Free (Book.Cache); end if; - case Ptr.Actual.Kind is + case Book.Data.Kind is when Unify_Node => - Book.Exclude (Ptr.Actual); - Do_Reset (Ptr.Actual.Uni_Goal'Unchecked_Access); + Do_Reset (Ptr.Uni_Goal.Actual, Book.Next1, Extra); when Disjunct_Node => - Book.Exclude (Ptr.Actual); - Do_Reset (Ptr.Actual.Dis_Goal1'Unchecked_Access); - Do_Reset (Ptr.Actual.Dis_Goal2'Unchecked_Access); + Do_Reset (Ptr.Dis_Goal1.Actual, Book.Next1, Extra); + Do_Reset (Ptr.Dis_Goal2.Actual, Book.Next2, Extra); when Conjunct_Node => - if Book.Contains (Ptr.Actual) then - Reset (Constant_Goal_Access (Book.Element (Ptr.Actual).Con_Part)); - Free (Book (Ptr.Actual).Con_Part); - Free (Book (Ptr.Actual).Con_Base); - Book.Delete (Ptr.Actual); + 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); end if; - Do_Reset (Ptr.Actual.Con_Goal'Unchecked_Access); + Free (Book.Data.Con_Base); when Recurse_Node => - Book.Exclude (Ptr.Actual); - Do_Reset (Ptr.Actual.Rec_Goal'Unchecked_Access); + Do_Reset (Ptr.Rec_Goal.Actual, Book.Next1, Extra); end case; + + if Ptr.Counter > 1 then + if not Extra.Contains (Book) then + Extra.Append (Book); + end if; + else + Free (Book); + end if; end Do_Reset; procedure Reset - (Ptr : in Constant_Goal_Access) is + (Ptr : in Graph_Component_Access; + Book : in out Book_Node_Access) + is + Extra : Book_Node_Vectors.Vector; begin - if Ptr = null then - return; + Do_Reset (Ptr, Book, Extra); + for Item of Extra loop + if Item = Book then + Free (Book); + else + Free (Item); + end if; + end loop; + end Reset; + + + function Raw_New_Book + (Kind : in Node_Kind) + return Book_Node_Access is + begin + 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 => <>); + end case; + end Raw_New_Book; + + + function New_Book + (Ptr : in Graph_Component_Access) + return Book_Node_Access is + begin + pragma Assert (Ptr.Counter /= 0); + if Ptr.Counter = 1 or Ptr = Relation.Graph.Actual then + return Raw_New_Book (Ptr.Kind); else - Do_Reset (Ptr.Graph'Access); + return Acc : constant Book_Node_Access := Raw_New_Book (Ptr.Kind) do + Loose_Books.Append ((1, Ptr, Acc)); + end return; end if; - end Reset; + end New_Book; - function Get_Next - (Ptr : in Constant_Graph_Access; - Base : in State; - Index : in Long_Positive; - Result : out State) - return Boolean; + function Connect_Loose + (Ptr : in Graph_Component_Access) + return Book_Node_Access is + 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; + end if; + end loop; + return null; + end Connect_Loose; 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) @@ -214,183 +257,191 @@ package body Kompsos.Collector is begin case Ptr.Kind is when Unify_Node => - if not Book.Contains (Ptr) then - Book.Insert (Ptr, (Kind => Unify_Data, others => <>)); + if Book = null then + Book := New_Book (Ptr); end if; while Get_Next (Ptr.Uni_Goal'Unchecked_Access, - Base, - Index + Book.Element (Ptr).Uni_Offset, + 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 (Ptr).Uni_Offset := Book.Element (Ptr).Uni_Offset + 1; + Book.Data.Uni_Offset := Book.Data.Uni_Offset + 1; end if; end loop; return False; when Disjunct_Node => - if not Book.Contains (Ptr) then - Book.Insert (Ptr, (Kind => Disjunct_Data, others => <>)); + if Book = null then + Book := New_Book (Ptr); end if; - if Book.Element (Ptr).Dis_Gone1 then - if Book.Element (Ptr).Dis_Gone2 then + if Book.Data.Dis_Gone1 then + if Book.Data.Dis_Gone2 then return False; elsif Get_Next (Ptr.Dis_Goal2'Unchecked_Access, - Base, - Book.Element (Ptr).Dis_Next2, + Book.Next2, Base, + Book.Data.Dis_Next2, Result) then - Book (Ptr).Dis_Next2 := Book.Element (Ptr).Dis_Next2 + 1; + Book.Data.Dis_Next2 := Book.Data.Dis_Next2 + 1; return True; else - Book (Ptr).Dis_Gone2 := True; + Book.Data.Dis_Gone2 := True; return False; end if; - elsif Book.Element (Ptr).Dis_Gone2 then + elsif Book.Data.Dis_Gone2 then if Get_Next (Ptr.Dis_Goal1'Unchecked_Access, - Base, - Book.Element (Ptr).Dis_Next1, + Book.Next1, Base, + Book.Data.Dis_Next1, Result) then - Book (Ptr).Dis_Next1 := Book.Element (Ptr).Dis_Next1 + 1; + Book.Data.Dis_Next1 := Book.Data.Dis_Next1 + 1; return True; else - Book (Ptr).Dis_Gone1 := True; + Book.Data.Dis_Gone1 := True; return False; end if; - elsif Book.Element (Ptr).Dis_Flag then + elsif Book.Data.Dis_Flag then if Get_Next (Ptr.Dis_Goal1'Unchecked_Access, - Base, - Book.Element (Ptr).Dis_Next1, + Book.Next1, Base, + Book.Data.Dis_Next1, Result) then - Book (Ptr).Dis_Next1 := Book.Element (Ptr).Dis_Next1 + 1; - Book (Ptr).Dis_Flag := not Book.Element (Ptr).Dis_Flag; + Book.Data.Dis_Next1 := Book.Data.Dis_Next1 + 1; + Book.Data.Dis_Flag := not Book.Data.Dis_Flag; return True; else - Book (Ptr).Dis_Gone1 := True; + Book.Data.Dis_Gone1 := True; if Get_Next (Ptr.Dis_Goal2'Unchecked_Access, - Base, - Book.Element (Ptr).Dis_Next2, + Book.Next2, Base, + Book.Data.Dis_Next2, Result) then - Book (Ptr).Dis_Next2 := Book.Element (Ptr).Dis_Next2 + 1; + Book.Data.Dis_Next2 := Book.Data.Dis_Next2 + 1; return True; else - Book (Ptr).Dis_Gone2 := True; + Book.Data.Dis_Gone2 := True; return False; end if; end if; else if Get_Next (Ptr.Dis_Goal2'Unchecked_Access, - Base, - Book.Element (Ptr).Dis_Next2, + Book.Next2, Base, + Book.Data.Dis_Next2, Result) then - Book (Ptr).Dis_Next2 := Book.Element (Ptr).Dis_Next2 + 1; - Book (Ptr).Dis_Flag := not Book.Element (Ptr).Dis_Flag; + Book.Data.Dis_Next2 := Book.Data.Dis_Next2 + 1; + Book.Data.Dis_Flag := not Book.Data.Dis_Flag; return True; else - Book (Ptr).Dis_Gone2 := True; + Book.Data.Dis_Gone2 := True; if Get_Next (Ptr.Dis_Goal1'Unchecked_Access, - Base, - Book.Element (Ptr).Dis_Next1, + Book.Next1, Base, + Book.Data.Dis_Next1, Result) then - Book (Ptr).Dis_Next1 := Book.Element (Ptr).Dis_Next1 + 1; + Book.Data.Dis_Next1 := Book.Data.Dis_Next1 + 1; return True; else - Book (Ptr).Dis_Gone1 := True; + Book.Data.Dis_Gone1 := True; return False; end if; end if; end if; when Conjunct_Node => - if not Book.Contains (Ptr) then - Book.Insert (Ptr, (Kind => Conjunct_Data, others => <>)); - if not Get_Next (Ptr.Con_Goal'Unchecked_Access, Base, 1, Result) then - Book (Ptr).Con_Gone := True; + 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 (Ptr).Con_Base := new State'(Result); - Book (Ptr).Con_Part := new Goal'( + 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 (Ptr).Con_Part.Next_Var; + Global_Var := Book.Data.Con_Part.Next_Var; end if; end if; - if Book (Ptr).Con_Gone then + if Book.Data.Con_Gone then return False; end if; while not Get_Next - (Constant_Graph_Access'(Book.Element (Ptr).Con_Part.Graph'Access), - Book.Element (Ptr).Con_Base.all, - Book.Element (Ptr).Con_Next, + (Constant_Graph_Access'(Book.Data.Con_Part.Graph'Access), + Book.Next2, Book.Data.Con_Base.all, + Book.Data.Con_Next, Result) loop - Reset (Constant_Goal_Access (Book.Element (Ptr).Con_Part)); - Book (Ptr).Con_From := Book.Element (Ptr).Con_From + 1; + 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, - Base, - Book.Element (Ptr).Con_From, + Book.Next1, Base, + Book.Data.Con_From, Result) then - Book (Ptr).Con_Base.all := Result; - Book (Ptr).Con_Next := 1; + Book.Data.Con_Base.all := Result; + Book.Data.Con_Next := 1; else - Book (Ptr).Con_Gone := True; - Free (Book (Ptr).Con_Part); - Free (Book (Ptr).Con_Base); + Book.Data.Con_Gone := True; + Free (Book.Data.Con_Part); + Free (Book.Data.Con_Base); return False; end if; end loop; - Book (Ptr).Con_Next := Book.Element (Ptr).Con_Next + 1; + Book.Data.Con_Next := Book.Data.Con_Next + 1; return True; when Recurse_Node => - if not Book.Contains (Ptr) then - Book.Insert (Ptr, (Kind => Recurse_Data, others => <>)); - if Ptr.Rec_Goal.Actual = null then - Book (Ptr).Rec_Cache := False; - elsif not Cache.Contains (Ptr.Rec_Goal.Actual) then - Cache.Insert (Ptr.Rec_Goal.Actual, (True, State_Vectors.Empty_Vector)); + 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 + Book.Next1 := Connect_Loose (Ptr.Rec_Goal.Actual); + end if; + if Book.Data.Rec_Cache 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); + elsif Book.Next1.Cache = null then + Book.Next1.Cache := new Cache_Entry'(True, State_Vectors.Empty_Vector); else - Cache (Ptr.Rec_Goal.Actual).Keep := True; + Book.Next1.Cache.Keep := True; end if; end if; - if Book (Ptr).Rec_Gone then + if Book.Data.Rec_Gone then return False; end if; while not Get_Next (Ptr.Rec_Goal'Unchecked_Access, - Base, - Book.Element (Ptr).Rec_Next, + Book.Next1, Base, + Book.Data.Rec_Next, Result) loop - if Book.Element (Ptr).Rec_Next = 1 then - Book (Ptr).Rec_Gone := True; + if Book.Data.Rec_Next = 1 then + Book.Data.Rec_Gone := True; return False; else - Book (Ptr).Rec_Next := 1; - Book (Ptr).Rec_Cache := False; + Book.Data.Rec_Next := 1; + Book.Data.Rec_Cache := False; end if; end loop; - if Book (Ptr).Rec_Cache and Ptr.Rec_Goal.Actual.Counter = 1 then - Cache (Ptr.Rec_Goal.Actual).Data.Append ((1, new State'(Result))); + 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 (Ptr).Rec_Next := Book.Element (Ptr).Rec_Next + 1; + Book.Data.Rec_Next := Book.Data.Rec_Next + 1; return True; end case; end Do_Get_Next; @@ -398,6 +449,7 @@ package body Kompsos.Collector is function Get_Next (Ptr : in Constant_Graph_Access; + Book : in out Book_Node_Access; Base : in State; Index : in Long_Positive; Result : out State) @@ -412,25 +464,28 @@ package body Kompsos.Collector is else return False; end if; - elsif Cache.Contains (Ptr.Actual) and then - Index <= Cache (Ptr.Actual).Data.Last_Index + elsif Book = null then + Book := Connect_Loose (Ptr.Actual); + end if; + if Book /= null and then Book.Cache /= null and then + Index <= Book.Cache.Data.Last_Index then - Result := Cache (Ptr.Actual).Data (Index).Data.all; - Cache (Ptr.Actual).Data (Index).Used := Cache (Ptr.Actual).Data (Index).Used + 1; - if not Cache (Ptr.Actual).Keep and then - Natural (Cache (Ptr.Actual).Data (Index).Used) >= Ptr.Actual.Counter - then - Free (Cache (Ptr.Actual).Data (Index).Data); + 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; return True; else - return Found : constant Boolean := Do_Get_Next (Ptr.Actual, Base, Index, Result) do - if Found and Ptr.Actual.Counter > 1 then - if not Cache.Contains (Ptr.Actual) then - Cache.Insert (Ptr.Actual, (False, State_Vectors.Empty_Vector)); + 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 + Book.Cache := new Cache_Entry'(False, State_Vectors.Empty_Vector); end if; - pragma Assert (Index = Cache (Ptr.Actual).Data.Last_Index + 1); - Cache (Ptr.Actual).Data.Append ((1, new State'(Result))); + pragma Assert (Index = Book.Cache.Data.Last_Index + 1); + Book.Cache.Data.Append ((1, new State'(Result))); end if; end return; end if; @@ -453,7 +508,7 @@ package body Kompsos.Collector is elsif Exhausted then return False; else - State_Valid := Get_Next (Ptr, Within, Next_Index, Next_State); + State_Valid := Get_Next (Ptr, Book_Root, Within, Next_Index, Next_State); if not State_Valid then Exhausted := True; else @@ -490,9 +545,8 @@ package body Kompsos.Collector is procedure Reset is - Ptr : constant Constant_Goal_Access := Relation'Access; begin - Reset (Ptr); + Reset (Relation.Graph.Actual, Book_Root); Next_Index := 1; State_Valid := False; Exhausted := False; diff --git a/src/kompsos-collector.ads b/src/kompsos-collector.ads index d352fa3..c1ea8bc 100644 --- a/src/kompsos-collector.ads +++ b/src/kompsos-collector.ads @@ -8,7 +8,6 @@ private with - Ada.Containers.Ordered_Maps, Ada.Containers.Vectors, Ada.Finalization; @@ -48,46 +47,34 @@ private - type Eval_Kind is - (Unify_Data, - Disjunct_Data, - Conjunct_Data, - Recurse_Data); - - type Eval_Data (Kind : Eval_Kind := Unify_Data) is record + type Eval_Data (Kind : Node_Kind := Unify_Node) is record case Kind is - when Unify_Data => + when Unify_Node => Uni_Offset : Long_Natural := 0; - when Disjunct_Data => + 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_Data => + 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_Data => + when Recurse_Node => Rec_Next : Long_Positive := 1; Rec_Gone : Boolean := False; Rec_Cache : Boolean := True; end case; end record; - package Eval_Maps is new Ada.Containers.Ordered_Maps - (Key_Type => Graph_Component_Access, - Element_Type => Eval_Data); - - - subtype Short_Positive is Short_Integer range 1 .. Short_Integer'Last; type Cached_State is record - Used : Short_Positive; - Data : State_Access; + Used : Positive := 1; + Data : State_Access := null; end record; package State_Vectors is new Ada.Containers.Vectors @@ -95,13 +82,54 @@ private Element_Type => Cached_State); type Cache_Entry is record - Keep : Boolean; - Data : State_Vectors.Vector; + Keep : Boolean := False; + Data : State_Vectors.Vector := State_Vectors.Empty_Vector; + end record; + + type Cache_Entry_Access is access Cache_Entry; + + + + type Book_Node; + + type Book_Node_Access is access Book_Node; + + type Book_Node is record + Data : Eval_Data; + Cache : Cache_Entry_Access := null; + Next1 : Book_Node_Access := null; + Next2 : Book_Node_Access := null; + end record; + + + + type Loose_Book is record + Used : Positive := 1; + Ptr : Graph_Component_Access := null; + Book : Book_Node_Access := null; end record; - package Cache_Maps is new Ada.Containers.Ordered_Maps - (Key_Type => Graph_Component_Access, - Element_Type => Cache_Entry); + package Loose_Book_Vectors is new Ada.Containers.Vectors + (Index_Type => Long_Positive, + Element_Type => Loose_Book); + + package Book_Node_Vectors is new Ada.Containers.Vectors + (Index_Type => Long_Positive, + Element_Type => Book_Node_Access); + + + + procedure Reset + (Ptr : in Graph_Component_Access; + Book : in out Book_Node_Access); + + 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; diff --git a/src/kompsos.ads b/src/kompsos.ads index 9a00251..84b3ce2 100644 --- a/src/kompsos.ads +++ b/src/kompsos.ads @@ -9,7 +9,6 @@ private with Ada.Containers.Indefinite_Holders, - Ada.Containers.Ordered_Maps, Ada.Containers.Vectors, Ada.Finalization; @@ -415,10 +414,6 @@ private - type Term_Component; - - type Term_Component_Access is access Term_Component; - subtype Not_Null_Term_Kind is Term_Kind range Atom_Term .. Pair_Term; type Term_Component (Kind : Not_Null_Term_Kind) is limited record @@ -434,6 +429,8 @@ private end case; end record; + type Term_Component_Access is access Term_Component; + type Term is new Ada.Finalization.Controlled with record Actual : Term_Component_Access := null; end record; -- cgit