From 0188dfb4d373cc8570222496f7d04cd3ae2774f3 Mon Sep 17 00:00:00 2001 From: Jedidiah Barber Date: Fri, 19 Dec 2025 21:51:48 +1300 Subject: Worlds separated into Goals that run on a State, improvement to unification efficiency --- src/kompsos-collector.adb | 101 +++++++++++++++++++++++++--------------------- 1 file changed, 55 insertions(+), 46 deletions(-) (limited to 'src/kompsos-collector.adb') diff --git a/src/kompsos-collector.adb b/src/kompsos-collector.adb index d7c40eb..e2ee677 100644 --- a/src/kompsos-collector.adb +++ b/src/kompsos-collector.adb @@ -17,14 +17,15 @@ package body Kompsos.Collector is -- Memory Management -- ------------------------- - procedure Free is new Ada.Unchecked_Deallocation (World, World_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 Managed_Map) is begin for Datum of This.Actual loop if Datum.Kind = Conjunct_Data then + Free (Datum.Con_Base); Free (Datum.Con_Part); end if; end loop; @@ -138,12 +139,8 @@ package body Kompsos.Collector is -- Unify Pair Terms by unifying each corresponding part if Real_Left.Kind = Pair_Term and then Real_Right.Kind = Pair_Term then - declare - Middle : State; - begin - return Do_Unify (Potential, Real_Left.Left, Real_Right.Left, Middle) and then - Do_Unify (Middle, Real_Left.Right, Real_Right.Right, Extended); - end; + return Do_Unify (Potential, Real_Left.Left, Real_Right.Left, Extended) and then + Do_Unify (Extended, Real_Left.Right, Real_Right.Right, Extended); end if; -- Not sure how things get here, but if all else fails @@ -155,9 +152,9 @@ package body Kompsos.Collector is -- Result Collection -- function Call_Lazy - (This : in World; + (This : in Goal; Data : in Lazy_Holders.Holder) - return World + return Goal is Ref : constant Lazy_Holders.Constant_Reference_Type := Data.Constant_Reference; begin @@ -173,7 +170,7 @@ package body Kompsos.Collector is procedure Reset - (Ptr : in Constant_World_Access) is + (Ptr : in Constant_Goal_Access) is begin if Ptr = null or else Ptr.Actual = null then return; @@ -185,53 +182,55 @@ package body Kompsos.Collector is when Static_Node => return; when Fresh_Node => - Reset (Ptr.Actual.Frs_World'Unchecked_Access); + Reset (Ptr.Actual.Frs_Goal'Unchecked_Access); when Unify_Node => Book.Exclude (Ptr.Actual); - Reset (Ptr.Actual.Uni_World'Unchecked_Access); + Reset (Ptr.Actual.Uni_Goal'Unchecked_Access); when Disjunct_Node => Book.Exclude (Ptr.Actual); - Reset (Ptr.Actual.Dis_World1'Unchecked_Access); - Reset (Ptr.Actual.Dis_World2'Unchecked_Access); + Reset (Ptr.Actual.Dis_Goal1'Unchecked_Access); + Reset (Ptr.Actual.Dis_Goal2'Unchecked_Access); when Conjunct_Node => if Book.Contains (Ptr.Actual) then - Reset (Constant_World_Access (Book.Element (Ptr.Actual).Con_Part)); + 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); end if; - Reset (Ptr.Actual.Con_World'Unchecked_Access); + Reset (Ptr.Actual.Con_Goal'Unchecked_Access); when Recurse_Node => Book.Exclude (Ptr.Actual); - Reset (Ptr.Actual.Rec_World'Unchecked_Access); + Reset (Ptr.Actual.Rec_Goal'Unchecked_Access); end case; end Reset; function Get_Next - (Ptr : in Constant_World_Access; + (Ptr : in Constant_Goal_Access; + Base : in State; Index : in Long_Positive; Result : out State) return Boolean; function Do_Get_Next - (Ptr : in World_Component_Access; + (Ptr : in Goal_Component_Access; + Base : in State; Index : in Long_Positive; Result : out State) return Boolean is begin case Ptr.Kind is when Static_Node => - if Index <= Ptr.Stc_States.Last_Index then - Result := Ptr.Stc_States (Index); + if Index = 1 then + Result := Base; return True; else return False; end if; when Fresh_Node => - if Get_Next (Ptr.Frs_World'Unchecked_Access, Index, Result) then + if Get_Next (Ptr.Frs_Goal'Unchecked_Access, Base, Index, Result) then Result.LVars.Append (Ptr.Frs_Var.Name); Result.Ident.Insert (Ptr.Frs_Var.Ident, Result.LVars.Last_Index); return True; @@ -244,7 +243,8 @@ package body Kompsos.Collector is Book.Insert (Ptr, (Kind => Unify_Data, others => <>)); end if; while Get_Next - (Ptr.Uni_World'Unchecked_Access, + (Ptr.Uni_Goal'Unchecked_Access, + Base, Index + Book.Element (Ptr).Uni_Offset, Result) loop @@ -264,7 +264,8 @@ package body Kompsos.Collector is if Book.Element (Ptr).Dis_Gone2 then return False; elsif Get_Next - (Ptr.Dis_World2'Unchecked_Access, + (Ptr.Dis_Goal2'Unchecked_Access, + Base, Book.Element (Ptr).Dis_Next2, Result) then @@ -276,7 +277,8 @@ package body Kompsos.Collector is end if; elsif Book.Element (Ptr).Dis_Gone2 then if Get_Next - (Ptr.Dis_World1'Unchecked_Access, + (Ptr.Dis_Goal1'Unchecked_Access, + Base, Book.Element (Ptr).Dis_Next1, Result) then @@ -288,7 +290,8 @@ package body Kompsos.Collector is end if; elsif Book.Element (Ptr).Dis_Flag then if Get_Next - (Ptr.Dis_World1'Unchecked_Access, + (Ptr.Dis_Goal1'Unchecked_Access, + Base, Book.Element (Ptr).Dis_Next1, Result) then @@ -298,7 +301,8 @@ package body Kompsos.Collector is else Book (Ptr).Dis_Gone1 := True; if Get_Next - (Ptr.Dis_World2'Unchecked_Access, + (Ptr.Dis_Goal2'Unchecked_Access, + Base, Book.Element (Ptr).Dis_Next2, Result) then @@ -311,7 +315,8 @@ package body Kompsos.Collector is end if; else if Get_Next - (Ptr.Dis_World2'Unchecked_Access, + (Ptr.Dis_Goal2'Unchecked_Access, + Base, Book.Element (Ptr).Dis_Next2, Result) then @@ -321,7 +326,8 @@ package body Kompsos.Collector is else Book (Ptr).Dis_Gone2 := True; if Get_Next - (Ptr.Dis_World1'Unchecked_Access, + (Ptr.Dis_Goal1'Unchecked_Access, + Base, Book.Element (Ptr).Dis_Next1, Result) then @@ -337,29 +343,30 @@ package body Kompsos.Collector is when Conjunct_Node => if not Book.Contains (Ptr) then Book.Insert (Ptr, (Kind => Conjunct_Data, others => <>)); - if not Get_Next (Ptr.Con_World'Unchecked_Access, 1, Result) then + if not Get_Next (Ptr.Con_Goal'Unchecked_Access, Base, 1, Result) then Book (Ptr).Con_Gone := True; else - Book (Ptr).Con_Base := new World'(World (Static (Result))); - Book (Ptr).Con_Part := new World'(Call_Lazy - (Book.Element (Ptr).Con_Base.all, Ptr.Con_Data)); + Book (Ptr).Con_Base := new State'(Result); + Book (Ptr).Con_Part := new Goal'(Call_Lazy (Empty_Goal, Ptr.Con_Data)); end if; end if; if Book (Ptr).Con_Gone then return False; end if; while not Get_Next - (Constant_World_Access (Book.Element (Ptr).Con_Part), + (Constant_Goal_Access (Book.Element (Ptr).Con_Part), + Book.Element (Ptr).Con_Base.all, Book.Element (Ptr).Con_Next, Result) loop - Reset (Constant_World_Access (Book.Element (Ptr).Con_Part)); + Reset (Constant_Goal_Access (Book.Element (Ptr).Con_Part)); if Get_Next - (Ptr.Con_World'Unchecked_Access, + (Ptr.Con_Goal'Unchecked_Access, + Base, Book.Element (Ptr).Con_From, Result) then - Book (Ptr).Con_Base.Actual.Stc_States (1) := Result; + Book (Ptr).Con_Base.all := Result; Book (Ptr).Con_Next := 1; Book (Ptr).Con_From := Book.Element (Ptr).Con_From + 1; else @@ -380,7 +387,8 @@ package body Kompsos.Collector is return False; end if; while not Get_Next - (Ptr.Rec_World'Unchecked_Access, + (Ptr.Rec_Goal'Unchecked_Access, + Base, Book.Element (Ptr).Rec_Next, Result) loop @@ -398,7 +406,7 @@ package body Kompsos.Collector is function Cached - (Ptr : in World_Component_Access; + (Ptr : in Goal_Component_Access; Index : in Long_Positive; Result : out State) return Boolean is @@ -413,7 +421,7 @@ package body Kompsos.Collector is procedure Cache_This - (Ptr : in World_Component_Access; + (Ptr : in Goal_Component_Access; Index : in Long_Positive; Result : in State) is begin @@ -428,7 +436,8 @@ package body Kompsos.Collector is function Get_Next - (Ptr : in Constant_World_Access; + (Ptr : in Constant_Goal_Access; + Base : in State; Index : in Long_Positive; Result : out State) return Boolean is @@ -438,7 +447,7 @@ package body Kompsos.Collector is elsif Cached (Ptr.Actual, Index, Result) then return True; else - return Found : constant Boolean := Do_Get_Next (Ptr.Actual, Index, Result) do + return Found : constant Boolean := Do_Get_Next (Ptr.Actual, Base, Index, Result) do if Found then Cache_This (Ptr.Actual, Index, Result); end if; @@ -456,14 +465,14 @@ package body Kompsos.Collector is function Has_Next return Boolean is - Ptr : constant Constant_World_Access := Source'Access; + Ptr : constant Constant_Goal_Access := Relation'Access; begin if State_Valid then return True; elsif Exhausted then return False; else - State_Valid := Get_Next (Ptr, Next_Index, Next_State); + State_Valid := Get_Next (Ptr, Within, Next_Index, Next_State); if not State_Valid then Exhausted := True; else @@ -501,7 +510,7 @@ package body Kompsos.Collector is procedure Reset is - Ptr : constant Constant_World_Access := Source'Access; + Ptr : constant Constant_Goal_Access := Relation'Access; begin Reset (Ptr); Next_Index := 1; -- cgit