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_comp_duals, 29 [ comp_duals/0, 30 comp_duals3/2, 31 define_forall/3 32 ]). 33 34/** <module> Dual rule computation 35 36Computation of dual rules (rules for the negation of a literal). 37 38@author Kyle Marple 39@version 20170127 40@license BSD-3 41*/ 42 43:- use_module(library(lists)). 44:- use_module(common). 45:- use_module(program). 46:- use_module(variables). 47:- use_module(options). 48 49:- create_prolog_flag(scasp_plain_dual, false, []). 50 51%! comp_duals is det 52% 53% Compute rules for the negations of positive literals (dual rules), 54% even if there are no clauses for the positive literal (negation will 55% be a fact). Wrapper for comp_duals2/1. 56 57:- det(comp_duals/0). 58 59comp_duals :- 60 debug(scasp(compile), 'Computing dual rules...', []), 61 defined_predicates(Preds), 62 maplist(comp_dual, Preds). 63 64scasp_builtin('call_1'). 65scasp_builtin('findall_3'). 66 67%! comp_dual(+Predicate) is det 68% 69% get matching rules and call comp_duals3/2. 70 71comp_dual('_false_0') :- % Headless rules are handled by NMR check 72 !. 73comp_dual(X) :- 74 scasp_builtin(X), % skip dual of scasp builtins 75 !. 76comp_dual(X) :- 77 findall(R, (defined_rule(X, H, B, _), c_rule(R, H, B)), Rs), % get rules for a single predicate 78 comp_duals3(X, Rs). 79 80%! comp_duals3(+Predicate:atom, +Rules:list) is det 81% 82% Compute the dual for a single positive literal. Make sure that 83% Predicate is used for the dual head instead of taking the head from 84% one of the rules. This allows a new head to be passed during NMR 85% sub-check creation. 86% 87% @arg Predicate The head of each rule in Rules, of the form Head/arity. 88% @arg Rules The list of rules for a single predicate. 89 90:- det(comp_duals3/2). 91 92comp_duals3(P, []) :- 93 !, % Predicate is called but undefined. Dual will be a fact. 94 predicate(H, P, []), % create a dummy predicate for outer_dual_head/2. 95 outer_dual_head(H, Hd), 96 c_rule(Rd, Hd, []), 97 assert_rule(dual(Rd)). 98comp_duals3(P, R) :- % predicate is defined by one or more rules. 99 predicate(H, P, []), % create a dummy predicate for P. 100 outer_dual_head(H, Hd), 101 comp_dual(Hd, R, Db, 1), 102 c_rule(Rd, Hd, Db), 103 assert_rule(dual(Rd)). 104 105%! comp_dual(+DualHead:compound, +Rules:list, -DualBody:list, +Count:int) is det 106% 107% Compute the dual for a predicate with multiple rules. First, compute 108% the dual of each individual rule, replacing each head with a new, 109% unique one. Then create the overall dual using the heads of the 110% individual duals as goals. When finished, assert the overall dual. 111% 112% @arg DualHead The head of the dual rule. 113% @arg Rules The list of rules. 114% @arg DualBody The body of the outer dual rule. 115% @arg Count Counter used to ensure that new heads are unique. 116 117comp_dual(_, [], [], _) :- 118 !. 119comp_dual(Hn, [X|T], [Dg|Db], C) :- 120 c_rule(X, H, B), 121 % get unique head with Hn2 including original args and Hn3 using variable args 122 predicate(H, _, A1), 123 predicate(Hn, F, A2), 124 replace_prefix(F, n_, n__, F2), % add underscore to make it non-printing. 125 create_unique_functor(F2, C, F3), 126 abstract_structures(A1, A3, 0, G), 127 append(G, B, B2), 128 prep_args(A3, A2, [], A4, [], 0, G2), % get var list for inner dual clause heads and inner unifiability goals 129 append(G2, B2, B3), % combine all goals 130 predicate(Dh, F3, A4), % inner dual clause head 131 body_vars(Dh, B2, Bv), 132 predicate(Dg, F3, A2), % outer dual goal for inner dual 133 comp_dual2(Dh, B3, Bv), % create inner dual clauses 134 C2 is C + 1, 135 !, 136 comp_dual(Hn, T, Db, C2). 137 138%! comp_dual2(+DualHead:compound, +Body:list, +BodyVars:list) is det 139% 140% Compute the dual for a single clause. Since any body variables in 141% the original rule are existentially, they must be universally 142% quantified in the dual. This is accomplished by creating a new 143% predicate with both the original head variables and the body 144% variables in the head, which will contain the duals of the original 145% goals. The "inner dual" will then call this new predicate in a 146% forall over the body variables. 147% 148% @arg DualHead The head of the dual rule. 149% @arg Body The body of the original rule. 150% @arg BodyVars The list of variables in the body but not the head. 151 152comp_dual2(Hn, Bg, []) :- 153 !, % no body variables 154 comp_dual3(Hn, Bg, []). 155comp_dual2(Hn, Bg, Bv) :- 156 Hn =.. [F|A1], 157 append(A1, Bv, A2), 158 length(A2, Arity), 159 split_functor(F, Base0, _), % remove arity 160 atomic_list_concat([Base0, '_vh', Arity], Base), 161 join_functor(F2, Base, Arity), 162 Hn2 =.. [F2|A2], % add body variables to innermost head. 163 define_forall(Hn2, G, Bv), % get the call to the innermost dual 164 comp_dual3(Hn2, Bg, []), % create innermost duals 165 c_rule(Rd, Hn, [G]), % create dual 166 assert_rule(dual(Rd)). 167 168%! comp_dual3(+DualHead:compound, +Body:list, +UsedGoals:list) is det 169% 170% Compute the innermost dual for a single rule by negating each goal 171% in turn. Unlike grounded ASP, it is not enough to have a single-goal 172% clause for each original goal. Because side effects are possible, 173% the sub-dual for a given goal must include all previous goals and 174% retain program order. 175% 176% @arg DualHead The head of the dual rule. 177% @arg Body The body goals to negate. 178% @arg UsedGoals The goals that have already been processed, in original 179% order. 180 181comp_dual3(_, [], _) :- 182 !. 183comp_dual3(Hn, [X|T], U) :- 184 X = builtin_1(_), % handle built-ins specially 185 !, 186 ( current_prolog_flag(scasp_plain_dual, true) 187 -> U2 = [X] 188 ; append(U, [X], U2) 189 ), 190 comp_dual3(Hn, T, U2). 191comp_dual3(Hn, [X|T], U) :- 192 dual_goal(X, X2), 193 ( current_prolog_flag(scasp_plain_dual, true) 194 -> Db = [X2] 195 ; append(U, [X2], Db) % Keep all goals prior to the dual one. 196 ), 197 c_rule(Rd, Hn, Db), % Clause for negation of body goal 198 assert_rule(dual(Rd)), 199 append(U, [X], U2), 200 comp_dual3(Hn, T, U2). 201 202%! dual_goal(+GoalIn:compound, -GoalOut:compound) is det 203% 204% Given a goal, negated it. 205% 206% @arg GoalIn The original goal. 207% @arg GoalOut The negated goal. 208 209% constraint 210dual_goal(#=(A, B), #<>(A,B)). 211dual_goal(#<>(A, B), #=(A,B)). 212dual_goal(#>(A, B), #=<(A,B)). 213dual_goal(#<(A, B), #>=(A,B)). 214dual_goal(#>=(A, B), #<(A,B)). 215dual_goal(#=<(A, B), #>(A,B)). 216% clpq/r 217dual_goal(#=(A, B), #<>(A,B)). 218dual_goal(#<>(A, B), #=(A,B)). 219dual_goal(#>(A, B), #=<(A,B)). 220dual_goal(#<(A, B), #>=(A,B)). 221dual_goal(#>=(A, B), #<(A,B)). 222dual_goal(#=<(A, B), #>(A,B)). 223 224dual_goal(=\=(A, B), =:=(A,B)). 225dual_goal(=:=(A, B), =\=(A,B)). 226dual_goal(<(A, B), >=(A,B)). 227dual_goal(>(A, B), =<(A,B)). 228dual_goal(=<(A, B), >(A,B)). 229dual_goal(>=(A, B), <(A,B)). 230dual_goal(@<(A, B), @>=(A,B)). 231dual_goal(@>(A, B), @=<(A,B)). 232dual_goal(@=<(A, B), @>(A,B)). 233dual_goal(@>=(A, B), @<(A,B)). 234%dual_goal(=(A, B), '#<>'(A,B)). 235dual_goal(=(A, B), \=(A,B)). 236dual_goal(\=(A, B), =(A,B)). 237%dual_goal('#<>'(A, B), =(A,B)). 238dual_goal(is(A, B), not(is(A,B))). % special case for is 239dual_goal(not(X), X) :- 240 predicate(X, _, _), 241 !. 242dual_goal(X, not(X)) :- 243 predicate(X, _, _), 244 !. 245 246%! define_forall(+GoalIn:compound, -GoalOut:compound, +BodyVars:list) is det 247% 248% If BodyVars is empty, just return the original goal. Otherwise, 249% define a forall for the goal. For multiple body variables, the 250% forall will be nested, with each layer containing a single variable. 251% 252% @arg GoalIn Input goal. 253% @arg GoalOut Output goal. 254% @arg BodyVars Body variables present in GoalIn. 255 256define_forall(G, G, []) :- 257 !. 258define_forall(Gi, forall(X, G2), [X|T]) :- 259 define_forall(Gi, G2, T). 260 261%! outer_dual_head(+Head:atom, -DualHead:compound) is det 262% 263% Create the dual version of a rule head by negating the predicate 264% name and replacing the args with a variable list of the same arity. 265% 266% @arg Head The initial, positive head, a predicate name. 267% @arg DualHead The dual head, a predicate struct. 268 269outer_dual_head(H, D) :- 270 predicate(H, P, _Args), 271 negate_functor(P, Pd), 272 split_functor(Pd, _, A), % get the arity 273 var_list(A, Ad), % get the arg list 274 predicate(D, Pd, Ad). 275 276%! abstract_structures(+ArgsIn:list, -ArgsOut:list, +Counter:int, 277%! -Goals:list) is det 278% 279% Given a list of args, abstract any structures by replacing them with 280% variables and adding a goal unifying the variable with the 281% structure. 282% 283% @arg ArgsIn The original args from a clause head. 284% @arg ArgsOut Output new args. 285% @arg Counter Input counter. 286% @arg Goals Goals unifying non-variables with the variables replacing them. 287 288abstract_structures([], [], _, []). 289abstract_structures([X|T], [$Y|T2], C, [G|Gt]) :- 290 compound(X), 291 \+ is_var(X), 292 !, 293 atom_concat('_Z', C, Y), 294 C1 is C + 1, 295 G = ($Y = X), 296 abstract_structures(T, T2, C1, Gt). 297abstract_structures([X|T], [X|T2], C, G) :- 298 abstract_structures(T, T2, C, G). 299 300 301%! prep_args(+OrigArgs:list, +VarArgs:list, 302%! +NewArgsIn:list, -NewArgsOut:list, 303%! +VarsSeen:list, +Counter:int, -Goals:list) is det 304% 305% Given two sets of args, check if each of the original args is a 306% variable. If so, check if it's a member of NewArgsIn. If it's not, 307% add it to output args. If it isn't a variable, or the variable is 308% present in NewArgsIn, add the corresponding variable from VarArgs. 309% The result is a list of variables that keeps any variables in the 310% original head. When an element from VarArgs is used, add a 311% unification (=) goal to Goals. 312% 313% @arg OrigArgs The original args from a clause head. 314% @arg VarArgs A list of unique variable names of the same length as OrigArgs. 315% @arg NewArgsIn Input new args. 316% @arg NewArgsOut Output new args. 317% @arg VarsSeen List of variables encountered in original args. 318% @arg Counter Input counter. 319% @arg Goals Goals unifying non-variables with the variables replacing them. 320 321:- det(prep_args/7). 322 323prep_args([], _, Ai, Ao, _, _, []) :- 324 reverse(Ai, Ao). % Restore proper ordering 325prep_args([X|T], [Y|T2], Ai, Ao, Vs, C, [G|Gt]) :- 326 is_var(X), 327 memberchk(X, Vs), % X has already been seen 328 !, 329 G = (Y=X), % create unification goal 330 prep_args(T, T2, [Y|Ai], Ao, Vs, C, Gt). 331prep_args([X|T], [_|T2], Ai, Ao, Vs, C, G) :- 332 is_var(X), 333 !, 334 prep_args(T, T2, [X|Ai], Ao, [X|Vs], C, G). 335prep_args([X|T], [Y|T2], Ai, Ao, Vs, C, Go) :- 336 X =.. [F|X2], % X is a compound term; process it. 337 !, 338 prep_args2(X2, X3, Vs, Vs2, C, C2, Gs), 339 Xo =.. [F|X3], 340 G = (Y=Xo), % create unification goal 341 !, 342 prep_args(T, T2, [Y|Ai], Ao, Vs2, C2, Gt), 343 append([G|Gs], Gt, Go). 344prep_args([X|T], [Y|T2], Ai, Ao, Vs, C, [G|Gt]) :- 345 G = (Y=X), % create unification goal 346 prep_args(T, T2, [Y|Ai], Ao, Vs, C, Gt). 347 348%! prep_args2(+ArgsIn:list, -ArgsOut:list, 349%! +VarsSeenIn:list, -VarsSeenOut:list, 350%! +CounterIn:int, -CounterOut:int, -UniGoals:list) is det 351% 352% Given the arguments from a compound term, create unifiability goals 353% to be used in the dual. 354% 355% @arg ArgsIn Input args. 356% @arg ArgsOut Output args. 357% @arg VarsSeenIn Input vars seen. 358% @arg VarsSeenOut Output vars seen. 359% @arg CounterIn Input counter. 360% @arg CounterOut Output counter. 361% @arg UniGoals List of unification goals. 362 363:- det(prep_args2/7). 364 365prep_args2([], [], Vs, Vs, C, C, []). 366prep_args2([X|T], [Y|T2], Vsi, Vso, Ci, Co, [G|Gt]) :- 367 is_var(X), 368 !, 369 ( memberchk(X, Vsi) % X has been seen 370 -> Vs1 = Vsi 371 ; Vs1 = [X|Vsi] 372 ), 373 atom_concat('_Y', Ci, Y), 374 C1 is Ci + 1, 375 G = (Y=X), % create unification goal 376 prep_args2(T, T2, Vs1, Vso, C1, Co, Gt). 377prep_args2([X|T], [Y|T2], Vsi, Vso, Ci, Co, Go) :- 378 X =.. [F|X2], % X is a compound term 379 !, 380 atom_concat('_Y', Ci, Y), 381 C1 is Ci + 1, 382 prep_args2(X2, X3, Vsi, Vs1, C1, C2, Gs), 383 Xo =.. [F|X3], 384 G = (Y=Xo), % create unification goal 385 prep_args2(T, T2, Vs1, Vso, C2, Co, Gt), 386 append([G|Gs], Gt, Go). 387prep_args2([X|T], [Y|T2], Vsi, Vso, Ci, Co, [G|Gt]) :- 388 % X isn't a variable or compound term 389 atom_concat('_Y', Ci, Y), 390 C1 is Ci + 1, 391 G = (Y=X), % create unification goal 392 prep_args2(T, T2, Vsi, Vso, C1, Co, Gt)