From 3b526860ba94a805cffca3966ff717b6afa4d9be Mon Sep 17 00:00:00 2001 From: cedretaber Date: Wed, 25 Sep 2024 20:26:52 +0900 Subject: [PATCH] =?UTF-8?q?simplification=20=E3=82=B3=E3=83=9E=E3=83=B3?= =?UTF-8?q?=E3=83=89=E3=81=AB=20`--prepare`=20=E3=82=AA=E3=83=97=E3=82=B7?= =?UTF-8?q?=E3=83=A7=E3=83=B3=E3=82=92=E8=BF=BD=E5=8A=A0=E3=81=97=E3=81=9F?= =?UTF-8?q?=20(#48)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * A view can be delta predicates with --prepare option. * Add a sample code. * Add some tests for simplification. --- bin/dl2u.ml | 2 +- bin/simplification.ml | 9 +- examples/simplification_prepare1.dl | 5 + examples/simplification_prepare2.dl | 5 + examples/simplification_prepare3.dl | 13 + examples/simplification_prepare4.dl | 10 + examples/simplification_prepare5.dl | 13 + src/simplification.ml | 20 +- src/simplification.mli | 2 +- ...ast2sql_operation_based_conversion_test.ml | 2 +- test/simplification_test.ml | 443 +++++++++++++++++- 11 files changed, 509 insertions(+), 15 deletions(-) create mode 100644 examples/simplification_prepare1.dl create mode 100644 examples/simplification_prepare2.dl create mode 100644 examples/simplification_prepare3.dl create mode 100644 examples/simplification_prepare4.dl create mode 100644 examples/simplification_prepare5.dl diff --git a/bin/dl2u.ml b/bin/dl2u.ml index c306e27..a8a4c42 100644 --- a/bin/dl2u.ml +++ b/bin/dl2u.ml @@ -11,7 +11,7 @@ let sort rules = let simplify rules sources = let open Result in - match Simplification.simplify rules sources with + match Simplification.simplify rules None sources with | Error err -> error @@ Simplification.string_of_error err | Result.Ok rules -> diff --git a/bin/simplification.ml b/bin/simplification.ml index e541c9b..f7b897c 100644 --- a/bin/simplification.ml +++ b/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." @@ -10,11 +16,12 @@ let _ = 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 sources with + match Simplification.simplify rules view sources with | Result.Error err -> print_endline @@ Simplification.string_of_error err | Result.Ok rules -> diff --git a/examples/simplification_prepare1.dl b/examples/simplification_prepare1.dl new file mode 100644 index 0000000..ade78a3 --- /dev/null +++ b/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). diff --git a/examples/simplification_prepare2.dl b/examples/simplification_prepare2.dl new file mode 100644 index 0000000..ddcceaf --- /dev/null +++ b/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). diff --git a/examples/simplification_prepare3.dl b/examples/simplification_prepare3.dl new file mode 100644 index 0000000..4b73a21 --- /dev/null +++ b/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). diff --git a/examples/simplification_prepare4.dl b/examples/simplification_prepare4.dl new file mode 100644 index 0000000..e6232e9 --- /dev/null +++ b/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). diff --git a/examples/simplification_prepare5.dl b/examples/simplification_prepare5.dl new file mode 100644 index 0000000..ec886ab --- /dev/null +++ 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). diff --git a/src/simplification.ml b/src/simplification.ml index 305f443..0d3c81c 100644 --- a/src/simplification.ml +++ b/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,7 +620,7 @@ 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 @@ -628,7 +628,7 @@ let resolve_undefined_predicates (imrules : intermediate_rule list) : intermedia module TableNameSet = Set.Make(String) -let remove_unused_rules (sources : TableNameSet.t) (imrules : intermediate_rule list) : intermediate_rule list = +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 @@ -657,7 +657,7 @@ let remove_unused_rules (sources : TableNameSet.t) (imrules : intermediate_rule else (pred_set, acc) - ) imrules (PredicateSet.empty, []) + ) imrules (view, []) |> snd @@ -781,7 +781,7 @@ let remove_duplicate_rules (rules : rule list) : rule list = with | (rules, _) -> rules -let simplify (rules : rule list) (sources : source 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): *) @@ -794,8 +794,14 @@ let simplify (rules : rule list) (sources : source list) : (rule list, error) re (* 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 @@ -804,7 +810,7 @@ let simplify (rules : rule list) (sources : source list) : (rule list, error) re in (* Removes rules that are not used: *) - let imrules = imrules |> remove_unused_rules sources 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 diff --git a/src/simplification.mli b/src/simplification.mli index bd2d54a..f109fa1 100644 --- a/src/simplification.mli +++ b/src/simplification.mli @@ -3,6 +3,6 @@ open Expr type error -val simplify : rule list -> source list -> (rule list, error) result +val simplify : rule list -> view option -> source list -> (rule list, error) result val string_of_error : error -> string diff --git a/test/ast2sql_operation_based_conversion_test.ml b/test/ast2sql_operation_based_conversion_test.ml index 4671368..5a401b9 100644 --- a/test/ast2sql_operation_based_conversion_test.ml +++ b/test/ast2sql_operation_based_conversion_test.ml @@ -210,7 +210,7 @@ let main () = assert false | Ok rules -> let sources = [ "a", []; "b", []; "v", [] ] in - match Simplification.simplify rules sources with + match Simplification.simplify rules None sources with | Error err -> Printf.printf "Error: %s\n" (Simplification.string_of_error err); assert false diff --git a/test/simplification_test.ml b/test/simplification_test.ml index 11a2f23..fe65f03 100644 --- a/test/simplification_test.ml +++ b/test/simplification_test.ml @@ -5,7 +5,7 @@ open Expr type test_case = { title : string; - input : rule list * source list; + input : rule list * view option * source list; expected : rule list; } @@ -16,12 +16,12 @@ type test_result = let run_test (test_case : test_case) = let open ResultMonad in - let rules, sources = test_case.input in + let rules, view, sources = test_case.input in match Inlining.sort_rules rules with | Error err -> return (Fail { expected = "no error when sorting rules."; got = Inlining.string_of_error err }) | Ok rules -> - Simplification.simplify rules sources >>= fun got -> + Simplification.simplify rules view sources >>= fun got -> let s_got = got |> List.map string_of_rule |> String.concat "; " in let s_expected = test_case.expected |> List.map string_of_rule |> String.concat "; " in if String.equal s_got s_expected then @@ -61,7 +61,7 @@ let main () = run_tests [ { title = "empty"; - input = [], []; + input = [], None, []; expected = []; }; { @@ -82,6 +82,7 @@ let main () = Equat (Equation ("=", Var rating, Const (Int 1))); ]); ], + None, [ "tracks", [] ]; expected = [ (* (1) simplified: @@ -118,6 +119,7 @@ let main () = Not (Pred ("tracks", [ NamedVar "V31"; NamedVar "V32"; NamedVar "V33"; album ])); ]); ], + None, [ "tracks", [] ]; expected = []; }; @@ -139,6 +141,7 @@ let main () = Equat (Equation ("=", Var (NamedVar "V6855"), Const (Int 1))); ]); ], + None, [ "albums", [] ]; expected = [ (* (7) simplified: @@ -173,6 +176,7 @@ let main () = Noneq (Equation ("=", Var rating, Const (Int 1))); ]); ], + None, [ "albums", [] ]; expected = [ (* (32) simplified: @@ -209,6 +213,7 @@ let main () = Not (Pred ("eed", [NamedVar "E"; NamedVar "D"])); ]); ], + None, [ "eed", []; "ed", [] ]; expected = [ (* Boolean body simplified: @@ -257,6 +262,7 @@ let main () = (Pred ("g", [NamedVar "X"]), [Equat (Equation ("=", (Var (NamedVar "X")), (Const (Int 1))))]); (Pred ("f", [NamedVar "X"]), [Equat (Equation ("=", (Var (NamedVar "X")), (Const (Int 1))))]); ], + None, [ "f", []; "g", []; "a", []; "b", []; "c", []; "d", [] ]; expected = [ (Deltadelete ("g", [NamedVar "X"]), [Rel (Pred ("g", [NamedVar "X"]))]); @@ -309,6 +315,7 @@ let main () = ]); (Pred ("v", [NamedVar "A"]), [Rel (Pred ("s", [NamedVar "A"; NamedVar "B"]))]); ], + None, [ "v", []; "s", [] ]; expected = [ (Deltainsert ("s", [NamedVar "A"; NamedVar "B"]), [ @@ -394,6 +401,7 @@ let main () = (Equat (Equation ("<>", Var (NamedVar "A"), Const (Int 4)))); ]); ], + None, ["ps", []]; expected = [ (* @@ -507,6 +515,7 @@ let main () = Not (Pred ("__updated__v", [NamedVar "A"; NamedVar "B"; NamedVar "GENV1"])) ]); ], + None, ["a", []; "b", []]; expected = [ (* @@ -543,5 +552,431 @@ let main () = Equat (Equation ("=", Var (NamedVar "GENV2"), Const (Int 30))) ]); ] + }; + (* --prepare *) + { + title = "--prepare option"; + input = [ + (* + source x('A':int). + view v('A':int). + + +x(A) :- x(A), v(A), A <> 42. + -x(A) :- +x(A), -v(A). + *) + (Deltainsert ("x", [NamedVar "A"]), [ + Rel (Pred ("x", [NamedVar "A"])); + Rel (Pred ("v", [NamedVar "A"])); + Equat (Equation ("<>", Var (NamedVar "A"), Const (Int 42))) + ]); + (Deltadelete ("x", [NamedVar "A"]), [ + Rel (Deltainsert ("x", [NamedVar "A"])); + Rel (Deltadelete ("v", [NamedVar "A"])) + ]); + ], + Some ("v", []), + ["x", []]; + expected = [ + (* + -x(A) :- -v(A) , +x(A). + +x(A) :- v(A) , x(A) , not A = 42. + *) + (Deltadelete ("x", [NamedVar "A"]), [ + Rel (Deltadelete ("v", [NamedVar "A"])); + Rel (Deltainsert ("x", [NamedVar "A"])) + ]); + (Deltainsert ("x", [NamedVar "A"]), [ + Rel (Pred ("v", [NamedVar "A"])); + Rel (Pred ("x", [NamedVar "A"])); + Noneq (Equation ("=", Var (NamedVar "A"), Const (Int 42))) + ]); + ] + }; + { + title = "Same input without --prepare option"; + input = [ + (* + source x('A':int). + view v('A':int). + + +x(A) :- x(A), v(A), A <> 42. + -x(A) :- +x(A), -v(A). + *) + (Deltainsert ("x", [NamedVar "A"]), [ + Rel (Pred ("x", [NamedVar "A"])); + Rel (Pred ("v", [NamedVar "A"])); + Equat (Equation ("<>", Var (NamedVar "A"), Const (Int 42))) + ]); + (Deltadelete ("x", [NamedVar "A"]), [ + Rel (Deltainsert ("x", [NamedVar "A"])); + Rel (Deltadelete ("v", [NamedVar "A"])) + ]); + ], + None, + ["x", []]; + expected = [ + (* + +x(A) :- v(A) , x(A) , not A = 42. + *) + (Deltainsert ("x", [NamedVar "A"]), [ + Rel (Pred ("v", [NamedVar "A"])); + Rel (Pred ("x", [NamedVar "A"])); + Noneq (Equation ("=", Var (NamedVar "A"), Const (Int 42))) + ]); + ] + }; + { + title = "--prepare option: join"; + input = [ + (* + 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). + *) + (* -a(A, B) :- a(A, B) , not __updated__v(A, B, GENV1). *) + (Deltadelete ("a", [NamedVar "A"; NamedVar "B"]), [ + Rel (Pred ("a", [NamedVar "A"; NamedVar "B"])); + Not (Pred ("__updated__v", [NamedVar "A"; NamedVar "B"; NamedVar "GENV1"])) + ]); + (* -b(B, C) :- b(B, C) , a(GENV2, B) , b(B, GENV3) , not -v(GENV2, B, GENV3) , not __updated__v(GENV4, B, C). *) + (Deltadelete ("b", [NamedVar "B"; NamedVar "C"]), [ + Rel (Pred ("b", [NamedVar "B"; NamedVar "C"])); + Rel (Pred ("a", [NamedVar "GENV2"; NamedVar "B"])); + Rel (Pred ("b", [NamedVar "B"; NamedVar "GENV3"])); + Not (Deltadelete ("v", [NamedVar "GENV2"; NamedVar "B"; NamedVar "GENV3"])); + Not (Pred ("__updated__v", [NamedVar "GENV4"; NamedVar "B"; NamedVar "C"])) + ]); + (* -b(B, C) :- b(B, C) , +v(GENV2, B, GENV3) , not __updated__v(GENV4, B, C). *) + (Deltadelete ("b", [NamedVar "B"; NamedVar "C"]), [ + Rel (Pred ("b", [NamedVar "B"; NamedVar "C"])); + Rel (Deltainsert ("v", [NamedVar "GENV2"; NamedVar "B"; NamedVar "GENV3"])); + Not (Pred ("__updated__v", [NamedVar "GENV4"; NamedVar "B"; NamedVar "C"])) + ]); + (* +a(A, B) :- a(A, B) , b(B, GENV5) , not -v(A, B, GENV5) , not a(A, B). *) + (Deltainsert ("a", [NamedVar "A"; NamedVar "B"]), [ + Rel (Pred ("a", [NamedVar "A"; NamedVar "B"])); + Rel (Pred ("b", [NamedVar "B"; NamedVar "GENV5"])); + Not (Deltadelete ("v", [NamedVar "A"; NamedVar "B"; NamedVar "GENV5"])); + Not (Pred ("a", [NamedVar "A"; NamedVar "B"])) + ]); + (* +a(A, B) :- +v(A, B, GENV5) , not a(A, B). *) + (Deltainsert ("a", [NamedVar "A"; NamedVar "B"]), [ + Rel (Deltainsert ("v", [NamedVar "A"; NamedVar "B"; NamedVar "GENV5"])); + Not (Pred ("a", [NamedVar "A"; NamedVar "B"])) + ]); + (* +b(B, C) :- a(GENV6, B) , b(B, C) , not -v(GENV6, B, C) , not b(B, C). *) + (Deltainsert ("b", [NamedVar "B"; NamedVar "C"]), [ + Rel (Pred ("a", [NamedVar "GENV6"; NamedVar "B"])); + Rel (Pred ("b", [NamedVar "B"; NamedVar "C"])); + Not (Deltadelete ("v", [NamedVar "GENV6"; NamedVar "B"; NamedVar "C"])); + Not (Pred ("b", [NamedVar "B"; NamedVar "C"])) + ]); + (* +b(B, C) :- +v(GENV6, B, C) , not b(B, C). *) + (Deltainsert ("b", [NamedVar "B"; NamedVar "C"]), [ + Rel (Deltainsert ("v", [NamedVar "GENV6"; NamedVar "B"; NamedVar "C"])); + Not (Pred ("b", [NamedVar "B"; NamedVar "C"])) + ]); + (* __updated__v(A, B, C) :- a(A, B) , b(B, C) , not -v(A, B, C). *) + (Pred ("__updated__v", [NamedVar "A"; NamedVar "B"; NamedVar "C"]), [ + Rel (Pred ("a", [NamedVar "A"; NamedVar "B"])); + Rel (Pred ("b", [NamedVar "B"; NamedVar "C"])); + Not (Deltadelete ("v", [NamedVar "A"; NamedVar "B"; NamedVar "C"])) + ]); + (* __updated__v(A, B, C) :- +v(A, B, C). *) + (Pred ("__updated__v", [NamedVar "A"; NamedVar "B"; NamedVar "C"]), [ + Rel (Deltainsert ("v", [NamedVar "A"; NamedVar "B"; NamedVar "C"])) + ]); + (* v(A, B, C) :- a(A, B) , b(B, C). *) + (Pred ("v", [NamedVar "A"; NamedVar "B"; NamedVar "C"]), [ + Rel (Pred ("a", [NamedVar "A"; NamedVar "B"])); + Rel (Pred ("b", [NamedVar "B"; NamedVar "C"])) + ]); + ], + Some ("v", []), + ["a", []; "b", []]; + expected = [ + (* + source a('A':int, 'B':int). + source b('B':int, 'C':int). + view v('A':int, 'B':int, 'C':int). + -a(A, B) :- a(A, B) , not __updated__v(A, B, _). + -b(B, C) :- +v(_, B, _) , b(B, C) , not __updated__v(_, B, C). + -b(B, C) :- a(GENV2, B) , b(B, C) , b(B, GENV3) , not -v(GENV2, B, GENV3) , not __updated__v(_, B, C). + __updated__v(A, B, C) :- +v(A, B, C). + __updated__v(A, B, C) :- a(A, B) , b(B, C) , not -v(A, B, C). + +b(B, C) :- +v(_, B, C) , not b(B, C). + +a(A, B) :- +v(A, B, _) , not a(A, B). + *) + (* -a(A, B) :- a(A, B) , not __updated__v(A, B, _). *) + (Deltadelete ("a", [NamedVar "A"; NamedVar "B"]), [ + Rel (Pred ("a", [NamedVar "A"; NamedVar "B"])); + Not (Pred ("__updated__v", [NamedVar "A"; NamedVar "B"; AnonVar])) + ]); + (* -b(B, C) :- +v(_, B, _) , b(B, C) , not __updated__v(_, B, C). *) + (Deltadelete ("b", [NamedVar "B"; NamedVar "C"]), [ + Rel (Deltainsert ("v", [AnonVar; NamedVar "B"; AnonVar])); + Rel (Pred ("b", [NamedVar "B"; NamedVar "C"])); + Not (Pred ("__updated__v", [AnonVar; NamedVar "B"; NamedVar "C"])) + ]); + (* -b(B, C) :- a(GENV2, B) , b(B, C) , b(B, GENV3) , not -v(GENV2, B, GENV3) , not __updated__v(_, B, C). *) + (Deltadelete ("b", [NamedVar "B"; NamedVar "C"]), [ + Rel (Pred ("a", [NamedVar "GENV2"; NamedVar "B"])); + Rel (Pred ("b", [NamedVar "B"; NamedVar "C"])); + Rel (Pred ("b", [NamedVar "B"; NamedVar "GENV3"])); + Not (Deltadelete ("v", [NamedVar "GENV2"; NamedVar "B"; NamedVar "GENV3"])); + Not (Pred ("__updated__v", [AnonVar; NamedVar "B"; NamedVar "C"])) + ]); + (* __updated__v(A, B, C) :- +v(A, B, C). *) + (Pred ("__updated__v", [NamedVar "A"; NamedVar "B"; NamedVar "C"]), [ + Rel (Deltainsert ("v", [NamedVar "A"; NamedVar "B"; NamedVar "C"])) + ]); + (* __updated__v(A, B, C) :- a(A, B) , b(B, C) , not -v(A, B, C). *) + (Pred ("__updated__v", [NamedVar "A"; NamedVar "B"; NamedVar "C"]), [ + Rel (Pred ("a", [NamedVar "A"; NamedVar "B"])); + Rel (Pred ("b", [NamedVar "B"; NamedVar "C"])); + Not (Deltadelete ("v", [NamedVar "A"; NamedVar "B"; NamedVar "C"])) + ]); + (* +b(B, C) :- +v(_, B, C) , not b(B, C). *) + (Deltainsert ("b", [NamedVar "B"; NamedVar "C"]), [ + Rel (Deltainsert ("v", [AnonVar; NamedVar "B"; NamedVar "C"])); + Not (Pred ("b", [NamedVar "B"; NamedVar "C"])) + ]); + (* +a(A, B) :- +v(A, B, _) , not a(A, B). *) + (Deltainsert ("a", [NamedVar "A"; NamedVar "B"]), [ + Rel (Deltainsert ("v", [NamedVar "A"; NamedVar "B"; AnonVar])); + Not (Pred ("a", [NamedVar "A"; NamedVar "B"])) + ]); + ] + }; + { + title = "--prepare option: projection"; + input = [ + (* + 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). + *) + (* -projs(A, B) :- projs(A, B) , -projv(A). *) + (Deltadelete ("projs", [NamedVar "A"; NamedVar "B"]), [ + Rel (Pred ("projs", [NamedVar "A"; NamedVar "B"])); + Rel (Deltadelete ("projv", [NamedVar "A"])) + ]); + (* +projs(A, B) :- projs(A, GENV7) , not -projv(A) , not projs(A, GENV1) , not -projs(GENV2, GENV3) , B = 'a'. *) + (Deltainsert ("projs", [NamedVar "A"; NamedVar "B"]), [ + Rel (Pred ("projs", [NamedVar "A"; NamedVar "GENV7"])); + Not (Deltadelete ("projv", [NamedVar "A"])); + Not (Pred ("projs", [NamedVar "A"; NamedVar "GENV1"])); + Not (Deltadelete ("projs", [NamedVar "GENV2"; NamedVar "GENV3"])); + Equat (Equation ("=", Var (NamedVar "B"), Const (String "a"))) + ]); + (* +projs(A, B) :- projs(A, GENV8) , not -projv(A) , not projs(A, GENV4) , projs(GENV5, B) , -projv(GENV5). *) + (Deltainsert ("projs", [NamedVar "A"; NamedVar "B"]), [ + Rel (Pred ("projs", [NamedVar "A"; NamedVar "GENV8"])); + Not (Deltadelete ("projv", [NamedVar "A"])); + Not (Pred ("projs", [NamedVar "A"; NamedVar "GENV4"])); + Rel (Pred ("projs", [NamedVar "GENV5"; NamedVar "B"])); + Rel (Deltadelete ("projv", [NamedVar "GENV5"])) + ]); + (* +projs(A, B) :- +projv(A) , not projs(A, GENV1) , not -projs(GENV2, GENV3) , B = 'a'. *) + (Deltainsert ("projs", [NamedVar "A"; NamedVar "B"]), [ + Rel (Deltainsert ("projv", [NamedVar "A"])); + Not (Pred ("projs", [NamedVar "A"; NamedVar "GENV1"])); + Not (Deltadelete ("projs", [NamedVar "GENV2"; NamedVar "GENV3"])); + Equat (Equation ("=", Var (NamedVar "B"), Const (String "a"))) + ]); + (* +projs(A, B) :- +projv(A) , not projs(A, GENV4) , projs(GENV5, B) , -projv(GENV5). *) + (Deltainsert ("projs", [NamedVar "A"; NamedVar "B"]), [ + Rel (Deltainsert ("projv", [NamedVar "A"])); + Not (Pred ("projs", [NamedVar "A"; NamedVar "GENV4"])); + Rel (Pred ("projs", [NamedVar "GENV5"; NamedVar "B"])); + Rel (Deltadelete ("projv", [NamedVar "GENV5"])) + ]); + (* __updated__projv(A) :- projs(A, GENV6) , not -projv(A). *) + (Pred ("__updated__projv", [NamedVar "A"]), [ + Rel (Pred ("projs", [NamedVar "A"; NamedVar "GENV6"])); + Not (Deltadelete ("projv", [NamedVar "A"])) + ]); + (* __updated__projv(A) :- +projv(A). *) + (Pred ("__updated__projv", [NamedVar "A"]), [ + Rel (Deltainsert ("projv", [NamedVar "A"])) + ]); + (* projv(A) :- projs(A, B). *) + (Pred ("projv", [NamedVar "A"]), [ + Rel (Pred ("projs", [NamedVar "A"; NamedVar "B"])) + ]); + ], + Some ("projv", []), + ["projs", []]; + expected = [ + (* + source projs('A':int, 'B':string). + view projv('A':int). + +projs(A, B) :- -projv(GENV5) , +projv(A) , projs(GENV5, B) , not projs(A, _). + +projs(A, B) :- +projv(A) , not -projs(_, _) , not projs(A, _) , B = 'a'. + -projs(A, B) :- -projv(A) , projs(A, B). + *) + (* +projs(A, B) :- -projv(GENV5) , +projv(A) , projs(GENV5, B) , not projs(A, _). *) + (Deltainsert ("projs", [NamedVar "A"; NamedVar "B"]), [ + Rel (Deltadelete ("projv", [NamedVar "GENV5"])); + Rel (Deltainsert ("projv", [NamedVar "A"])); + Rel (Pred ("projs", [NamedVar "GENV5"; NamedVar "B"])); + Not (Pred ("projs", [NamedVar "A"; AnonVar])) + ]); + (* +projs(A, B) :- +projv(A) , not -projs(_, _) , not projs(A, _) , B = 'a'. *) + (Deltainsert ("projs", [NamedVar "A"; NamedVar "B"]), [ + Rel (Deltainsert ("projv", [NamedVar "A"])); + Not (Deltadelete ("projs", [AnonVar; AnonVar])); + Not (Pred ("projs", [NamedVar "A"; AnonVar])); + Equat (Equation ("=", Var (NamedVar "B"), Const (String "a"))) + ]); + (* -projs(A, B) :- -projv(A) , projs(A, B). *) + (Deltadelete ("projs", [NamedVar "A"; NamedVar "B"]), [ + Rel (Deltadelete ("projv", [NamedVar "A"])); + Rel (Pred ("projs", [NamedVar "A"; NamedVar "B"])) + ]); + ] + }; + { + title = "--prepare option: union"; + input = [ + (* + 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). + *) + (* -uniona(N) :- uniona(N) , -unionview(N, T) , T = 'A'. *) + (Deltadelete ("uniona", [NamedVar "N"]), [ + Rel (Pred ("uniona", [NamedVar "N"])); + Rel (Deltadelete ("unionview", [NamedVar "N"; NamedVar "T"])); + Equat (Equation ("=", Var (NamedVar "T"), Const (String "A"))) + ]); + (* -unionb(N) :- unionb(N) , -unionview(N, T) , T = 'B'. *) + (Deltadelete ("unionb", [NamedVar "N"]), [ + Rel (Pred ("unionb", [NamedVar "N"])); + Rel (Deltadelete ("unionview", [NamedVar "N"; NamedVar "T"])); + Equat (Equation ("=", Var (NamedVar "T"), Const (String "B"))) + ]); + (* -uniono(N, T) :- uniono(N, T) , -unionview(N, T). *) + (Deltadelete ("uniono", [NamedVar "N"; NamedVar "T"]), [ + Rel (Pred ("uniono", [NamedVar "N"; NamedVar "T"])); + Rel (Deltadelete ("unionview", [NamedVar "N"; NamedVar "T"])) + ]); + (* +uniona(N) :- +unionview(N, T) , not uniona(N) , T = 'A' , not uniono(N, T). *) + (Deltainsert ("uniona", [NamedVar "N"]), [ + Rel (Deltainsert ("unionview", [NamedVar "N"; NamedVar "T"])); + Not (Pred ("uniona", [NamedVar "N"])); + Equat (Equation ("=", Var (NamedVar "T"), Const (String "A"))); + Not (Pred ("uniono", [NamedVar "N"; NamedVar "T"])) + ]); + (* +unionb(N) :- +unionview(N, T) , not unionb(N) , T = 'B' , not uniono(N, T). *) + (Deltainsert ("unionb", [NamedVar "N"]), [ + Rel (Deltainsert ("unionview", [NamedVar "N"; NamedVar "T"])); + Not (Pred ("unionb", [NamedVar "N"])); + Equat (Equation ("=", Var (NamedVar "T"), Const (String "B"))); + Not (Pred ("uniono", [NamedVar "N"; NamedVar "T"])) + ]); + (* +uniono(N, T) :- +unionview(N, T) , not uniono(N, T) , not T = 'A' , not T = 'B'. *) + (Deltainsert ("uniono", [NamedVar "N"; NamedVar "T"]), [ + Rel (Deltainsert ("unionview", [NamedVar "N"; NamedVar "T"])); + Not (Pred ("uniono", [NamedVar "N"; NamedVar "T"])); + Noneq (Equation ("=", Var (NamedVar "T"), Const (String "A"))); + Noneq (Equation ("=", Var (NamedVar "T"), Const (String "B"))) + ]); + (* unionview(N, T) :- uniona(N) , T = 'A'. *) + (Pred ("unionview", [NamedVar "N"; NamedVar "T"]), [ + Rel (Pred ("uniona", [NamedVar "N"])); + Equat (Equation ("=", Var (NamedVar "T"), Const (String "A"))) + ]); + (* unionview(N, T) :- unionb(N) , T = 'B'. *) + (Pred ("unionview", [NamedVar "N"; NamedVar "T"]), [ + Rel (Pred ("unionb", [NamedVar "N"])); + Equat (Equation ("=", Var (NamedVar "T"), Const (String "B"))) + ]); + (* unionview(N, T) :- uniono(N, T). *) + (Pred ("unionview", [NamedVar "N"; NamedVar "T"]), [ + Rel (Pred ("uniono", [NamedVar "N"; NamedVar "T"])) + ]); + ], + Some ("unionview", []), + ["uniona", []; "unionb", []; "uniono", []]; + expected = [ + (* + source uniono('NAME':string, 'TP':string). + source unionb('NAME':string). + source uniona('NAME':string). + view unionview('NAME':string, 'TP':string). + +uniono(N, T) :- +unionview(N, T) , not uniono(N, T) , not T = 'A' , not T = 'B'. + +unionb(N) :- +unionview(N, T) , not unionb(N) , not uniono(N, T) , T = 'B'. + +uniona(N) :- +unionview(N, T) , not uniona(N) , not uniono(N, T) , T = 'A'. + -uniono(N, T) :- -unionview(N, T) , uniono(N, T). + -unionb(N) :- -unionview(N, T) , unionb(N) , T = 'B'. + -uniona(N) :- -unionview(N, T) , uniona(N) , T = 'A'. + *) + (* +uniono(N, T) :- +unionview(N, T) , not uniono(N, T) , not T = 'A' , not T = 'B'. *) + (Deltainsert ("uniono", [NamedVar "N"; NamedVar "T"]), [ + Rel (Deltainsert ("unionview", [NamedVar "N"; NamedVar "T"])); + Not (Pred ("uniono", [NamedVar "N"; NamedVar "T"])); + Noneq (Equation ("=", Var (NamedVar "T"), Const (String "A"))); + Noneq (Equation ("=", Var (NamedVar "T"), Const (String "B"))) + ]); + (* +unionb(N) :- +unionview(N, T) , not unionb(N) , not uniono(N, T) , T = 'B'. *) + (Deltainsert ("unionb", [NamedVar "N"]), [ + Rel (Deltainsert ("unionview", [NamedVar "N"; NamedVar "T"])); + Not (Pred ("unionb", [NamedVar "N"])); + Not (Pred ("uniono", [NamedVar "N"; NamedVar "T"])); + Equat (Equation ("=", Var (NamedVar "T"), Const (String "B"))) + ]); + (* +uniona(N) :- +unionview(N, T) , not uniona(N) , not uniono(N, T) , T = 'A'. *) + (Deltainsert ("uniona", [NamedVar "N"]), [ + Rel (Deltainsert ("unionview", [NamedVar "N"; NamedVar "T"])); + Not (Pred ("uniona", [NamedVar "N"])); + Not (Pred ("uniono", [NamedVar "N"; NamedVar "T"])); + Equat (Equation ("=", Var (NamedVar "T"), Const (String "A"))) + ]); + (* -uniono(N, T) :- -unionview(N, T) , uniono(N, T). *) + (Deltadelete ("uniono", [NamedVar "N"; NamedVar "T"]), [ + Rel (Deltadelete ("unionview", [NamedVar "N"; NamedVar "T"])); + Rel (Pred ("uniono", [NamedVar "N"; NamedVar "T"])) + ]); + (* -unionb(N) :- -unionview(N, T) , unionb(N) , T = 'B'. *) + (Deltadelete ("unionb", [NamedVar "N"]), [ + Rel (Deltadelete ("unionview", [NamedVar "N"; NamedVar "T"])); + Rel (Pred ("unionb", [NamedVar "N"])); + Equat (Equation ("=", Var (NamedVar "T"), Const (String "B"))) + ]); + (* -uniona(N) :- -unionview(N, T) , uniona(N) , T = 'A'. *) + (Deltadelete ("uniona", [NamedVar "N"]), [ + Rel (Deltadelete ("unionview", [NamedVar "N"; NamedVar "T"])); + Rel (Pred ("uniona", [NamedVar "N"])); + Equat (Equation ("=", Var (NamedVar "T"), Const (String "A"))) + ]); + ] } ]