1/* 2* Copyright (c) 2016, University of Texas at Dallas 3* All rights reserved. 4* 5* Redistribution and use in source and binary forms, with or without 6* modification, are permitted provided that the following conditions are met: 7* * Redistributions of source code must retain the above copyright 8* notice, this list of conditions and the following disclaimer. 9* * Redistributions in binary form must reproduce the above copyright 10* notice, this list of conditions and the following disclaimer in the 11* documentation and/or other materials provided with the distribution. 12* * Neither the name of the University of Texas at Dallas nor the 13* names of its contributors may be used to endorse or promote products 14* derived from this software without specific prior written permission. 15* 16* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" 17* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE 18* IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE 19* DISCLAIMED. IN NO EVENT SHALL THE UNIVERSITY OF TEXAS AT DALLAS BE LIABLE FOR 20* ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES 21* (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; 22* LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND 23* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT 24* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS 25* SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. 26*/ 27 28:- module(scasp_nmr_check, 29 [ generate_nmr_check/1 % +Module 30 ]). 31 32/** <module> Detect OLON rules and construct nmr_check 33 34Detect OLON rules and construct nmr_check. 35 36Terminology: 37 38 - OLON: a loop with an odd number of default. negations in its 39 circular call dependency path. 40 - CHS: _Coinductive Hypothesis Set_, i.e., an atom that is true 41 due to coinduction, i.e. because it unifies with an ancestor. 42 - NMR check: non-monotonic reasoning check (from _Computing Stable 43 Models of Normal Logic Programs Without Grounding_ by Kyle Marple 44 et al. 45 46@author Kyle Marple 47@version 20170127 48@license BSD-3 49 50@see An OLON is a loop with an odd number of default. negations in its 51circular call dependency path, from "Layered Models Top-Down Querying of 52Normal Logic Programs" by LM Pereira, PADL09. 53@see "Galliwasp: A Goal-Directed Answer Set Solver" by Kyle Marple and 54Gopal Gupta, LOPSTR 2012 for details on the _NMR check_ 55*/ 56 57:- use_module(library(lists)). 58:- use_module(call_graph). 59:- use_module(common). 60:- use_module(comp_duals). 61:- use_module(program). 62:- use_module(variables). 63:- use_module(library(apply)). 64:- use_module(library(debug)). 65 66:- create_prolog_flag(scasp_compile_olon, true, []). 67:- create_prolog_flag(scasp_compile_nmr, true, []). 68 69%! generate_nmr_check(+Module) is det 70% 71% Get the rules in the program containing odd loops and compute the 72% NMR check. After this step, headless rules are useless, so remove 73% them and add a fact for the negation of the dummy head (_false_0). 74% Call generate_nmr_check/0 instead of this. 75 76:- det(generate_nmr_check/1). 77 78generate_nmr_check(M) :- 79 debug(scasp(compile), 'Generating NMR check...', []), 80 findall(R, (defined_rule(_, H, B, _), c_rule(R, H, B)), Rs), % get all rules 81 olon_rules(Rs, M, Rc), 82 nmr_check(Rc, Nmrchk), 83 retractall(defined_rule('_false_0', _, _, _)), % remove headless rules 84 negate_functor('_false_0', Nf), 85 predicate(Np, Nf, []), 86 c_rule(Nr, Np, []), 87 assert_rule(nmr(Nr)), % assert fact for negation of dummy head. 88 assert_nmr_check(Nmrchk). 89 90%! nmr_check(+OLONrules:list, -NmrCheck:list) is det 91% 92% Build the nmr_check. 93% 94% @arg OLONrules List of rules to create NMR sub-checks for. 95% @arg NmrCheck List of NMR sub-check goals. 96 97nmr_check([], []) :- 98 !. 99nmr_check(Rc, Nmrchk) :- 100 debug(scasp(compile), 'Creating sub-checks...', []), 101 olon_chks(Rc, Nmrchk, 1). 102 103%! olon_rules(+Rules:list, +Module, -OLONrules:list) is det 104% 105% Determine which of the original rules are part of odd loops, and 106% return them in a list. 107% 108% @arg RuleIn Input list of rules. 109% @arg OLONrules Rules for which NMR sub-checks will need to be created. 110 111:- det(olon_rules/3). 112 113olon_rules(R, M, Rc) :- 114 debug(scasp(compile), 'Detecting rules that contain odd loops over negation...', []), 115 assign_unique_ids(R, R1), 116 sort(R1, R2), % ensure that all rules with the same head are together 117 debug(scasp(compile), 'Building call graph...', []), 118 setup_call_cleanup( 119 build_call_graph(R2, Ns), % build call graph, skipping duals. 120 olon_rules_(R2, M, Ns, Rc), 121 destroy_call_graph). 122 123olon_rules_(R2, M, Ns, Rc) :- 124 dfs(Ns, Pc, _, _), 125 ( current_prolog_flag(scasp_dcc, true) 126 -> get_headless_rules(R2,[],Denials), 127 create_dcc_rules(Denials, M) 128 ; true 129 ), 130 ( current_prolog_flag(scasp_compile_olon, false) 131 -> Rc1 = [] 132 ; extract_ids(Pc, Ic), 133 divide_rules(R2, Ic, Rc1, _) % get OLON rules 134 ), 135 ( current_prolog_flag(scasp_compile_nmr, false) 136 -> Rc = [] 137 ; get_headless_rules(R2, Rc1, Rc) 138 ). 139 140 141%! dfs(+Nodes:list, -OLONs:list, -OrdinaryPaths:list, -PositiveLoops:list) is det 142% 143% Use depth first search to detect: cycles with no negation, cycles 144% with even (>2) negation, paths with no cycle and cycles with odd 145% negation. A list of paths will be returned for each type. Wrapper 146% for dfs2/8. 147% 148% @arg Nodes Nodes in the call graph. 149% @arg OLONs Paths containing odd loops. A list of lists of arcs, with each 150% sublist representing a path containing an odd loop. 151% @arg OrdinaryPaths Paths containing no odd loops and no even loops without 152% an intervening negation. A list of lists of arcs, with each sublist 153% representing a path containing only ordinary rules. 154% @arg PositiveLoops Path with cycles that have no negation. A list of lists 155% of arcs, with each sublist representing a path containing a positive 156% loop. 157 158dfs(N, Pc, Po, Pr) :- 159 debug(scasp(compile), 'Detecting cycles in call graph...', []), 160 dfs2(N, [], [], Pc, [], Po, [], Pr). 161 162%! dfs2(+Nodes:list, +Tested:list, +OlonIn:list, 163%! -OlonOut:list, +OrdIn:list, -OrdOut:list, 164%! +PosIn:list, -PosOut:list) is det 165% 166% Test each node in case the graph isn't connected. For a visited 167% node, dfs3/11 will return quickly as no paths will be expanded. 168% 169% @arg Nodes Nodes in the call graph. 170% @arg Tested List of visited nodes with negation, so that we only visit each 171% node at most once for each negation option: no negation, odd negation 172% and even negation. Elements are of the form v(X, N), where X is the 173% node and N is 0 = no negations, 1 = odd negs or 2 = even > 0 negs. 174% @arg OlonIn Input list of paths containing OLONs. 175% @arg OlonOut Output list of paths containing OLONs. 176% @arg OrdIn Input list of ordinary paths. 177% @arg OrdOut Output list of ordinary paths. 178% @arg PosIn Input list of paths with cycles and no negations. 179% @arg PosOut Output list of paths with cycles and no negations. 180 181dfs2([], _, Pc, Pc, Po, Po, Pr, Pr). 182dfs2([X|T], V, Pci, Pco, Poi, Poo, Pri, Pro) :- 183 findall(a(X, Y, N, I), a(X, Y, N, I), As), % Get all arcs from X 184 dfs3(As, [v(X, 0)|V], Vo, [], 0, Pci, Pc1, Poi, Po1, Pri, Pr1), 185 dfs2(T, Vo, Pc1, Pco, Po1, Poo, Pr1, Pro). 186 187%! dfs3(+Arcs:list, +VisitedIn:list, -VisitedOut:list, +Path:list, 188%! +Negations:int, +OlonIn:list, -OlonOut:list, 189%! +OrdIn:list, -OrdOut:list, +PosIn:list, -PosOut:list) is det 190% 191% The main traversal. Traverse each arc for a node, but don't 192% recursively search previously visited nodes. 193% 194% @arg Arcs The list of arcs in the call graph that originate at the last node 195% in the current path. 196% @arg VisitedIn Input list of visited nodes with negation, so that we only 197% visit each node at most once for each negation option: no negation, odd 198% negation and even negation. Elements are of the form v(X, N), where X 199% is the node and N is 0 = no negations, 1 = odd negs or 2 = even > 0 200% negs. 201% @arg VisitedOut Output list of visited nodes. 202% @arg Path List of arcs forming the path currently being examined. 203% @arg Negations 0 = no negations, 1 = odd negs or 2 = even > 0 negs 204% @arg OlonIn Input list of paths containing OLONs. 205% @arg OlonOut Output list of paths containing OLONs. 206% @arg OrdIn Input list of ordinary paths. 207% @arg OrdOut Output list of ordinary paths. 208% @arg PosIn Input list of paths with cycles and no negations. 209% @arg PosOut Output list of paths with cycles and no negations. 210 211:- det(dfs3/11). 212 213dfs3([], V, V, _, _, Pc, Pc, Po, Po, Pr, Pr). 214dfs3([A|T], Vi, Vo, P, N, Pci, Pco, Poi, Poo, Pri, [[A]|Pro]) :- % rule calls itself directly with no negation 215 A = a(X, X, 0, _), 216 !, 217 dfs3(T, Vi, Vo, P, N, Pci, Pco, Poi, Poo, Pri, Pro). 218dfs3([A|T], Vi, Vo, P, N, Pci, [[A]|Pco], Poi, Poo, Pri, Pro) :- % rule calls itself directly with a negation 219 A = a(X, X, 1, _), 220 !, 221 dfs3(T, Vi, Vo, P, N, Pci, Pco, Poi, Poo, Pri, Pro). 222dfs3([A|T], Vi, Vo, P, N, Pci, Pco, Poi, Poo, Pri, Pro) :- 223 A = a(_, Y, _, _), 224 memberchk(a(Y, _, _, _), P), % cycle 225 !, 226 check_cycle(Y, [A|P], Pci, Pc1, Poi, Po1, Pri, Pr1), 227 dfs3(T, Vi, Vo, P, N, Pc1, Pco, Po1, Poo, Pr1, Pro). 228dfs3([A|T], Vi, Vo, P, N, Pci, Pco, Poi, Poo, Pri, Pro) :- 229 A = a(_, Y, N2, _), 230 update_negation(N, N2, N3), 231 memberchk(v(Y, N3), Vi), % previously visited node, but not a cycle 232 !, 233 dfs3(T, Vi, Vo, P, N, Pci, Pco, Poi, Poo, Pri, Pro). 234dfs3([A|T], Vi, Vo, P, N, Pci, Pco, Poi, Poo, Pri, Pro) :- 235 A = a(_, Y, N2, _), % not previously visited or a cycle; expand 236 !, 237 update_negation(N, N2, N3), 238 set_append(v(Y, N3), Vi, V1), 239 findall(a(Y, Y2, Y3, Y4), a(Y, Y2, Y3, Y4), As), % Get all arcs from Y 240 dfs3(As, V1, V2, [A|P], N3, Pci, Pc1, Poi, Po1, Pri, Pr1), 241 dfs3(T, V2, Vo, P, N, Pc1, Pco, Po1, Poo, Pr1, Pro). 242 243%! check_cycle(+Node:list, +Path:list, +OlonIn:list, -OlonOut:list, 244%! +OrdIn:list, -OrdOut:list, 245%! +PosIn:list, -PosOut:list) is det 246% 247% Get the cycle and classify by number of negations. 248% 249% @arg Node A node in the call graph. 250% @arg Path List of arcs forming the path currently being examined. 251% @arg OlonIn Input list of paths containing OLONs. 252% @arg OlonOut Output list of paths containing OLONs. 253% @arg OrdIn Input list of ordinary paths. 254% @arg OrdOut Output list of ordinary paths. 255% @arg PosIn Input list of paths with cycles and no negations. 256% @arg PosOut Output list of paths with cycles and no negations. 257 258check_cycle(X, P, Pci, Pco, Poi, Poo, Pri, Pro) :- 259 get_cycle(X, P, C, N), 260 classify_cycle(N, C, Pci, Pco, Poi, Poo, Pri, Pro). 261 262%! get_cycle(+Node:list, +Path:list, -Cycle:list, -Negations:int) is det 263% 264% Get the portion of the path forming the cycle on node X. Count the 265% negations as we go. Will fail if path doesn't have a cycle over X. 266% Wrapper for get_cycle2/5. 267% 268% @arg Node A node in Path. 269% @arg Path List of arcs forming the path currently being examined. 270% @arg Cycle List of arcs forming a cycle on Node. 271% @arg Negations The number of negations in Cycle. 272 273:- det(get_cycle/4). 274 275get_cycle(X, P, C, N) :- 276 get_cycle2(X, P, C, 0, N). 277 278%! get_cycle2(+Node:list, +Path:list, -Cycle:list, 279%! +NegsIn:int, -NegsOut:int) is det 280% 281% See get_cycle/4. Call that instead. 282% 283% @arg Node A node in Path. 284% @arg Path List of arcs forming the path currently being examined. 285% @arg Cycle List of arcs forming a cycle on the original node. 286% @arg NegsIn Input number of negations in Cycle. 287% @arg NegsOut Output number of negations in Cycle. 288 289get_cycle2(X, [A|_], [A], Ni, No) :- 290 A = a(X, _, N, _), 291 !, 292 No is Ni + N. 293get_cycle2(X, [A|P], [A|C], Ni, No) :- 294 A = a(_, _, N, _), 295 N2 is N + Ni, 296 get_cycle2(X, P, C, N2, No). 297 298%! classify_cycle(+Negs:int, +Cycle:list, +OlonIn:list, -OlonOut:list, 299%! +OrdIn:list, -OrdOut:list, 300%! +PosIn:list, -PosOut:list) is det 301% 302% Put the cycle into the right group based on number of negations. 303% 304% @arg Negs Number of negations in Cycle. 305% @arg Cycle List of arcs forming a cycle. 306% @arg OlonIn Input list of paths containing OLONs. 307% @arg OlonOut Output list of paths containing OLONs. 308% @arg OrdIn Input list of ordinary paths. 309% @arg OrdOut Output list of ordinary paths. 310% @arg PosIn Input list of paths with cycles and no negations. 311% @arg PosOut Output list of paths with cycles and no negations. 312 313classify_cycle(0, C, Pc, Pc, Po, Po, Pr, [C|Pr]) :- 314 !. 315classify_cycle(N, C, Pc, Pc, Po, [C|Po], Pr, Pr) :- 316 N > 0, 317 N mod 2 =:= 0, 318 !. 319classify_cycle(N, C, Pc, [C|Pc], Po, Po, Pr, Pr) :- 320 N mod 2 =:= 1. 321 322%! update_negation(+NegsIn1:int, +NegsIn2:int, -NegsOut:int) is det 323% 324% Update negation value. 0 = no negations, 1 = odd negs, 2 = even > 0 325% negs. 326% 327% @arg NegsIn Input negation value 1. 328% @arg NegsIn2 Input negation value 2. 329% @arg NegsOut Output negation value. 330 331update_negation(2, 1, 1) :- 332 !. 333update_negation(X, Y, Z) :- 334 Z is X + Y. 335 336%! set_append(+Element:callable, +Set:list, +SetOut:list) is det 337% 338% Append Elements only if not already present in Set. 339% 340% @arg Element The element to append. 341% @arg Set Input set. 342% @arg SetOut Output set. 343 344set_append(X, Y, Y) :- 345 memberchk(X, Y), 346 !. 347set_append(X, Y, [X|Y]). 348 349%! extract_ids(+Cycles:list, -IDs:list) is det 350% 351% Given a list of cycles, get the unique rules IDs. 352% 353% @arg Cycles List of cycles in the call graph. Each cycle is a list of arcs. 354% @arg IDs List of rule IDs from Cycles. 355 356extract_ids(C, I) :- 357 extract_ids2(C, [], I2), 358 sort(I2, I). % remove duplicates 359 360%! extract_ids2(+Cycles:list, +IdsIn:list, -IdsOut:list) is det 361% 362% Get the lists of ids from each path and merge them. 363% 364% @arg Cycles List of cycles in the call graph. Each cycle is a list of arcs. 365% @arg IdsIn Input list of rules IDs from Cycles. 366% @arg IdsOut Output list of rules IDs from Cycles. 367 368extract_ids2([X|T], Ii, Io) :- 369 extract_ids3(X, [], I), 370 append(I, Ii, I1), 371 extract_ids2(T, I1, Io). 372extract_ids2([], I, I). 373 374%! extract_ids3(+Cycle:list, +IdsIn:list, -IdsOut:list) is det 375% 376% Get a list of IDs from a single path, extracting the rule ID for 377% each arc. 378% 379% @arg Cycle A list of arcs representing a cycle in the call graph. 380% @arg IdsIn Input list of rules IDs from Cycles. 381% @arg IdsOut Output list of rules IDs from Cycles. 382 383extract_ids3([X|T], Ii, Io) :- 384 X = a(_, _, _, I), % I is the arc ID 385 once(ar(I, Ri)), % ar/2 associates an arc ID with a list of rule IDs 386 append(Ri, Ii, I1), 387 extract_ids3(T, I1, Io). 388extract_ids3([], I, I). 389 390%! divide_rules(+RulesIn:list, +IDs:list, -Members:list, -Nonmembers:list) is det 391% 392% Split rules based on ID list membership. 393% 394% @arg RulesIn Input list of rules. 395% @arg IDs A list of rule IDs. 396% @arg Members Rules whose ID is a member of IDs. 397% @arg Nonmembers Rules whose ID is not in IDs. 398 399divide_rules([X|T], Is, [X|To], To2) :- % rule in list 400 rule(X, _, I, _), 401 memberchk(I, Is), 402 !, 403 divide_rules(T, Is, To, To2). 404divide_rules([X|T], Is, To, [X|To2]) :- % rule not in list 405 !, 406 divide_rules(T, Is, To, To2). 407divide_rules([], _, [], []). 408 409%! get_headless_rules(+RulesIn:list, +HeadlessIn:list, -HeadlessOut:list) is det 410% 411% Get rules with the head '_false', indicating the rule was headless 412% in the original program, and thus an OLON rule. 413% 414% @arg RulesIn Input rule list. 415% @arg HeadlessIn Input list of headless rules (head = 1). 416% @arg HeadlessOut Output list of headless rules (head = 1). 417 418get_headless_rules([X|T], Rci, [X|Rco]) :- 419 rule(X, H, _, _), 420 predicate(H, '_false_0', _), % headless rule 421 !, 422 get_headless_rules(T, Rci, Rco). 423get_headless_rules([_|T], Rci, Rco) :- 424 get_headless_rules(T, Rci, Rco). 425get_headless_rules([], Rc, Rc). 426 427%! olon_chks(+RulesIn:list, -NMRCheck:list, +Counter:int) is det 428% 429% For each OLON rule, create a check that contains the negation of the 430% rule's head by copying the rule and adding the negation if not 431% present. Create the duals here since we can discard the unused 432% non-dual. Add the new (dual) rule's head to the list of nmr checks. 433% Use the original rule's ID for the goal ID in the NMR check. When 434% adding the negation of the head to a rule, set the ID to ensure that 435% it will be the last goal in the rule. 436% 437% @arg RulesIn List of rules to create NMR sub-checks for. 438% @arg NMRCheck List of NMR sub-check goals. 439% @arg Counter Counter used to ensure sub-check heads are unique. 440 441olon_chks([R|T], [not(G)|Nmr], C) :- 442 rule(R, X, _, Y), 443 predicate(X, '_false_0', _), % headless rule 444 !, 445 c_rule(R2, X, Y), % strip ID for comp_duals3/2 446 create_unique_functor('_chk_0', C, H), % Create functor for sub-check head 447 comp_duals3(H, [R2]), 448 predicate(G, H, []), % Create goal for NMR check 449 C1 is C + 1, 450 olon_chks(T, Nmr, C1). 451olon_chks([R|T], [Go|Nmr], C) :- 452 rule(R, X, _, Y), 453 !, 454 ( memberchk(not(X), Y) % negated head must match exactly, including args 455 -> c_rule(R2, X, Y) 456 ; append(Y, [not(X)], Y2), 457 c_rule(R2, X, Y2) % add negated head to body 458 ), 459 predicate(X, Hi, _), 460 split_functor(Hi, _, A), % get arity of head 461 atom_concat('_chk_', A, Hb), 462 create_unique_functor(Hb, C, H), % Create functor for sub-check head 463 comp_duals3(H, [R2]), 464 var_list(A, V), % Get place holder args for NMR check goal 465 predicate(G, H, V), 466 define_forall(not(G), Go, V), % forall for every variable in the head. 467 C1 is C + 1, 468 olon_chks(T, Nmr, C1). 469olon_chks([], [], _). 470 471%! assign_unique_ids(+ListIn:list, -ListOut:list) is det 472% 473% Give each rule or goal a unique ID to allow individual members to be 474% identified later. Wrapper for assign_unique_ids2/3. Note that list 475% order is not changed. The IDs are sequential, and allow the original 476% order to be restored by sorting later. 477% 478% @arg ListIn A list of rules or goals without attached IDs. 479% @arg ListOut A list of rules or goals with unique IDs attached. 480 481assign_unique_ids(Ri, Ro) :- 482 assign_unique_ids2(Ri, Ro, 1). 483 484%! assign_unique_ids2(+ListIn:list, -ListOut:list, +Counter:int) is det 485% 486% Assign each rule or goal (int) a unique ID, the current value of 487% Counter. Call assign_unique_ids/2 instead of this predicate. 488% 489% @arg ListIn A list of rules or goals without attached IDs. 490% @arg ListOut A list of rules or goals with unique IDs attached. 491% @arg Counter The next ID to assign. 492 493assign_unique_ids2([], [], _). 494assign_unique_ids2([X|T], [X2|T2], C) :- 495 c_rule(X, H, B), % rule 496 !, 497 rule(X2, H, C, B), 498 C1 is C + 1, 499 assign_unique_ids2(T, T2, C1). 500assign_unique_ids2([X|T], [X2|T2], C) :- 501 X2 = -(X, C), 502 C1 is C + 1, 503 assign_unique_ids2(T, T2, C1). 504 505 506 /******************************* 507 * DCC RULES * 508 *******************************/ 509 510%! create_dcc_rules(+Rc, +Module) is det 511% 512% Create dcc rules to check consistency on-the-fly 513 514create_dcc_rules([], _). 515create_dcc_rules([-(-(_,_),Rule)|Rc], M) :- 516 maplist(remove_arity, Rule, Dcc), 517 revar(Dcc, RDcc, _), 518 assert_dcc_rule([], RDcc, M), 519 create_dcc_rules(Rc, M). 520 521remove_arity(not(R), not(D)) :- !, 522 remove_arity(R, D). 523remove_arity(R, D) :- 524 R =.. [RName|Args], 525 split_functor(RName, DName, _), 526 !, 527 D =.. [DName|Args]. 528remove_arity(R, R). 529 530assert_dcc_rule(Prev, [A|Next], M) :- 531 !, 532 append(Prev, Next, Prev0), 533 ( skip_dcc(A) 534 -> true 535 ; assert(M:pr_dcc_predicate(dcc(A), Prev0)), 536 true 537 ), 538 append(Prev, [A], Prev1), 539 assert_dcc_rule(Prev1, Next, M). 540assert_dcc_rule(_, [], _). 541 542skip_dcc(forall(_,_)) => true. 543skip_dcc(A) => functor(A, Op, 2), operator(Op,_,_)