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

   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, []).

 generate_nmr_check(+Module) is det

Get the rules in the program containing odd loops and compute the NMR check. After this step, headless rules are useless, so remove them and add a fact for the negation of the dummy head (_false_0). Call generate_nmr_check/0 instead of this.

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

 nmr_check(+OLONrules:list, -NmrCheck:list) is det

Build the nmr_check.

Arguments:

OLONrules	- List of rules to create NMR sub-checks for.
NmrCheck	- List of NMR sub-check goals.

   97nmr_check([], []) :-
   98    !.
   99nmr_check(Rc, Nmrchk) :-
  100    debug(scasp(compile), 'Creating sub-checks...', []),
  101    olon_chks(Rc, Nmrchk, 1).

 olon_rules(+Rules:list, +Module, -OLONrules:list) is det

Determine which of the original rules are part of odd loops, and return them in a list.

Arguments:

RuleIn	- Input list of rules.
OLONrules	- Rules for which NMR sub-checks will need to be created.

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

 dfs(+Nodes:list, -OLONs:list, -OrdinaryPaths:list, -PositiveLoops:list) is det

Use depth first search to detect: cycles with no negation, cycles with even (>2) negation, paths with no cycle and cycles with odd negation. A list of paths will be returned for each type. Wrapper for dfs2/8.

Arguments:

Nodes	- Nodes in the call graph.
OLONs	- Paths containing odd loops. A list of lists of arcs, with each sublist representing a path containing an odd loop.
OrdinaryPaths	- Paths containing no odd loops and no even loops without an intervening negation. A list of lists of arcs, with each sublist representing a path containing only ordinary rules.
PositiveLoops	- Path with cycles that have no negation. A list of lists of arcs, with each sublist representing a path containing a positive loop.

  158dfs(N, Pc, Po, Pr) :-
  159    debug(scasp(compile), 'Detecting cycles in call graph...', []),
  160    dfs2(N, [], [], Pc, [], Po, [], Pr).

 dfs2(+Nodes:list, +Tested:list, +OlonIn:list, -OlonOut:list, +OrdIn:list, -OrdOut:list, +PosIn:list, -PosOut:list) is det

Test each node in case the graph isn't connected. For a visited node, dfs3/11 will return quickly as no paths will be expanded.

Arguments:

Nodes	- Nodes in the call graph.
Tested	- List of visited nodes with negation, so that we only visit each node at most once for each negation option: no negation, odd negation and even negation. Elements are of the form v(X, N), where X is the node and N is 0 = no negations, 1 = odd negs or 2 = even > 0 negs.
OlonIn	- Input list of paths containing OLONs.
OlonOut	- Output list of paths containing OLONs.
OrdIn	- Input list of ordinary paths.
OrdOut	- Output list of ordinary paths.
PosIn	- Input list of paths with cycles and no negations.
PosOut	- Output list of paths with cycles and no negations.

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

 dfs3(+Arcs:list, +VisitedIn:list, -VisitedOut:list, +Path:list, +Negations:int, +OlonIn:list, -OlonOut:list, +OrdIn:list, -OrdOut:list, +PosIn:list, -PosOut:list) is det

The main traversal. Traverse each arc for a node, but don't recursively search previously visited nodes.

Arguments:

Arcs	- The list of arcs in the call graph that originate at the last node in the current path.
VisitedIn	- Input list of visited nodes with negation, so that we only visit each node at most once for each negation option: no negation, odd negation and even negation. Elements are of the form v(X, N), where X is the node and N is 0 = no negations, 1 = odd negs or 2 = even > 0 negs.
VisitedOut	- Output list of visited nodes.
Path	- List of arcs forming the path currently being examined.
Negations	- 0 = no negations, 1 = odd negs or 2 = even > 0 negs
OlonIn	- Input list of paths containing OLONs.
OlonOut	- Output list of paths containing OLONs.
OrdIn	- Input list of ordinary paths.
OrdOut	- Output list of ordinary paths.
PosIn	- Input list of paths with cycles and no negations.
PosOut	- Output list of paths with cycles and no negations.

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

 check_cycle(+Node:list, +Path:list, +OlonIn:list, -OlonOut:list, +OrdIn:list, -OrdOut:list, +PosIn:list, -PosOut:list) is det

Get the cycle and classify by number of negations.

Arguments:

Node	- A node in the call graph.
Path	- List of arcs forming the path currently being examined.
OlonIn	- Input list of paths containing OLONs.
OlonOut	- Output list of paths containing OLONs.
OrdIn	- Input list of ordinary paths.
OrdOut	- Output list of ordinary paths.
PosIn	- Input list of paths with cycles and no negations.
PosOut	- Output list of paths with cycles and no negations.

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

 get_cycle(+Node:list, +Path:list, -Cycle:list, -Negations:int) is det

Get the portion of the path forming the cycle on node X. Count the negations as we go. Will fail if path doesn't have a cycle over X. Wrapper for get_cycle2/5.

Arguments:

Node	- A node in Path.
Path	- List of arcs forming the path currently being examined.
Cycle	- List of arcs forming a cycle on Node.
Negations	- The number of negations in Cycle.

  273:- det(get_cycle/4).  274
  275get_cycle(X, P, C, N) :-
  276    get_cycle2(X, P, C, 0, N).

 get_cycle2(+Node:list, +Path:list, -Cycle:list, +NegsIn:int, -NegsOut:int) is det

