sources に出現せず他の述語でも使われていないΔ述語を除去するようにした

bin/dl2u.ml

@@ -9,9 +9,9 @@ let sort rules =
   | Ok rules ->
       ok rules
 
-let simplify rules =
+let simplify rules sources =
   let open Result in
-  match Simplification.simplify rules with
+  match Simplification.simplify rules sources with
   | Error err ->
       error @@ Simplification.string_of_error err
   | Result.Ok rules ->
@@ -33,7 +33,7 @@ let convert ast =
 let main (ast : Expr.expr) =
   let open ResultMonad in
   sort ast.rules >>= fun rules ->
-  simplify rules >>= fun rules ->
+  simplify rules ast.sources >>= fun rules ->
   let ast = { ast with rules = rules } in
   convert ast
 

bin/simplification.ml

@@ -9,11 +9,12 @@ let _ =
     let lexbuf = Lexing.from_channel chan in
     let ast = Parser.main Lexer.token lexbuf in
     let rules = ast.rules in
+    let sources = ast.sources in
     match Inlining.sort_rules rules with
     | Result.Error err ->
       print_endline @@ Inlining.string_of_error err
     | Result.Ok rules ->
-      match Simplification.simplify rules with
+      match Simplification.simplify rules sources with
       | Result.Error err ->
         print_endline @@ Simplification.string_of_error err
       | Result.Ok rules ->

examples/simplification3_1.dl

@@ -0,0 +1,8 @@
+source ps('A':int, 'B':int).
+view pv('A':int).
+-ps(A, B) :- ps(A, B) , ps(A, GENV9) , A = 1 , A <> 4.
+-pv(GENV1) :- ps(GENV1, GENV7) , GENV1 = 1 , GENV1 <> 4.
++ps(A, B) :- A = 4 , ps(GENV10, GENV11) , GENV10 = 1 , GENV10 <> 4 , not ps(A, GENV1) , ps(GENV2, B) , ps(GENV2, GENV12) , GENV2 = 1 , GENV2 <> 4.
++ps(A, B) :- A = 4 , ps(GENV13, GENV14) , GENV13 = 1 , GENV13 <> 4 , not ps(A, GENV3) , not -ps(GENV4, GENV5) , B = -100.
++pv(GENV1) :- GENV1 = 4 , ps(GENV1_2, GENV8) , GENV1_2 = 1 , GENV1_2 <> 4.
+pv(A) :- ps(A, GENV6).

examples/simplification3_2.dl

@@ -0,0 +1,14 @@
+source b('B':int, 'C':int).
+source a('A':int, 'B':int).
+view v('A':int, 'B':int, 'C':int).
+-a(A, B) :- a(A, B) , not __updated__v(A, B, GENV1).
+-b(B, C) :- b(B, C) , a(GENV2, B) , b(B, GENV3) , not -v(GENV2, B, GENV3) , not __updated__v(GENV4, B, C).
+-b(B, C) :- b(B, C) , +v(GENV2, B, GENV3) , not __updated__v(GENV4, B, C).
+-v(GENV1, GENV2, GENV3) :- a(GENV1, GENV2) , b(GENV2, GENV3) , GENV2 = 30 , GENV2 <> 60.
++a(A, B) :- a(A, B) , b(B, GENV5) , not -v(A, B, GENV5) , not a(A, B).
++a(A, B) :- +v(A, B, GENV5) , not a(A, B).
++b(B, C) :- a(GENV6, B) , b(B, C) , not -v(GENV6, B, C) , not b(B, C).
++b(B, C) :- +v(GENV6, B, C) , not b(B, C).
+__updated__v(A, B, C) :- a(A, B) , b(B, C) , not -v(A, B, C).
+__updated__v(A, B, C) :- +v(A, B, C).
+v(A, B, C) :- a(A, B) , b(B, C).

src/simplification.ml

@@ -628,38 +628,36 @@ let resolve_undefined_predicates (imrules : intermediate_rule list) : intermedia
 module TableNameSet = Set.Make(String)
 
 
