More complete IDDFS that resets counter when backtracking

2 files changed, 45 insertions, 6 deletions

diff --git a/src/kompsos-collector.adb b/src/kompsos-collector.adb
index b64d284..6e3d75d 100644
--- a/src/kompsos-collector.adb
+++ b/src/kompsos-collector.adb
@@ -32,9 +32,12 @@ package body Kompsos.Collector is
     Local_Cursor : Upwards_Maps.Cursor;
     Next_Pick    : Positive;
 
-    Conjunct_Count : Natural := 0;
-    Conjunct_Limit : Positive := Initial_Depth_Limit;
-    Already_Done   : Choice_Vector_Vectors.Vector;
+    Conjunct_Need_More    : Boolean  := False;
+    Conjunct_Count_Active : Boolean  := False;
+    Conjunct_Trail_Start  : Natural  := 0;
+    Conjunct_Count        : Natural  := 0;
+    Conjunct_Limit        : Positive := Initial_Depth_Limit;
+    Already_Done          : Choice_Vector_Vectors.Vector;
 
     Result      : State   := Within;
     State_Valid : Boolean := False;
@@ -304,6 +307,9 @@ package body Kompsos.Collector is
 
     procedure Reset_Position is
     begin
+        Conjunct_Need_More := False;
+        Conjunct_Count_Active := False;
+        Conjunct_Trail_Start := 0;
         Conjunct_Count := 0;
         Conjunct_Limit := Conjunct_Limit * 2;
         Walk_Trail.Clear;
@@ -333,6 +339,12 @@ package body Kompsos.Collector is
                 Truncate (Result, Crumb.State_Size);
                 Walk_Trail.Set_Length (Ada.Containers.Count_Type (Marker - 1));
                 Walk_Choices.Set_Length (Ada.Containers.Count_Type (Marker - 1));
+                if Conjunct_Count_Active and then Marker - 1 < Conjunct_Trail_Start then
+                    Conjunct_Count_Active := False;
+                    Conjunct_Trail_Start := 0;
+                    Conjunct_Count := 0;
+                    Conjunct_Limit := Conjunct_Limit * 2;
+                end if;
                 return True;  --  Backtracking success
             else
                 Marker := Marker - 1;
@@ -359,7 +371,7 @@ package body Kompsos.Collector is
                         State_Valid := True;
                         return;
                     elsif not Choose_Another_Way then
-                        if Conjunct_Count >= Conjunct_Limit then
+                        if Conjunct_Need_More then
                             Reset_Position;
                         else
                             State_Valid := False;
@@ -373,9 +385,15 @@ package body Kompsos.Collector is
                 loop
                     Ptr := Up_Vector (Upwards_Maps.Element (Local_Cursor)).Parents (Next_Pick).Node;
                     exit when Ptr.Kind /= Conjunct_Node;
+                    if not Conjunct_Count_Active then
+                        Conjunct_Count_Active := True;
+                        Conjunct_Trail_Start := Walk_Trail.Last_Index;
+                    end if;
                     if Conjunct_Count >= Conjunct_Limit then
                         if not Choose_Another_Way then
                             Reset_Position;
+                        else
+                            Conjunct_Need_More := True;
                         end if;
                     else
                         Expand_Conjunct (Ptr);
@@ -399,7 +417,7 @@ package body Kompsos.Collector is
                 --  If unification fails then backtrack if possible,
                 --  or otherwise reset if the Graph isn't exhausted
                 if not Choose_Another_Way then
-                    if Conjunct_Count > 0 then
+                    if Conjunct_Need_More then
                         Reset_Position;
                     else
                         State_Valid := False;
@@ -416,7 +434,7 @@ package body Kompsos.Collector is
     begin
         if Choose_Another_Way then
             Walk_Graph;
-        elsif Conjunct_Count >= Conjunct_Limit then
+        elsif Conjunct_Need_More then
             Reset_Position;
             Walk_Graph;
         else
diff --git a/test/complete.adb b/test/complete.adb
index 0890e8b..75aadf5 100644
--- a/test/complete.adb
+++ b/test/complete.adb
@@ -35,6 +35,14 @@ procedure Complete is
         return Disjunct (One, Two);
     end Fives;
 
+    function Simple
+           (This : in Goal;
+            Item : in Term'Class)
+        return Goal is
+    begin
+        return This.Unify (Item, 1);
+    end Simple;
+
 begin
 
     TIO.Put_Line ("This program will loop forever unless the implementation is using");
@@ -65,6 +73,19 @@ begin
 
     TIO.New_Line;
 
+    declare
+        Relation : Goal          := Empty_Goal;
+        Value    : constant Term := Relation.Fresh;
+    begin
+        Relation.Unify (Value, 9);
+        Relation := Fives (Relation, Value);
+        Relation.Disjunct (Empty_Goal.Conjunct (Simple'Access, Value));
+        TIO.Put_Line ("Value is " & Printer.Image (Value.Resolve (Relation.Run)) &
+            " after escaping Conjunct trap.");
+    end;
+
+    TIO.New_Line;
+
     TIO.Put_Line ("Test complete.");
 
 end Complete;