Merge remote-tracking branch 'upstream/master' into feat/dl2u_del2

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 None 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/inlining.ml

@@ -1,5 +1,13 @@
 open Birds
 
+let parse_inlining_mode arg =
+  if String.starts_with ~prefix:"+" arg then
+    Inlining.InliningPredType.Deltainsert, String.sub arg 1 (String.length arg - 1)
+  else if String.starts_with ~prefix:"-" arg then
+    Inlining.InliningPredType.Deltadelete, String.sub arg 1 (String.length arg - 1)
+  else
+    Inlining.InliningPredType.Pred, arg
+
 let _ =
   if Array.length Sys.argv < 2 then
     print_endline "Invalid arguments. File name must be passed."
@@ -9,7 +17,18 @@ let _ =
     let lexbuf = Lexing.from_channel chan in
     let ast = Parser.main Lexer.token lexbuf in
     let rules = ast.rules in
-    match Inlining.inline_rules rules with
+    let mode =
+      if Array.length Sys.argv < 3 then
+        Inlining.All
+      else
+        let target =
+          Sys.argv.(2)
+          |> parse_inlining_mode
+          |> Inlining.TableNameSet.singleton
+        in
+        Inlining.Just target
+    in
+    match Inlining.inline_rules mode rules with
     | Result.Error err ->
       print_endline @@ Inlining.string_of_error err
     | Result.Ok rules ->

bin/simplification.ml

@@ -1,5 +1,11 @@
 open Birds
 
+let build_view ast =
+  if Array.length Sys.argv >= 3 && Sys.argv.(2) = "--prepare" then
+    ast.Expr.view
+  else
+    None
+
 let _ =
   if Array.length Sys.argv < 2 then
     print_endline "Invalid arguments. File name must be passed."
@@ -9,11 +15,13 @@ 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
+    let view = build_view ast 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 view sources with
       | Result.Error err ->
         print_endline @@ Simplification.string_of_error err
       | Result.Ok rules ->

examples/inlining4.dl

@@ -0,0 +1,7 @@
+a(X) :- X = 1.
+a(X) :- X = 2.
+
+b(X) :- X = 1.
+b(X) :- X = 2.
+
+f(X) :- a(X), NOT b(X).

examples/inlining5.dl

@@ -0,0 +1,6 @@
+a(X) :- X = 1.
+a(X) :- X = 2.
++a(X) :- a(X), X = 1.
++a(X) :- a(X), X = 2.
+
++f(X) :- +a(X).

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).

examples/simplification_prepare1.dl

@@ -0,0 +1,5 @@
+source x('A':int).
+view v('A':int).
+
++x(A) :- x(A), v(A), A <> 42.
+-x(A) :- +x(A), -v(A).

examples/simplification_prepare2.dl

@@ -0,0 +1,5 @@
+source x('A':int).
+view v('A':int).
+
++x(A) :- x(A), v(A), A <> 42.
+-x(A) :- +x(A), +v(A).

examples/simplification_prepare3.dl

@@ -0,0 +1,13 @@
+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).
++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).

examples/simplification_prepare4.dl

@@ -0,0 +1,10 @@
+source projs('A':int, 'B':string).
+view projv('A':int).
+-projs(A, B) :- projs(A, B) , -projv(A).
++projs(A, B) :- projs(A, GENV7) , not -projv(A) , not projs(A, GENV1) , not -projs(GENV2, GENV3) , B = 'a'.
++projs(A, B) :- projs(A, GENV8) , not -projv(A) , not projs(A, GENV4) , projs(GENV5, B) , -projv(GENV5).
++projs(A, B) :- +projv(A) , not projs(A, GENV1) , not -projs(GENV2, GENV3) , B = 'a'.
++projs(A, B) :- +projv(A) , not projs(A, GENV4) , projs(GENV5, B) , -projv(GENV5).
+__updated__projv(A) :- projs(A, GENV6) , not -projv(A).
+__updated__projv(A) :- +projv(A).
+projv(A) :- projs(A, B).

examples/simplification_prepare5.dl

@@ -0,0 +1,13 @@
+source uniona('NAME':string).
+source unionb('NAME':string).
+source uniono('NAME':string, 'TP':string).
+view unionview('NAME':string, 'TP':string).
+-uniona(N) :- uniona(N) , -unionview(N, T) , T = 'A'.
+-unionb(N) :- unionb(N) , -unionview(N, T) , T = 'B'.
+-uniono(N, T) :- uniono(N, T) , -unionview(N, T).
++uniona(N) :- +unionview(N, T) , not uniona(N) , T = 'A' , not uniono(N, T).
++unionb(N) :- +unionview(N, T) , not unionb(N) , T = 'B' , not uniono(N, T).
++uniono(N, T) :- +unionview(N, T) , not uniono(N, T) , not T = 'A' , not T = 'B'.
+unionview(N, T) :- uniona(N) , T = 'A'.
+unionview(N, T) :- unionb(N) , T = 'B'.
+unionview(N, T) :- uniono(N, T).

src/inlining.ml

@@ -2,6 +2,37 @@
 open Expr
 open Utils
 
