diff options
| -rw-r--r-- | src/kompsos-collector.adb | 124 | ||||
| -rw-r--r-- | src/kompsos-collector.ads | 12 | ||||
| -rw-r--r-- | test/complete.adb | 72 | ||||
| -rw-r--r-- | tests.gpr | 26 |
4 files changed, 192 insertions, 42 deletions
diff --git a/src/kompsos-collector.adb b/src/kompsos-collector.adb index cca9dbd..b64d284 100644 --- a/src/kompsos-collector.adb +++ b/src/kompsos-collector.adb @@ -15,23 +15,27 @@ with package body Kompsos.Collector is - ---------------------- - -- Progress State -- - ---------------------- + --------------------- + -- Progress Info -- + --------------------- Conjunct_Goals : Goal_Access_Vectors.Vector; - - Global_Var : Variable := Relation.Next_Var; + Global_Var : Variable := Relation.Next_Var; Up_Map : Upwards_Maps.Map; Up_Vector : Upwards_Vectors.Vector; Do_Walk : access procedure; Walk_Trail : Breadcrumb_Vectors.Vector; + Walk_Choices : Choice_Vector; Location : Graph_Component_Access; Local_Cursor : Upwards_Maps.Cursor; Next_Pick : Positive; + Conjunct_Count : Natural := 0; + Conjunct_Limit : Positive := Initial_Depth_Limit; + Already_Done : Choice_Vector_Vectors.Vector; + Result : State := Within; State_Valid : Boolean := False; Exhausted : Boolean := False; @@ -61,6 +65,7 @@ package body Kompsos.Collector is -- Datatypes -- ----------------- + -- Compares two sparsely encoded binary numbers function "<" (Left, Right : in Disjuncts_Chosen) return Boolean is @@ -109,7 +114,7 @@ package body Kompsos.Collector is -- Unification -- - procedure Walk + procedure Walk_State (This : in State; Item : in out Term) is @@ -118,7 +123,7 @@ package body Kompsos.Collector is while Item.Kind = Var_Term and then Lookup (This, Item.Var, Bound_Term) loop Item := Bound_Term; end loop; - end Walk; + end Walk_State; function Do_Unify @@ -130,8 +135,8 @@ package body Kompsos.Collector is Real_Right : Term := Term (Right); begin -- Resolve Variable substitution - Walk (Subst, Real_Left); - Walk (Subst, Real_Right); + Walk_State (Subst, Real_Left); + Walk_State (Subst, Real_Right); -- Unify equal Variable/Atom/Null Terms if (Real_Left.Kind = Var_Term and then @@ -269,7 +274,10 @@ package body Kompsos.Collector is Old_Choices : Disjuncts_Chosen := Up_Vector (Upwards_Maps.Element (Local_Cursor)).Parents (Next_Pick).Order; begin + -- Remove the no longer needed edge leading to the Conjunct node Up_Vector (Upwards_Maps.Element (Local_Cursor)).Parents.Delete (Next_Pick); + + -- Expand out the Conjunct Conjunct_Goals.Append (new Goal'( Call_Lazy ((Graph => (Ada.Finalization.Controlled with Actual => null), @@ -277,40 +285,60 @@ package body Kompsos.Collector is Node.Con_Data.all))); Global_Var := Conjunct_Goals.Last_Element.Next_Var; declare + -- Declare needed to avoid Tampering issues 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)); + + -- Join the top of the expanded subgraph up to whatever the Conjunct was joined to + if Up_Map.Contains (Node) then + Up_Map.Insert (Conjunct_Goals.Last_Element.Graph.Actual, Up_Map.Element (Node)); + end if; end Expand_Conjunct; - -- Upwards Depth First Search -- + -- Upwards Iterative Deepening Depth First Search -- + + procedure Reset_Position is + begin + Conjunct_Count := 0; + Conjunct_Limit := Conjunct_Limit * 2; + Walk_Trail.Clear; + Walk_Choices.Clear; + Location := null; + Local_Cursor := Up_Map.Find (Location); + Next_Pick := 1; + Truncate (Result, Long_Natural (Within.Binds.Length)); + end Reset_Position; + function Choose_Another_Way return Boolean is Marker : Natural := Walk_Trail.Last_Index; - Crumb : Breadcrumb; + Crumb : Breadcrumb; + Option : Positive; begin + -- Backtrack until a choice point with unexplored branches is found while Marker /= Breadcrumb_Vectors.No_Index loop Crumb := Walk_Trail (Marker); + Option := Walk_Choices (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; + if Up_Vector (Upwards_Maps.Element (Local_Cursor)).Parents.Last_Index >= Option + 1 then + Next_Pick := Option + 1; Truncate (Result, Crumb.State_Size); Walk_Trail.Set_Length (Ada.Containers.Count_Type (Marker - 1)); - return True; + Walk_Choices.Set_Length (Ada.Containers.Count_Type (Marker - 1)); + return True; -- Backtracking success else Marker := Marker - 1; end if; end loop; - return False; + return False; -- Backtracking failure, nothing further available end Choose_Another_Way; @@ -319,29 +347,65 @@ package body Kompsos.Collector is Ptr : Graph_Component_Access; begin loop + -- Make sure current State passes unification if Location = null or else Location.Kind /= Unify_Node or else Do_Unify (Result, Location.Uni_Term1, Location.Uni_Term2) then + + -- Have we reached the top of the Graph? if Local_Cursor = Upwards_Maps.No_Element then - State_Valid := True; - return; - end if; - Ptr := Up_Vector (Upwards_Maps.Element (Local_Cursor)).Parents (Next_Pick).Node; - if Ptr.Kind = Conjunct_Node then - Expand_Conjunct (Ptr); + if not Already_Done.Contains (Walk_Choices) then + Already_Done.Append (Walk_Choices); + State_Valid := True; + return; + elsif not Choose_Another_Way then + if Conjunct_Count >= Conjunct_Limit then + Reset_Position; + else + State_Valid := False; + Exhausted := True; + return; + end if; + end if; end if; + + -- If next node is a Conjunct then expand as necessary until the current limit + loop + Ptr := Up_Vector (Upwards_Maps.Element (Local_Cursor)).Parents (Next_Pick).Node; + exit when Ptr.Kind /= Conjunct_Node; + if Conjunct_Count >= Conjunct_Limit then + if not Choose_Another_Way then + Reset_Position; + end if; + else + Expand_Conjunct (Ptr); + Conjunct_Count := Conjunct_Count + 1; + end if; + end loop; + + -- Keep a trail for backtracking if Up_Vector (Upwards_Maps.Element (Local_Cursor)).Parents.Last_Index > 1 then - Walk_Trail.Append ((Location, Next_Pick, Result.Binds.Last_Index)); + Walk_Trail.Append ((Location, Result.Binds.Last_Index)); + Walk_Choices.Append (Next_Pick); end if; + + -- Move up a node Location := Up_Vector (Upwards_Maps.Element (Local_Cursor)).Parents (Next_Pick).Node; Local_Cursor := Up_Map.Find (Location); Next_Pick := 1; else + + -- If unification fails then backtrack if possible, + -- or otherwise reset if the Graph isn't exhausted if not Choose_Another_Way then - State_Valid := False; - Exhausted := True; - return; + if Conjunct_Count > 0 then + Reset_Position; + else + State_Valid := False; + Exhausted := True; + return; + end if; end if; end if; end loop; @@ -352,6 +416,9 @@ package body Kompsos.Collector is begin if Choose_Another_Way then Walk_Graph; + elsif Conjunct_Count >= Conjunct_Limit then + Reset_Position; + Walk_Graph; else State_Valid := False; Exhausted := True; @@ -425,6 +492,7 @@ package body Kompsos.Collector is begin declare + -- Declare needed because this parameter must be a variable Temp : Positive_Vectors.Vector := Positive_Vectors.Empty_Vector; begin Build_Up_Map (Relation.Graph.Actual, null, 0, Temp); diff --git a/src/kompsos-collector.ads b/src/kompsos-collector.ads index a341e1b..6a890a3 100644 --- a/src/kompsos-collector.ads +++ b/src/kompsos-collector.ads @@ -88,11 +88,10 @@ private Element_Type => Goal_Access); - -- Upwards Depth First Search -- + -- Upwards Iterative Deepening Depth First Search -- type Breadcrumb is record Choice_Node : Graph_Component_Access; - Option : Positive; State_Size : Long_Natural; end record; @@ -100,6 +99,15 @@ private (Index_Type => Positive, Element_Type => Breadcrumb); + subtype Choice_Vector is Positive_Vectors.Vector; + + package Choice_Vector_Vectors is new Ada.Containers.Vectors + (Index_Type => Positive, + Element_Type => Choice_Vector, + "=" => Positive_Vectors."="); + + Initial_Depth_Limit : constant Positive := 5; + -- Cleanup -- diff --git a/test/complete.adb b/test/complete.adb new file mode 100644 index 0000000..0890e8b --- /dev/null +++ b/test/complete.adb @@ -0,0 +1,72 @@ + + +-- Programmed by Jedidiah Barber +-- Licensed under the Sunset License v1.0 + +-- See license.txt for further details + + +with + + Ada.Text_IO, + Kompsos.Pretty_Print; + + +procedure Complete is + + package TIO renames Ada.Text_IO; + + + package InKomp is new Kompsos (Integer); + use InKomp; + + package Printer is new InKomp.Pretty_Print (Integer'Image); + + + function Fives + (This : in Goal; + Item : in Term'Class) + return Goal + is + One, Two : Goal := This; + begin + One.Unify (Item, 5); + Two.Conjunct (Fives'Access, Item); + return Disjunct (One, Two); + end Fives; + +begin + + TIO.Put_Line ("This program will loop forever unless the implementation is using"); + TIO.Put_Line ("a complete search strategy. It is suggested to terminate it manually"); + TIO.Put_Line ("if it doesn't complete quickly."); + + TIO.New_Line; + + declare + Relation : Goal := Empty_Goal; + Value : constant Term := Relation.Fresh; + Ignore : constant Term := Relation.Fresh; + begin + Relation := Disjunct (Relation.Unify (Ignore, 6), Relation.Unify (Value, 7)); + Relation := Fives (Relation, Ignore); + TIO.Put_Line ("Value is " & Printer.Image (Value.Resolve (Relation.Run)) & " on right."); + end; + + declare + Relation : Goal := Empty_Goal; + Value : constant Term := Relation.Fresh; + Ignore : constant Term := Relation.Fresh; + begin + Relation := Disjunct (Relation.Unify (Value, 7), Relation.Unify (Ignore, 6)); + Relation := Fives (Relation, Ignore); + TIO.Put_Line ("Value is " & Printer.Image (Value.Resolve (Relation.Run)) & " on left."); + end; + + TIO.New_Line; + + TIO.Put_Line ("Test complete."); + +end Complete; + + @@ -19,6 +19,7 @@ project Tests is ("ab.adb", "addsubo.adb", "boolnum.adb", + "complete.adb", "divo.adb", "expo.adb", "fivesix.adb", @@ -30,18 +31,19 @@ project Tests is "trees.adb"); package Builder is - for Executable ("ab.adb") use "ab"; - for Executable ("addsubo.adb") use "addsubo"; - for Executable ("boolnum.adb") use "boolnum"; - for Executable ("divo.adb") use "divo"; - for Executable ("expo.adb") use "expo"; - for Executable ("fivesix.adb") use "fivesix"; - for Executable ("logo.adb") use "logo"; - for Executable ("membero.adb") use "membero"; - for Executable ("multo.adb") use "multo"; - for Executable ("pprint.adb") use "pprint"; - for Executable ("rembero.adb") use "rembero"; - for Executable ("trees.adb") use "trees"; + for Executable ("ab.adb") use "ab"; + for Executable ("addsubo.adb") use "addsubo"; + for Executable ("boolnum.adb") use "boolnum"; + for Executable ("complete.adb") use "complete"; + for Executable ("divo.adb") use "divo"; + for Executable ("expo.adb") use "expo"; + for Executable ("fivesix.adb") use "fivesix"; + for Executable ("logo.adb") use "logo"; + for Executable ("membero.adb") use "membero"; + for Executable ("multo.adb") use "multo"; + for Executable ("pprint.adb") use "pprint"; + for Executable ("rembero.adb") use "rembero"; + for Executable ("trees.adb") use "trees"; for Default_Switches ("Ada") use Common.Builder'Default_Switches ("Ada"); |