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