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

1 files changed, 96 insertions, 28 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);