See get_cycle/4. Call that instead.

Arguments:

Node	- A node in Path.
Path	- List of arcs forming the path currently being examined.
Cycle	- List of arcs forming a cycle on the original node.
NegsIn	- Input number of negations in Cycle.
NegsOut	- Output number of negations in Cycle.

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

 classify_cycle(+Negs:int, +Cycle:list, +OlonIn:list, -OlonOut:list, +OrdIn:list, -OrdOut:list, +PosIn:list, -PosOut:list) is det

Put the cycle into the right group based on number of negations.

Arguments:

Negs	- Number of negations in Cycle.
Cycle	- List of arcs forming a cycle.
OlonIn	- Input list of paths containing OLONs.
OlonOut	- Output list of paths containing OLONs.
OrdIn	- Input list of ordinary paths.
OrdOut	- Output list of ordinary paths.
PosIn	- Input list of paths with cycles and no negations.
PosOut	- Output list of paths with cycles and no negations.

  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.

 update_negation(+NegsIn1:int, +NegsIn2:int, -NegsOut:int) is det

Update negation value. 0 = no negations, 1 = odd negs, 2 = even > 0 negs.

Arguments:

NegsIn	- Input negation value 1.
NegsIn2	- Input negation value 2.
NegsOut	- Output negation value.

  331update_negation(2, 1, 1) :-
  332    !.
  333update_negation(X, Y, Z) :-
  334    Z is X + Y.

 set_append(+Element:callable, +Set:list, +SetOut:list) is det

Append Elements only if not already present in Set.

Arguments:

Element	- The element to append.
Set	- Input set.
SetOut	- Output set.

  344set_append(X, Y, Y) :-
  345    memberchk(X, Y),
  346    !.
  347set_append(X, Y, [X|Y]).

 extract_ids(+Cycles:list, -IDs:list) is det

Given a list of cycles, get the unique rules IDs.

Arguments:

Cycles	- List of cycles in the call graph. Each cycle is a list of arcs.
IDs	- List of rule IDs from Cycles.

  356extract_ids(C, I) :-
  357    extract_ids2(C, [], I2),
  358    sort(I2, I). % remove duplicates

 extract_ids2(+Cycles:list, +IdsIn:list, -IdsOut:list) is det

Get the lists of ids from each path and merge them.

Arguments:

Cycles	- List of cycles in the call graph. Each cycle is a list of arcs.
IdsIn	- Input list of rules IDs from Cycles.
IdsOut	- Output list of rules IDs from Cycles.

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

 extract_ids3(+Cycle:list, +IdsIn:list, -IdsOut:list) is det

Get a list of IDs from a single path, extracting the rule ID for each arc.

Arguments:

Cycle	- A list of arcs representing a cycle in the call graph.
IdsIn	- Input list of rules IDs from Cycles.
IdsOut	- Output list of rules IDs from Cycles.

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

 divide_rules(+RulesIn:list, +IDs:list, -Members:list, -Nonmembers:list) is det

Split rules based on ID list membership.

Arguments:

RulesIn	- Input list of rules.
IDs	- A list of rule IDs.
Members	- Rules whose ID is a member of IDs.
Nonmembers	- Rules whose ID is not in IDs.

  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([], _, [], []).

 get_headless_rules(+RulesIn:list, +HeadlessIn:list, -HeadlessOut:list) is det

Get rules with the head '_false', indicating the rule was headless in the original program, and thus an OLON rule.

Arguments:

RulesIn	- Input rule list.
HeadlessIn	- Input list of headless rules (head = 1).
HeadlessOut	- Output list of headless rules (head = 1).

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

 olon_chks(+RulesIn:list, -NMRCheck:list, +Counter:int) is det

For each OLON rule, create a check that contains the negation of the rule's head by copying the rule and adding the negation if not present. Create the duals here since we can discard the unused non-dual. Add the new (dual) rule's head to the list of nmr checks. Use the original rule's ID for the goal ID in the NMR check. When adding the negation of the head to a rule, set the ID to ensure that it will be the last goal in the rule.

Arguments:

RulesIn	- List of rules to create NMR sub-checks for.
NMRCheck	- List of NMR sub-check goals.
Counter	- Counter used to ensure sub-check heads are unique.

  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([], [], _).

 assign_unique_ids(+ListIn:list, -ListOut:list) is det

Give each rule or goal a unique ID to allow individual members to be identified later. Wrapper for assign_unique_ids2/3. Note that list order is not changed. The IDs are sequential, and allow the original order to be restored by sorting later.

Arguments:

ListIn	- A list of rules or goals without attached IDs.
ListOut	- A list of rules or goals with unique IDs attached.

  481assign_unique_ids(Ri, Ro) :-
  482    assign_unique_ids2(Ri, Ro, 1).

 assign_unique_ids2(+ListIn:list, -ListOut:list, +Counter:int) is det

Assign each rule or goal (int) a unique ID, the current value of Counter. Call assign_unique_ids/2 instead of this predicate.

Arguments:

ListIn	- A list of rules or goals without attached IDs.
ListOut	- A list of rules or goals with unique IDs attached.
Counter	- The next ID to assign.

  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		 *******************************/

 create_dcc_rules(+Rc, +Module) is det

Create dcc rules to check consistency on-the-fly

  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,_,_)