Evaluation algorithm changed to inverted interleaved depth first search

1 files changed, 49 insertions, 76 deletions

diff --git a/src/kompsos-collector.ads b/src/kompsos-collector.ads
index ac451c2..da3c592 100644
--- a/src/kompsos-collector.ads
+++ b/src/kompsos-collector.ads
@@ -8,6 +8,7 @@
 
 private with
 
+    Ada.Containers.Hashed_Maps,
     Ada.Containers.Vectors,
     Ada.Finalization;
 
@@ -31,108 +32,80 @@ package Kompsos.Collector is
            (Default : in State)
         return State;
 
-    procedure Reset;
-
 
 private
 
 
-    type Goal_Access is access all Goal;
-    type Constant_Goal_Access is access constant Goal;
-
-    type Graph_Access is access all Goal_Graph;
-    type Constant_Graph_Access is access constant Goal_Graph;
-
-
-
-    type Eval_Data (Kind : Node_Kind := Unify_Node) is record
-        case Kind is
-        when Unify_Node =>
-            Uni_Offset : Long_Natural  := 0;
-        when Disjunct_Node =>
-            Dis_Flag   : Boolean       := True;
-            Dis_Next1  : Long_Positive := 1;
-            Dis_Next2  : Long_Positive := 1;
-            Dis_Gone1  : Boolean       := False;
-            Dis_Gone2  : Boolean       := False;
-        when Conjunct_Node =>
-            Con_From   : Long_Positive := 1;
-            Con_Base   : State_Access  := null;
-            Con_Part   : Goal_Access   := null;
-            Con_Next   : Long_Positive := 1;
-            Con_Gone   : Boolean       := False;
-        when Recurse_Node =>
-            Rec_Next   : Long_Positive := 1;
-            Rec_Gone   : Boolean       := False;
-        end case;
-    end record;
+    --  Interleaved Graph Inversion  --
 
+    package Positive_Vectors is new Ada.Containers.Vectors
+       (Index_Type   => Positive,
+        Element_Type => Positive);
 
+    subtype Disjuncts_Chosen is Positive_Vectors.Vector;
 
-    type Cached_State is record
-        Used : Positive     := 1;
-        Data : State_Access := null;
-    end record;
-
-    package State_Vectors is new Ada.Containers.Vectors
-       (Index_Type   => Long_Positive,
-        Element_Type => Cached_State);
+    function "<"
+           (Left, Right : in Disjuncts_Chosen)
+        return Boolean;
 
-    type Cache_Entry is record
-        Keep : Boolean              := False;
-        Data : State_Vectors.Vector := State_Vectors.Empty_Vector;
+    type Parent_Arrow is record
+        Node  : Graph_Component_Access;
+        Order : Disjuncts_Chosen;
     end record;
 
-    type Cache_Entry_Access is access Cache_Entry;
-
-
+    function "<"
+           (Left, Right : in Parent_Arrow)
+        return Boolean;
 
-    type Book_Node;
+    package Parent_Arrow_Vectors is new Ada.Containers.Vectors
+       (Index_Type   => Positive,
+        Element_Type => Parent_Arrow);
 
-    type Book_Node_Access is access Book_Node;
+    subtype Disjuncts_Passed is Natural;
 
-    type Book_Node is record
-        Data  : Eval_Data;
-        Cache : Cache_Entry_Access := null;
-        Next1 : Book_Node_Access   := null;
-        Next2 : Book_Node_Access   := null;
+    type Node_Upwards is record
+        Depth   : Disjuncts_Passed;
+        Parents : Parent_Arrow_Vectors.Vector;
     end record;
 
+    package Upwards_Vectors is new Ada.Containers.Vectors
+       (Index_Type   => Positive,
+        Element_Type => Node_Upwards);
 
+    function Graph_Component_Access_Hash
+           (Key : in Graph_Component_Access)
+        return Ada.Containers.Hash_Type;
 
-    --  Used to keep track of and connect up bookkeeping nodes corresponding to
-    --  graph nodes with more than one parent, so as to avoid ending up with an
-    --  exponential tree instead of the desired directed acyclic graph.
+    package Upwards_Maps is new Ada.Containers.Hashed_Maps
+       (Key_Type        => Graph_Component_Access,
+        Element_Type    => Positive,
+        Hash            => Graph_Component_Access_Hash,
+        Equivalent_Keys => "=");
 
-    type Loose_Book is record
-        Used : Positive               := 1;
-        Ptr  : Graph_Component_Access := null;
-        Book : Book_Node_Access       := null;
-    end record;
 
-    package Loose_Book_Vectors is new Ada.Containers.Vectors
-       (Index_Type   => Long_Positive,
-        Element_Type => Loose_Book);
+    --  Conjunct Expansion  --
 
-    package Book_Node_Vectors is new Ada.Containers.Vectors
-       (Index_Type   => Long_Positive,
-        Element_Type => Book_Node_Access);
+    type Goal_Access is access all Goal;
 
+    package Goal_Access_Vectors is new Ada.Containers.Vectors
+       (Index_Type   => Positive,
+        Element_Type => Goal_Access);
 
 
-    procedure Reset
-           (Ptr  : in     Graph_Component_Access;
-            Book : in out Book_Node_Access);
+    --  Upwards Depth First Search  --
 
-    function Get_Next
-           (Ptr    : in     Constant_Graph_Access;
-            Book   : in out Book_Node_Access;
-            Base   : in     State;
-            Index  : in     Long_Positive;
-            Result :    out State)
-        return Boolean;
+    type Breadcrumb is record
+        Choice_Node : Graph_Component_Access;
+        Option      : Positive;
+        State_Size  : Long_Natural;
+    end record;
+
+    package Breadcrumb_Vectors is new Ada.Containers.Vectors
+       (Index_Type   => Positive,
+        Element_Type => Breadcrumb);
 
 
+    --  Cleanup  --
 
     type Collector_Final_Controller is new Ada.Finalization.Limited_Controlled with null record;