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(common).   45:- use_module(program).   46:- use_module(variables).   47:- use_module(options).   48
   49:- 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.

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

 comp_dual(+Predicate) is det

get matching rules and call comp_duals3/2.

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

 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.

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

 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.

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

 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.

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

 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.

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

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

Given a goal, negated it.

Arguments:

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

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

 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.

  256define_forall(G, G, []) :-
  257    !.
  258define_forall(Gi, forall(X, G2), [X|T]) :-
  259    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.

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

 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.

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

 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.

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

 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.

  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)