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 ]). 34 35/** <module> Build the call graph used for NMR check construction and indexing. 36 37Given the input program, build a call graph and assert the components. 38 39@author Kyle Marple 40@version 20170127 41@license BSD-3 42*/ 43 44:- use_module(common). 45 46%! a(?Head:int, ?Goal:int, ?Negation:int, ?ID:int) is det 47% 48% Arc in the call graph from Head to Goal. Both head and goal will 49% always be positive with Negation indicating whether or not Goal was 50% originally negated. ID is the arc ID used to get associated rule IDs 51% from ar/2. 52% 53% @arg Head Rule head. 54% @arg Goal Absolute value of rule goal. 55% @arg Negation 1 or 0 indicating if Goal was originally negated. 56% @arg ID Arc ID. See ar/2. 57 58%! ar(?ArcID:int, ?RuleIDs:list) is det 59% 60% Associate an arc ID with a list of rule IDs. Each rule contains the 61% associated arc in the call graph; this avoids duplicate arcs. 62% 63% @arg ArcID An integer ID indicating an arc. See a/4. 64% @arg RuleIDs A list of rule IDs with matching arcs in the call graph. 65 66%! e(Literal:int) is det 67% 68% A literal to skip when building the call graph. 69% 70% @arg Literal The literal to skip. 71 72:- thread_local 73 a/4, % a(head, goal, negation, id) 74 ar/2. % ar(arc_id, rule_ids) 75 76%! build_call_graph(+Rules:list, -Nodes:list) 77% 78% Build and assert the call graph. Return a list of nodes. Don't 79% includes rules with heads present in the list of exclude. 80% 81% @arg Rules Rules to use in building call graph. 82% @arg Nodes Nodes in call graph. 83 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). 93 94%! get_nodes(+Arcs:list, -Nodes:list) 95% 96% Get a list of nodes in the graph. These are the positive literals 97% that occur as rule heads. 98% 99% @arg Arcs List of arcs in call graph, of the form a(Head, Goal, Neg, ID). 100% @arg Nodes Nodes in call graph. 101 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 ). 115 116%! get_arcs(+Rules:list, +ArcsIn:list, -ArcsOut:list) 117% 118% Get call graph edges w/ negation parity from rules. If rule/4 fails 119% (rules have no ID), use rule/3 and an ID of -1. 120% 121% @arg Rules The list of rules in the program. 122% @arg ArcsIn List of arcs of the form a(Head, Goal, Neg, ID). 123% @arg ArcsOut List of arcs of the form a(Head, Goal, Neg, ID). 124 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). 144 145 146%! get_arcs2(+Head:ground, +ID:int, +Goals:list, +ArcsIn:list, -ArcsOut:list) 147% 148% Get call graph arcs for a single rule. Format is: a(head, goal, 149% negation, id). 150% 151% @arg Head Head of a rule. 152% @arg ID Rule ID. 153% @arg Goals Body of rule. 154% @arg ArcsIn List of arcs of the form a(Head, Goal, Neg, ID). 155% @arg ArcsOut List of arcs of the form a(Head, Goal, Neg, ID). 156 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). 174 175%! merge_arcs(+ArcsIn:list, -ArcsOut:list, -IDgroups:list) is det. 176% 177% Ensure that at most one arc for each negation exists between two 178% nodes. Create a list of IDs for an arc to later associate with 179% rules. Use the first rule ID as the ID for the list of rules. 180% 181% @arg ArcsIn List of arcs of the form a(Head, Goal, Neg, ID). 182% @arg ArcsOut List of arcs of the form a(Head, Goal, Neg, ID). 183% @arg IDgroups List of ID groups of the form ar(ID, IDlist). 184 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([], [], []). 193 194%! merge_arcs2(+Head:int, +Goal:int, +Neg:int, 195%! +ArcsIn:list, -ArcsOut:list, -IDs:list) is det. 196% 197% Get rules associate with a single arc in the final graph 198% 199% @arg Head Head of rule. 200% @arg Goal Rule goal. Always positive, with Neg indicating negation. 201% @arg Neg 1 or 0 indicating if goal is negated. 202% @arg ArcsIn List of arcs of the form a(Head, Goal, Neg, ID). 203% @arg ArcsOut List of arcs of the form a(Head, Goal, Neg, ID). 204% @arg IDs IDs associated with the current arc. 205 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], []). 213 214%! assert_all(+List:list) 215% 216% Assert each element in a list. 217% 218% @arg List List of facts to assert. 219 220assert_all([X|T]) :- 221 assertz(X), 222 assert_all(T). 223assert_all([]). 224 225%! destroy_call_graph 226% 227% Retract the assertions for the call graph. 228 229destroy_call_graph :- 230 retractall(a(_,_,_,_)), 231 retractall(ar(_,_))