View source with raw comments or as raw
    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_call_graph,
   29          [ build_call_graph/2,
   30            destroy_call_graph/0,
   31            a/4,
   32            ar/2
   33          ]).

Build the call graph used for NMR check construction and indexing.

Given the input program, build a call graph and assert the components.

author
- Kyle Marple
version
- 20170127
license
- BSD-3 */
   44:- use_module(common).
 a(?Head:int, ?Goal:int, ?Negation:int, ?ID:int) is det
Arc in the call graph from Head to Goal. Both head and goal will always be positive with Negation indicating whether or not Goal was originally negated. ID is the arc ID used to get associated rule IDs from ar/2.
Arguments:
Head- Rule head.
Goal- Absolute value of rule goal.
Negation- 1 or 0 indicating if Goal was originally negated.
ID- Arc ID. See ar/2.
 ar(?ArcID:int, ?RuleIDs:list) is det
Associate an arc ID with a list of rule IDs. Each rule contains the associated arc in the call graph; this avoids duplicate arcs.
Arguments:
ArcID- An integer ID indicating an arc. See a/4.
RuleIDs- A list of rule IDs with matching arcs in the call graph.
 e(Literal:int) is det
A literal to skip when building the call graph.
Arguments:
Literal- The literal to skip.
   72:- thread_local
   73    a/4,		% a(head, goal, negation, id)
   74    ar/2.               % ar(arc_id, rule_ids)
 build_call_graph(+Rules:list, -Nodes:list)
Build and assert the call graph. Return a list of nodes. Don't includes rules with heads present in the list of exclude.
Arguments:
Rules- Rules to use in building call graph.
Nodes- Nodes in call graph.
   84build_call_graph([], []) :-
   85    !.
   86build_call_graph(R, Ns) :-
   87    get_arcs(R, [], As),
   88    sort(As, As2),
   89    merge_arcs(As2, As3, Rs),
   90    get_nodes(As3, Ns),
   91    assert_all(As3),
   92    assert_all(Rs).
 get_nodes(+Arcs:list, -Nodes:list)
Get a list of nodes in the graph. These are the positive literals that occur as rule heads.
Arguments:
Arcs- List of arcs in call graph, of the form a(Head, Goal, Neg, ID).
Nodes- Nodes in call graph.
  102get_nodes([X|T], [N|Ns]) :-
  103    X = a(N, _, _, _),
  104    get_nodes(T, N, Ns).
  105get_nodes([], []).
  106
  107get_nodes([], _, []).
  108get_nodes([X|T], N, Ns) :-
  109    X = a(Y, _, _, _),
  110    (   Y = N
  111    ->  get_nodes(T, N, Ns)
  112    ;   Ns = [Y|Ns2],
  113        get_nodes(T, Y, Ns2)
  114    ).
 get_arcs(+Rules:list, +ArcsIn:list, -ArcsOut:list)
Get call graph edges w/ negation parity from rules. If rule/4 fails (rules have no ID), use rule/3 and an ID of -1.
Arguments:
Rules- The list of rules in the program.
ArcsIn- List of arcs of the form a(Head, Goal, Neg, ID).
ArcsOut- List of arcs of the form a(Head, Goal, Neg, ID).
  125get_arcs([], G, G).
  126get_arcs([R|T], Gi, Go) :-
  127    (   rule(R, H, I, Y)
  128    ->  true
  129    ;   c_rule(R, H, Y)
  130    ->  I = -1
  131    ),
  132    rule(R, H, I, Y), % Rules have IDs.
  133    predicate(H, F, _), % get functor of head
  134    \+ ignore_edge(F),
  135    !,
  136    get_arcs2(F, I, Y, Gi, G1),
  137    get_arcs(T, G1, Go).
  138get_arcs([_|T], Gi, Go) :-
  139    get_arcs(T, Gi, Go).
  140
  141ignore_edge('_false_0'). % ignore headless rules
  142ignore_edge(F) :-        % and duals.
  143    is_dual(F).
 get_arcs2(+Head:ground, +ID:int, +Goals:list, +ArcsIn:list, -ArcsOut:list)
Get call graph arcs for a single rule. Format is: a(head, goal, negation, id).
Arguments:
Head- Head of a rule.
ID- Rule ID.
Goals- Body of rule.
ArcsIn- List of arcs of the form a(Head, Goal, Neg, ID).
ArcsOut- List of arcs of the form a(Head, Goal, Neg, ID).
  157get_arcs2(_, _, [], G, G) :-
  158    !.
  159get_arcs2(H, I, [Y|T], Gi, [G|Go]) :-
  160    predicate(Y, Gy, _), % if goal is a predicate, get the functor
  161    \+ is_dual(Gy),
  162    !,
  163    G = a(H, Gy, 0, I),
  164    get_arcs2(H, I, T, Gi, Go).
  165get_arcs2(H, I, [Y|T], Gi, [G|Go]) :-
  166    Y = not(Y2),
  167    !,
  168    predicate(Y2, Gn, _), % get the functor
  169    G = a(H, Gn, 1, I),
  170    get_arcs2(H, I, T, Gi, Go).
  171get_arcs2(H, I, [Y|T], Gi, Go) :-
  172    \+ predicate(Y, _, _), % goal isn't a predicate; skip it
  173    get_arcs2(H, I, T, Gi, Go).
 merge_arcs(+ArcsIn:list, -ArcsOut:list, -IDgroups:list) is det
Ensure that at most one arc for each negation exists between two nodes. Create a list of IDs for an arc to later associate with rules. Use the first rule ID as the ID for the list of rules.
Arguments:
ArcsIn- List of arcs of the form a(Head, Goal, Neg, ID).
ArcsOut- List of arcs of the form a(Head, Goal, Neg, ID).
IDgroups- List of ID groups of the form ar(ID, IDlist).
  185:- det(merge_arcs/3).  186
  187merge_arcs([X|T], [X|As], [Ar|Is]) :-
  188    X = a(H, G, N, I),
  189    merge_arcs2(H, G, N, T, To, Rs),
  190    Ar = ar(I, [I|Rs]),
  191    merge_arcs(To, As, Is).
  192merge_arcs([], [], []).
 merge_arcs2(+Head:int, +Goal:int, +Neg:int, +ArcsIn:list, -ArcsOut:list, -IDs:list) is det
Get rules associate with a single arc in the final graph
Arguments:
Head- Head of rule.
Goal- Rule goal. Always positive, with Neg indicating negation.
Neg- 1 or 0 indicating if goal is negated.
ArcsIn- List of arcs of the form a(Head, Goal, Neg, ID).
ArcsOut- List of arcs of the form a(Head, Goal, Neg, ID).
IDs- IDs associated with the current arc.
  206merge_arcs2(_, _, _, [], [], []) :-
  207    !.
  208merge_arcs2(H, G, N, [X|T], To, [I|Rs]) :-
  209    X = a(H, G, N, I),
  210    !,
  211    merge_arcs2(H, G, N, T, To, Rs).
  212merge_arcs2(_, _, _, [X|T], [X|T], []).
 assert_all(+List:list)
Assert each element in a list.
Arguments:
List- List of facts to assert.
  220assert_all([X|T]) :-
  221    assertz(X),
  222    assert_all(T).
  223assert_all([]).
 destroy_call_graph
Retract the assertions for the call graph.
  229destroy_call_graph :-
  230    retractall(a(_,_,_,_)),
  231    retractall(ar(_,_))