+module InliningPredType = struct
+  type t =
+    | Pred
+    | Deltainsert
+    | Deltadelete
+
+  let compare (type1 : t) (type2 : t) : int =
+    match (type1, type2) with
+    | (Pred, Pred)               -> 0
+    | (Pred, _)                  -> 1
+    | (_, Pred)                  -> -1
+    | (Deltainsert, Deltainsert) -> 0
+    | (Deltainsert, _)           -> 1
+    | (_, Deltainsert)           -> -1
+    | (Deltadelete, Deltadelete) -> 0
+end
+
+module TableNameSet = Set.Make(struct
+  type t = InliningPredType.t * string
+
+  let compare (type1, name1) (type2, name2) =
+    match InliningPredType.compare type1 type2 with
+    | 0 -> String.compare name1 name2
+    | c -> c
+end)
+
+(** Select whether all predicates should be inlining or only certain predicates should be inlining. *)
+type inlining_mode =
+  | All
+  | Just of TableNameSet.t
+
 
 (** The prefix used for variables generated during inlining. *)
 let generated_variable_prefix = "GENV"
@@ -438,14 +469,24 @@ let negate_rule_abstractions (state : state) (ruleabss : rule_abstraction list)
           |> List.map (fun body -> { binder; body })
         )
 
+let is_inlined (mode : inlining_mode) (pred : intermediate_predicate) : bool =
+  match mode with
+  | All -> true
+  | Just tables -> tables |> TableNameSet.mem (
+    match pred with
+    | ImPred table -> InliningPredType.Pred, table
+    | ImDeltaInsert table -> InliningPredType.Deltainsert, table
+    | ImDeltaDelete table -> InliningPredType.Deltadelete, table
+  )
+
 (** `inline_rule_abstraction state improg_inlined ruleabs` performs inlining of `ruleabs`
     by using `improg_inlined`, which consists of "already inlined" definitions. *)
-let inline_rule_abstraction (state : state) (improg_inlined : intermediate_program) (ruleabs : rule_abstraction) : (state * rule_abstraction list, error) result =
+let inline_rule_abstraction (state : state) (mode : inlining_mode) (improg_inlined : intermediate_program) (ruleabs : rule_abstraction) : (state * rule_abstraction list, error) result =
   let open ResultMonad in
   let { binder; body } = ruleabs in
   body |> foldM (fun ((state, accs) : state * (intermediate_clause list) list) (clause : intermediate_clause) ->
     match clause with
-    | ImPositive (impred, imargs) ->
+    | ImPositive (impred, imargs) when is_inlined mode impred ->
         begin
           match improg_inlined |> PredicateMap.find_opt impred with
           | Some ruleabsset ->
@@ -501,7 +542,7 @@ let inject_rule (impred : intermediate_predicate) (ruleabs : rule_abstraction) :
   let terms = body |> List.map inject_clause in
   (rterm, terms)
 
-let inline_rules (rules : rule list) : (rule list, error) result =
+let inline_rules (mode : inlining_mode) (rules : rule list) : (rule list, error) result =
   let open ResultMonad in
 
   (* Converts rules into intermediate ones
@@ -519,7 +560,7 @@ let inline_rules (rules : rule list) : (rule list, error) result =
   sorted_rules |> foldM (fun (state, improg_inlined) (impred, ruleabsset) ->
     let ruleabss = RuleAbstractionSet.elements ruleabsset in
     ruleabss |> foldM (fun (state, ruleabss_inlined) ruleabs ->
-      ruleabs |> inline_rule_abstraction state improg_inlined >>= fun (state, ruleabss_inlined_new) ->
+      ruleabs |> inline_rule_abstraction state mode improg_inlined >>= fun (state, ruleabss_inlined_new) ->
       return (state, List.append ruleabss_inlined ruleabss_inlined_new)
       ) (state, []) >>= fun (state, ruleabss_inlined) ->
     return (state, improg_inlined |> PredicateMap.add impred (RuleAbstractionSet.of_list ruleabss_inlined))

src/simplification.ml

@@ -585,7 +585,7 @@ let rec simplify_rule_recursively (imrule1 : intermediate_rule) : intermediate_r
     simplify_rule_recursively imrule2
 
 
-let resolve_undefined_predicates (imrules : intermediate_rule list) : intermediate_rule list =
+let resolve_undefined_predicates (view : PredicateSet.t) (imrules : intermediate_rule list) : intermediate_rule list =
   imrules
   |> List.fold_left (fun (preds_set, acc) imrule ->
     let { head_predicate; positive_terms; negative_terms; _ } = imrule in
@@ -620,46 +620,44 @@ let resolve_undefined_predicates (imrules : intermediate_rule list) : intermedia
         let preds_set = preds_set |> PredicateSet.add head_predicate in
         let imrule = { imrule with positive_terms; negative_terms } in
         (preds_set, imrule :: acc)
-  ) (PredicateSet.empty, [])
+  ) (view, [])
   |> snd
   |> List.rev
 
 
 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) (view : PredicateSet.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 (view, [])
   |> 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) (view : view option) (sources : source list) : (rule list, error) result =
   let open ResultMonad in
 
   (* Converts each rule to an intermediate rule (with unsatisfiable ones removed): *)
@@ -796,11 +794,23 @@ let simplify (rules : rule list) : (rule list, error) result =
   (* Performs per-rule simplification: *)
   let imrules = imrules |> List.map simplify_rule_recursively in
 
+  let view =
+    match view with
+    | None      -> PredicateSet.empty
+    | Some (view, _) -> PredicateSet.of_list [ImDeltaInsert view; ImDeltaDelete view]
+  in
+
   (* Removes predicates that are not defined: *)
-  let imrules = imrules |> resolve_undefined_predicates in
+  let imrules = imrules |> resolve_undefined_predicates view 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 view 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 -> view option -> 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 None sources with
                 | Error err ->
                     Printf.printf "Error: %s\n" (Simplification.string_of_error err);
                     assert false