Removed free logic Variable tracking in States, removed Fresh_Node and Static_Node from Goal graphs

5 files changed, 45 insertions, 138 deletions

diff --git a/src/kompsos-collector.adb b/src/kompsos-collector.adb
index e8314ff..7ccdb57 100644
--- a/src/kompsos-collector.adb
+++ b/src/kompsos-collector.adb
@@ -58,32 +58,13 @@ package body Kompsos.Collector is
 
     --  Unification  --
 
-    function Fully_Contains
-           (This : in State;
-            Item : in Term'Class)
-        return Boolean is
+    procedure Walk
+           (This : in     State;
+            Item : in out Term) is
     begin
-        case Item.Kind is
-        when Null_Term | Atom_Term =>
-            return True;
-        when Var_Term =>
-            return This.LVars.Contains (Item.Var);
-        when Pair_Term =>
-            return Fully_Contains (This, Item.Left) and then Fully_Contains (This, Item.Right);
-        end case;
-    end Fully_Contains;
-
-
-    function Walk
-           (This : in State;
-            Item : in Term'Class)
-        return Term'Class is
-    begin
-        if Item.Kind = Var_Term and then This.Subst.Contains (Item.Var) then
-            return Walk (This, This.Subst.Element (Item.Var));
-        else
-            return Item;
-        end if;
+        while Item.Kind = Var_Term and then This.Actual.Contains (Item.Var) loop
+            Item := This.Actual.Element (Item.Var);
+        end loop;
     end Walk;
 
 
@@ -93,20 +74,12 @@ package body Kompsos.Collector is
             Extended    :    out State)
         return Boolean
     is
-        Real_Left  : Term'Class := Left;
-        Real_Right : Term'Class := Right;
+        Real_Left  : Term := Term (Left);
+        Real_Right : Term := Term (Right);
     begin
-        --  Check for Variable validity with respect to State
-        pragma Assert (Fully_Contains (Potential, Real_Left));
-        pragma Assert (Fully_Contains (Potential, Real_Right));
-
         --  Resolve Variable substitution
-        if Left.Kind = Var_Term then
-            Real_Left := Walk (Potential, Real_Left);
-        end if;
-        if Right.Kind = Var_Term then
-            Real_Right := Walk (Potential, Real_Right);
-        end if;
+        Walk (Potential, Real_Left);
+        Walk (Potential, Real_Right);
 
         --  Unify equal Variable/Atom/Null Terms
         if (Real_Left.Kind = Var_Term and then
@@ -124,12 +97,12 @@ package body Kompsos.Collector is
         --  Unify Variable and other Terms by introducing a new substitution
         if Real_Left.Kind = Var_Term then
             Extended := Potential;
-            Extended.Subst.Insert (Real_Left.Var, Term (Real_Right));
+            Extended.Actual.Insert (Real_Left.Var, Real_Right);
             return True;
         end if;
         if Real_Right.Kind = Var_Term then
             Extended := Potential;
-            Extended.Subst.Insert (Real_Right.Var, Term (Real_Left));
+            Extended.Actual.Insert (Real_Right.Var, Real_Left);
             return True;
         end if;
 
@@ -139,11 +112,7 @@ package body Kompsos.Collector is
                 Do_Unify (Extended, Real_Left.Right, Real_Right.Right, Extended);
         end if;
 
-        --  Not sure how things get here, but if all else fails
-        return False;
-
-    exception
-    when Ada.Assertions.Assertion_Error =>
+        --  Otherwise unification fails
         return False;
     end Do_Unify;
 
@@ -179,10 +148,6 @@ package body Kompsos.Collector is
         Cache_Memo.Exclude (Ptr.Actual);
 
         case Ptr.Actual.Kind is
-        when Static_Node =>
-            return;
-        when Fresh_Node =>
-            Reset (Ptr.Actual.Frs_Goal'Unchecked_Access);
         when Unify_Node =>
             Book.Exclude (Ptr.Actual);
             Reset (Ptr.Actual.Uni_Goal'Unchecked_Access);
@@ -221,22 +186,6 @@ package body Kompsos.Collector is
         return Boolean is
     begin
         case Ptr.Kind is
-        when Static_Node =>
-            if Index = 1 then
-                Result := Base;
-                return True;
-            else
-                return False;
-            end if;
-
-        when Fresh_Node =>
-            if Get_Next (Ptr.Frs_Goal'Unchecked_Access, Base, Index, Result) then
-                Result.LVars.Append (Ptr.Frs_Var);
-                return True;
-            else
-                return False;
-            end if;
-
         when Unify_Node =>
             if not Book.Contains (Ptr) then
                 Book.Insert (Ptr, (Kind => Unify_Data, others => <>));
@@ -359,6 +308,7 @@ package body Kompsos.Collector is
                 Result)
             loop
                 Reset (Constant_Goal_Access (Book.Element (Ptr).Con_Part));
+                Book (Ptr).Con_From := Book.Element (Ptr).Con_From + 1;
                 if Get_Next
                    (Ptr.Con_Goal'Unchecked_Access,
                     Base,
@@ -367,7 +317,6 @@ package body Kompsos.Collector is
                 then
                     Book (Ptr).Con_Base.all := Result;
                     Book (Ptr).Con_Next := 1;
-                    Book (Ptr).Con_From := Book.Element (Ptr).Con_From + 1;
                 else
                     Book (Ptr).Con_Gone := True;
                     Free (Book (Ptr).Con_Part);
@@ -382,7 +331,7 @@ package body Kompsos.Collector is
             if not Book.Contains (Ptr) then
                 Book.Insert (Ptr, (Kind => Recurse_Data, others => <>));
                 if Ptr.Rec_Goal.Actual = null then
-                    Book (Ptr).Rec_Gone := True;
+                    Book (Ptr).Rec_Cache := False;
                 elsif not Cache_Memo.Contains (Ptr.Rec_Goal.Actual) then
                     Cache_Memo.Insert (Ptr.Rec_Goal.Actual, State_Vectors.Empty_Vector);
                 end if;
@@ -420,8 +369,15 @@ package body Kompsos.Collector is
             Result :    out State)
         return Boolean is
     begin
-        if Ptr = null or else Ptr.Actual = null then
+        if Ptr = null then
             return False;
+        elsif Ptr.Actual = null then
+            if Index = 1 then
+                Result := Base;
+                return True;
+            else
+                return False;
+            end if;
         elsif Cache_Memo.Contains (Ptr.Actual) and then
             Index <= Cache_Memo (Ptr.Actual).Last_Index
         then
@@ -429,7 +385,7 @@ package body Kompsos.Collector is
             return True;
         else
             return Found : constant Boolean := Do_Get_Next (Ptr.Actual, Base, Index, Result) do
-                if Found and Ptr.Actual.Counter > 1 and Ptr.Actual.Kind /= Static_Node then
+                if Found and Ptr.Actual.Counter > 1 then
                     if not Cache_Memo.Contains (Ptr.Actual) then
                         Cache_Memo.Insert (Ptr.Actual, State_Vectors.Empty_Vector);
                     end if;
diff --git a/src/kompsos-collector.ads b/src/kompsos-collector.ads
index cbe8dd7..4ee9402 100644
--- a/src/kompsos-collector.ads
+++ b/src/kompsos-collector.ads
@@ -61,7 +61,7 @@ private
             Dis_Gone1  : Boolean       := False;
             Dis_Gone2  : Boolean       := False;
         when Conjunct_Data =>
-            Con_From   : Long_Positive := 2;  --  Number one will be obtained by Get_Next already
+            Con_From   : Long_Positive := 1;
             Con_Base   : State_Access  := null;
             Con_Part   : Goal_Access   := null;
             Con_Next   : Long_Positive := 1;
@@ -84,6 +84,12 @@ private
     overriding procedure Finalize
            (This : in out Managed_Map);
 
+
+
+    package State_Vectors is new Ada.Containers.Vectors
+       (Index_Type   => Long_Positive,
+        Element_Type => State);
+
     package Cache_Maps is new Ada.Containers.Ordered_Maps
        (Key_Type     => Goal_Component_Access,
         Element_Type => State_Vectors.Vector,
diff --git a/src/kompsos-pretty_print.adb b/src/kompsos-pretty_print.adb
index c888e13..3171164 100644
--- a/src/kompsos-pretty_print.adb
+++ b/src/kompsos-pretty_print.adb
@@ -94,22 +94,11 @@ package body Kompsos.Pretty_Print is
     is
         Result : SU.Unbounded_String;
     begin
-        SU.Append (Result, Latin.HT & "Variables:");
-        if Item.LVars.Is_Empty then
-            SU.Append (Result, " N/A" & Latin.LF);
+        if Item.Actual.Is_Empty then
+            SU.Append (Result, Latin.HT & "N/A" & Latin.LF);
         else
-            SU.Append (Result, Latin.LF);
-            for LVar of Item.LVars loop
-                SU.Append (Result, Latin.HT & Latin.HT & Image (LVar) & Latin.LF);
-            end loop;
-        end if;
-        SU.Append (Result, Latin.HT & "Substitution:");
-        if Item.Subst.Is_Empty then
-            SU.Append (Result, " N/A" & Latin.LF);
-        else
-            SU.Append (Result, Latin.LF);
-            for Iter in Item.Subst.Iterate loop
-                SU.Append (Result, Latin.HT & Latin.HT &
+            for Iter in Item.Actual.Iterate loop
+                SU.Append (Result, Latin.HT &
                     Image (Binding_Maps.Key (Iter)) & " => " &
                     Image (Binding_Maps.Element (Iter)) & Latin.LF);
             end loop;
@@ -175,18 +164,6 @@ package body Kompsos.Pretty_Print is
         Nodes.Insert (This.Actual, Next);
         Next := Next + 1;
         case This.Actual.Kind is
-        when Static_Node =>
-            SU.Append (Result, Latin.HT &
-                "n" & Image (Nodes.Element (This.Actual)) & " [label=""static""];" & Latin.LF);
-        when Fresh_Node =>
-            SU.Append (Result, Latin.HT &
-                "n" & Image (Nodes.Element (This.Actual)) & " [label=""fresh""];" & Latin.LF);
-            Do_Structure_DOT (This.Actual.Frs_Goal, Nodes, Next, Result);
-            if Nodes.Contains (This.Actual.Frs_Goal.Actual) then
-                SU.Append (Result, Latin.HT &
-                    "n" & Image (Nodes.Element (This.Actual)) & " -> " &
-                    "n" & Image (Nodes.Element (This.Actual.Frs_Goal.Actual)) & ";" & Latin.LF);
-            end if;
         when Unify_Node =>
             SU.Append (Result, Latin.HT &
                 "n" & Image (Nodes.Element (This.Actual)) & " [label=""unify""];" & Latin.LF);
diff --git a/src/kompsos.adb b/src/kompsos.adb
index 7054714..080683b 100644
--- a/src/kompsos.adb
+++ b/src/kompsos.adb
@@ -254,17 +254,9 @@ package body Kompsos is
 
     function Fresh
            (This : in out Goal'Class)
-        return Term
-    is
-        My_Var : constant Variable := Next_Gen;
+        return Term is
     begin
-        return My_Term : constant Term := Term (T (My_Var)) do
-            This.Actual := new Goal_Component'(
-               (Kind     => Fresh_Node,
-                Counter  => 1,
-                Frs_Goal => Goal (This),
-                Frs_Var  => My_Var));
-        end return;
+        return Term (T (Next_Gen));
     end Fresh;
 
 
@@ -557,8 +549,8 @@ package body Kompsos is
         when Null_Term | Atom_Term =>
             return This;
         when Var_Term =>
-            if Subst.LVars.Contains (This.Var) and then Subst.Subst.Contains (This.Var) then
-                return Subst.Subst.Element (This.Var).Resolve (Subst);
+            if Subst.Actual.Contains (This.Var) then
+                return Subst.Actual.Element (This.Var).Resolve (Subst);
             else
                 return This;
             end if;
@@ -572,10 +564,10 @@ package body Kompsos is
            (Subst : in State)
         return Term is
     begin
-        if Subst.LVars.Is_Empty then
+        if Subst.Actual.Is_Empty then
             return Empty_Term;
         else
-            return Resolve (Term (T (Subst.LVars.First_Element)), Subst);
+            return Subst.Actual.First_Element.Resolve (Subst);
         end if;
     end Resolve_First;
 
diff --git a/src/kompsos.ads b/src/kompsos.ads
index 19cfeb8..32cfc24 100644
--- a/src/kompsos.ads
+++ b/src/kompsos.ads
@@ -415,7 +415,6 @@ private
 
 
 
-
     type Term_Component;
 
     type Term_Component_Access is access Term_Component;
@@ -464,28 +463,15 @@ private
 
 
 
-
-    package Variable_Vectors is new Ada.Containers.Vectors
-       (Index_Type   => Long_Positive,
-        Element_Type => Variable);
-
     package Binding_Maps is new Ada.Containers.Ordered_Maps
        (Key_Type     => Variable,
         Element_Type => Term);
 
     type State is record
-        LVars : Variable_Vectors.Vector;
-        Subst : Binding_Maps.Map;
+        Actual : Binding_Maps.Map;
     end record;
 
-    package State_Vectors is new Ada.Containers.Vectors
-       (Index_Type   => Long_Positive,
-        Element_Type => State);
-
-    Empty_State : constant State :=
-       (LVars => Variable_Vectors.Empty_Vector,
-        Subst => Binding_Maps.Empty_Map);
-
+    Empty_State : constant State := (Actual => Binding_Maps.Empty_Map);
 
 
 
@@ -515,9 +501,7 @@ private
     package Lazy_Holders is new Ada.Containers.Indefinite_Holders (Lazy_Data);
 
     type Node_Kind is
-       (Static_Node,
-        Fresh_Node,
-        Unify_Node,
+       (Unify_Node,
         Disjunct_Node,
         Conjunct_Node,
         Recurse_Node);
@@ -525,11 +509,6 @@ private
     type Goal_Component (Kind : Node_Kind) is limited record
         Counter : Natural;
         case Kind is
-        when Static_Node =>
-            null;
-        when Fresh_Node =>
-            Frs_Goal  : aliased Goal;
-            Frs_Var   : Variable;
         when Unify_Node =>
             Uni_Goal  : aliased Goal;
             Uni_Term1 : Term;
@@ -558,10 +537,7 @@ private
     overriding procedure Finalize
            (This : in out Goal);
 
-    Empty_Goal : constant Goal := (Ada.Finalization.Controlled with
-        Actual => new Goal_Component'(
-           (Kind    => Static_Node,
-            Counter => 1)));
+    Empty_Goal : constant Goal := (Ada.Finalization.Controlled with Actual => null);
 
 
 end Kompsos;