delay completion of a goal until whole underlying SCC is solved

datalog.opam

@@ -11,6 +11,7 @@ bug-reports: "https://github.com/c-cube/datalog/issues"
 depends: [
   "dune" {>= "2.7" & >= "2.7"}
   "ocaml" {>= "4.08"}
+  "containers" {>= "2.2"}
   "odoc" {with-doc}
   "mdx" {>= "1.3" & with-test}
 ]

dune-project

@@ -15,5 +15,6 @@
  (depends
   (dune ( >= "2.7" ))
   (ocaml ( >= "4.08" ))
+  (containers ( >= "2.2" ))
   (odoc :with-doc)
   (mdx (and ( >= "1.3" ) :with-test))))

src/top_down/Datalog_top_down.ml

@@ -1465,6 +1465,8 @@ module Make(Const : CONST) = struct
       mutable poss : (goal_entry * C.t) list; (* positive waiters *)
       mutable negs : (goal_entry * C.t) list; (* negative waiters *)
       mutable complete : bool;                (* goal evaluation completed? *)
+      dep_goals : goal_entry T.Tbl.t ;        (* forward edges: positive subgoals *)
+      mutable exit_fired : bool;              (* exit frame processed, pending completion (idempotence) *)
     } (** Root of the proof forest *)
 
     (** In a goal entry, [poss] and [negs] are other goals that depend
@@ -1487,6 +1489,14 @@ module Make(Const : CONST) = struct
       Subst.reset_renaming query.renaming;
       query.renaming
 
+    let[@inline] get_dep_goals (g:goal_entry) : _ T.Tbl.t = g.dep_goals
+
+    let all_deps_complete (g:goal_entry) : bool =
+      try
+        T.Tbl.iter (fun _ dep -> if not dep.complete then raise_notrace Exit) g.dep_goals;
+        true
+      with Exit -> false
+
     (* try to resolve fact with clause's first body literal *)
     let resolve ~query fact clause =
       match clause.C.body with
@@ -1522,7 +1532,7 @@ module Make(Const : CONST) = struct
         query.stack <- stack';
         (* close goal entry *)
         if not goal_entry.complete
-          then slg_complete ~query goal_entry;
+          then slg_exit ~query goal_entry;
         slg_main ~query
       | NewClause (goal_entry, clause, stack') ->
         query.stack <- stack';
@@ -1546,10 +1556,12 @@ module Make(Const : CONST) = struct
         (* new goal! insert it in the forest, and start solving it *)
         let goal_entry = {
           goal;
-          answers = T.Tbl.create 7;
+          answers = T.Tbl.create 8;
           poss = [];
           negs = [];
           complete = false;
+          dep_goals = T.Tbl.create 4;
+          exit_fired = false;
         } in
         TVariantTbl.add query.forest goal goal_entry;
         (* push the goal on stack so that it is solved *)
@@ -1631,6 +1643,12 @@ module Make(Const : CONST) = struct
       let subgoal_entry = slg_solve ~query subgoal in
       (* register for future answers *)
       subgoal_entry.poss <- (goal_entry, clause) :: subgoal_entry.poss;
+      (* record this as a forward dep if subgoal is still incomplete *)
+      if not subgoal_entry.complete
+      && not (T.Tbl.mem (get_dep_goals goal_entry) subgoal) then (
+        let tbl = get_dep_goals goal_entry in
+        T.Tbl.replace tbl subgoal subgoal_entry;
+      );
       (* use current answers *)
       T.Tbl.iter
         (fun ans () -> match resolve ~query ans clause with
@@ -1724,6 +1742,19 @@ module Make(Const : CONST) = struct
         groups;
       ()
 
+    (* Exit fires when local clause set is exhausted.
+       Defer actual completion until all positive deps are done. *)
+    and slg_exit ~query goal_entry =
+      goal_entry.exit_fired <- true;
+      try_complete ~query goal_entry
+
+    (* Complete only when Exit has fired AND all dep_goals are complete *)
+    and try_complete ~query goal_entry =
+      if goal_entry.exit_fired
+      && not goal_entry.complete
+      && all_deps_complete goal_entry
+      then slg_complete ~query goal_entry
+
     (* goal is completely evaluated, no more answers will arrive. *)
     and slg_complete ~query goal_entry =
       _debug (fun k->k "slg_complete %a" T.fmt goal_entry.goal);
@@ -1736,9 +1767,21 @@ module Make(Const : CONST) = struct
             (fun (goal, clause) -> slg_newclause ~query goal clause)
             goal_entry.negs
         end;
+      (* Notify distinct waiters: decrement their dep count, maybe unblock them *)
+      let seen = T.Tbl.create 4 in
+      List.iter (fun (waiter, _) ->
+        if not (T.Tbl.mem seen waiter.goal) then begin
+          T.Tbl.add seen waiter.goal ();
+          (* Remove completed dep from waiter's dep_goals *)
+
+          T.Tbl.remove waiter.dep_goals waiter.goal;
+          try_complete ~query waiter
+        end
+      ) goal_entry.poss;
       (* reclaim memory *)
       goal_entry.negs <- [];
       goal_entry.poss <- [];
+      T.Tbl.clear goal_entry.dep_goals;
       ()
   end
 

src/top_down/dune

@@ -1,7 +1,7 @@
 (library
  (name datalog_top_down)
  (public_name datalog.top_down)
- (libraries datalog)
+ (libraries datalog containers.scc)
  (flags :standard -color always -safe-string -warn-error -a+8))
 
 (ocamllex

tests/clique10.expected

@@ -0,0 +1,11 @@
+  (7).
+  (9).
+  (4).
+  (8).
+  (10).
+  (2).
+  (3).
+  (5).
+  (6).
+  (1).
+  (0).

tests/dune

@@ -0,0 +1,56 @@
+
+(rule
+ (alias runtest)
+ (deps
+  (:file reg13.pl)
+  (:bin ../src/top_down_cli/topDownCli.exe))
+ (action
+  (progn
+   (with-stdout-to reg13.out
+    (run %{bin} -load %{file} "(X) :- result(a3, X)"))
+   (diff reg13.out reg13.expected))))
+
+(rule
+ (alias runtest)
+ (deps
+  (:file clique10.pl)
+  (:bin ../src/top_down_cli/topDownCli.exe))
+ (action
+  (progn
+   (with-stdout-to clique10.out
+    (run %{bin} -load %{file} "(X) :- reachable(0,X)"))
+   (diff clique10.out clique10.expected))))
+
+(rule
+ (alias runtest)
+ (deps
+  (:file graph10.pl)
+  (:bin ../src/top_down_cli/topDownCli.exe))
+ (action
+  (progn
+   (with-stdout-to graph10.out
+    (run %{bin} -load %{file} "(X) :- increasing(3,X)" -builtin))
+   (diff graph10.out graph10.expected))))
+
+(rule
+ (alias runtest)
+ (deps
+  (:file small.pl)
+  (:bin ../src/top_down_cli/topDownCli.exe))
+ (action
+  (progn
+   (with-stdout-to small.out
+    (run %{bin} -load %{file} "(X) :- ancestor(X,john)"))
+   (diff small.out small.expected))))
+
+(rule
+ (alias runtest)
+ (deps
+  (:file ship.pl)
+  (:bin ../src/top_down_cli/topDownCli.exe))
+ (action
+  (progn
+   (with-stdout-to ship.out
+    (run %{bin} -load %{file} "(P,C) :- ship_to(P,C)"))
+   (diff ship.out ship.expected))))
+

tests/graph10.expected

@@ -0,0 +1,7 @@
+  (7).
+  (9).
+  (4).
+  (8).
+  (10).
+  (6).
+  (5).

tests/reg13.expected

@@ -0,0 +1 @@
+  (a2).

tests/reg13.pl

@@ -0,0 +1,13 @@
+% Test case for issue #13: Top down query has incorrect/differing behavior
+% https://github.com/c-cube/datalog/issues/13
+
+foo(a1, a3).
+foo(a2, a3).
+
+fooAlso(X, Y) :- foo(X, Y).
+
+bar(a1, a2).
+
+baz(a3, X) :- fooAlso(X, a3), fooAlso(Y, a3), bar(X, Y).
+
+result(a3, X) :- fooAlso(X, a3), ~baz(a3, X).

tests/ship.expected

@@ -0,0 +1,5 @@
+  (flowers, San Francisco).
+  (sausage, munich).
+  (horse, seoul).
+  (bread, paris).
+  (tea, london).

tests/small.expected

@@ -0,0 +1,4 @@
+  (jean-jacques).
+  (mireille).
+  (alphonse).
+  (brad).