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

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

 comp_duals is det

Compute rules for the negations of positive literals (dual rules), even if there are no clauses for the positive literal (negation will be a fact). Wrapper for comp_duals2/1.

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

 comp_dual(+Predicate) is det

get matching rules and call comp_duals3/2.

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

 comp_duals3(+Predicate:atom, +Rules:list) is det

Compute the dual for a single positive literal. Make sure that Predicate is used for the dual head instead of taking the head from one of the rules. This allows a new head to be passed during NMR sub-check creation.

Arguments:

Predicate	- The head of each rule in Rules, of the form Head/arity.
Rules	- The list of rules for a single predicate.

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

 comp_dual(+DualHead:compound, +Rules:list, -DualBody:list, +Count:int) is det

Compute the dual for a predicate with multiple rules. First, compute the dual of each individual rule, replacing each head with a new, unique one. Then create the overall dual using the heads of the individual duals as goals. When finished, assert the overall dual.

Arguments:

DualHead	- The head of the dual rule.
Rules	- The list of rules.
DualBody	- The body of the outer dual rule.
Count	- Counter used to ensure that new heads are unique.

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

 comp_dual2(+DualHead:compound, +Body:list, +BodyVars:list) is det

Compute the dual for a single clause. Since any body variables in the original rule are existentially, they must be universally quantified in the dual. This is accomplished by creating a new predicate with both the original head variables and the body variables in the head, which will contain the duals of the original goals. The "inner dual" will then call this new predicate in a forall over the body variables.

Arguments:

DualHead	- The head of the dual rule.
Body	- The body of the original rule.
BodyVars	- The list of variables in the body but not the head.

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

 comp_dual3(+DualHead:compound, +Body:list, +UsedGoals:list) is det

Compute the innermost dual for a single rule by negating each goal in turn. Unlike grounded ASP, it is not enough to have a single-goal clause for each original goal. Because side effects are possible, the sub-dual for a given goal must include all previous goals and retain program order.

Arguments:

DualHead	- The head of the dual rule.
Body	- The body goals to negate.
UsedGoals	- The goals that have already been processed, in original order.

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

 dual_goal(+GoalIn:compound, -GoalOut:compound) is det

Given a goal, negated it.

Arguments:

GoalIn	- The original goal.
GoalOut	- The negated goal.

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

 define_forall(+GoalIn:compound, -GoalOut:compound, +BodyVars:list) is det

If BodyVars is empty, just return the original goal. Otherwise, define a forall for the goal. For multiple body variables, the forall will be nested, with each layer containing a single variable.

Arguments:

GoalIn	- Input goal.
GoalOut	- Output goal.
BodyVars	- Body variables present in GoalIn.

  259define_forall(G, G, []) :-
  260    !.
  261define_forall(Gi, forall(X, G2), [X|T]) :-
  262    define_forall(Gi, G2, T).

 outer_dual_head(+Head:atom, -DualHead:compound) is det

Create the dual version of a rule head by negating the predicate name and replacing the args with a variable list of the same arity.

Arguments:

Head	- The initial, positive head, a predicate name.
DualHead	- The dual head, a predicate struct.

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

 abstract_structures(+ArgsIn:list, -ArgsOut:list, +Counter:int, -Goals:list) is det

Given a list of args, abstract any structures by replacing them with variables and adding a goal unifying the variable with the structure.

Arguments:

ArgsIn	- The original args from a clause head.
ArgsOut	- Output new args.
Counter	- Input counter.
Goals	- Goals unifying non-variables with the variables replacing them.

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

 prep_args(+OrigArgs:list, +VarArgs:list, +NewArgsIn:list, -NewArgsOut:list, +VarsSeen:list, +Counter:int, -Goals:list) is det

Given two sets of args, check if each of the original args is a variable. If so, check if it's a member of NewArgsIn. If it's not, add it to output args. If it isn't a variable, or the variable is present in NewArgsIn, add the corresponding variable from VarArgs. The result is a list of variables that keeps any variables in the original head. When an element from VarArgs is used, add a unification (=) goal to Goals.

Arguments:

OrigArgs	- The original args from a clause head.
VarArgs	- A list of unique variable names of the same length as OrigArgs.
NewArgsIn	- Input new args.
NewArgsOut	- Output new args.
VarsSeen	- List of variables encountered in original args.
Counter	- Input counter.
Goals	- Goals unifying non-variables with the variables replacing them.

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

 prep_args2(+ArgsIn:list, -ArgsOut:list, +VarsSeenIn:list, -VarsSeenOut:list, +CounterIn:int, -CounterOut:int, -UniGoals:list) is det

Given the arguments from a compound term, create unifiability goals to be used in the dual.

Arguments:

ArgsIn	- Input args.
ArgsOut	- Output args.
VarsSeenIn	- Input vars seen.
VarsSeenOut	- Output vars seen.
CounterIn	- Input counter.
CounterOut	- Output counter.
UniGoals	- List of unification goals.

  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)