Iterative deepening depth first search as a complete (?) search method

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;
+
+
diff --git a/tests.gpr b/tests.gpr
index 8dc84f9..d580429 100644
--- a/tests.gpr
+++ b/tests.gpr
@@ -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");