-let remove_unused_rules (imrules : intermediate_rule list) : intermediate_rule list =
-  List.fold_right (fun imrule (table_name_set, acc) ->
+let remove_unused_rules (sources : TableNameSet.t) (imrules : intermediate_rule list) : intermediate_rule list =
+  List.fold_right (fun imrule (pred_set, acc) ->
     let { positive_terms; negative_terms; _ } = imrule in
     let terms = PredicateMap.union (fun _ x _ -> Some x) positive_terms negative_terms in
-    let table_names =
+    let preds =
       terms
       |> PredicateMap.bindings
-      |> List.filter_map (fun (pred, _) ->
-        match pred with
-        | ImPred t ->
-            Some t
-        | ImDeltaInsert _
-        | ImDeltaDelete _ ->
-            None
-      )
+      |> List.map fst
     in
-    let new_table_name_set =
-      table_name_set
-      |> TableNameSet.add_seq @@ List.to_seq table_names
+    let new_pred_set =
+      pred_set
+      |> PredicateSet.add_seq @@ List.to_seq preds
     in
-    match imrule.head_predicate with
-    | ImDeltaInsert _
-    | ImDeltaDelete _ ->
-        (new_table_name_set, imrule :: acc)
-
-    | ImPred table_name when table_name_set |> TableNameSet.mem table_name ->
-        (new_table_name_set, imrule :: acc)
+    let pred = imrule.head_predicate in
+    match pred with
+    | ImDeltaInsert table_name
+    | ImDeltaDelete table_name ->
+        (* Leave delta pred only if it is a predicate on sources or is used from another predicate. *)
+        if TableNameSet.mem table_name sources || PredicateSet.mem pred pred_set then
+          (new_pred_set, imrule :: acc)
+        else
+          (pred_set, acc)
 
     | ImPred _ ->
-        (table_name_set, acc)
+        if pred_set |> PredicateSet.mem pred then
+          (new_pred_set, imrule :: acc)
+        else
+          (pred_set, acc)
 
-  ) imrules (TableNameSet.empty, [])
+  ) imrules (PredicateSet.empty, [])
   |> snd
 
 
@@ -783,7 +781,7 @@ let remove_duplicate_rules (rules : rule list) : rule list =
   with
   | (rules, _) -> rules
 
-let simplify (rules : rule list) : (rule list, error) result =
+let simplify (rules : rule list) (sources : source list) : (rule list, error) result =
   let open ResultMonad in
 
   (* Converts each rule to an intermediate rule (with unsatisfiable ones removed): *)
@@ -799,8 +797,14 @@ let simplify (rules : rule list) : (rule list, error) result =
   (* Removes predicates that are not defined: *)
   let imrules = imrules |> resolve_undefined_predicates in
 
+  let sources =
+    sources
+    |> List.map (fun (table_name, _) -> table_name)
+    |> TableNameSet.of_list
+  in
+
   (* Removes rules that are not used: *)
-  let imrules = imrules |> remove_unused_rules in
+  let imrules = imrules |> remove_unused_rules sources in
 
   (* Removes rules that have a contradicting body: *)
   let imrules = imrules |> List.filter (fun imrule -> not (has_contradicting_body imrule)) in

src/simplification.mli

@@ -3,6 +3,6 @@ open Expr
 
 type error
 
-val simplify : rule list -> (rule list, error) result
+val simplify : rule list -> source list -> (rule list, error) result
 
 val string_of_error : error -> string

test/ast2sql_operation_based_conversion_test.ml

@@ -209,7 +209,8 @@ let main () =
                   Printf.printf "Error: %s\n" (Inlining.string_of_error err);
                   assert false
               | Ok rules ->
-                match Simplification.simplify rules with
+                let sources = [ "a", []; "b", []; "v", [] ] in
+                match Simplification.simplify rules sources with
                 | Error err ->
                     Printf.printf "Error: %s\n" (Simplification.string_of_error err);
                     assert false