1:- module(diseq_oracle,
    2          [ (..=..)/2,
    3            (..\=..)/2,
    4            v/0,
    5
    6            op(700, xfx, ..=..),
    7            op(700, xfx, ..\=..)
    8          ]).    9
   10:- op(700, xfx, .=.).   11:- op(700, xfx, .\=.).   12
   13v :-
   14    wrap_predicate(clp_disequality_rt:(A .=. B), diseq,
   15                   Wrapped1,
   16                   diseq_oracle:v1(A,B,Wrapped1)),
   17    wrap_predicate(clp_disequality_rt:(A2 .\=. B2), diseq,
   18                   Wrapped2,
   19                   diseq_oracle:v2(A2,B2,Wrapped2)).
   20
   21
   22v1(A,B,Wrapped) :-
   23    copy_term(A+B, CA+CB),
   24    (   Wrapped
   25    ->  (   CA ..=.. CB
   26        ->  (   A+B =@= CA+CB
   27            ->  true
   28            ;   format(user_error, 'Different constraints for ~p~n', [A .=. B])
   29            )
   30        ;   format(user_error, 'Should fail ~p~n', [A .=. B]),
   31            break
   32        )
   33    ;   (   CA ..=.. CB
   34        ->  format(user_error, 'Should succeed ~p~n', [A .=. B])
   35        ;   true
   36        )
   37    ).
   38
   39
   40v2(A,B,Wrapped) :-
   41    copy_term(A+B, CA+CB),
   42    (   Wrapped
   43    ->  (   CA ..\=.. CB
   44        ->  copy_term(A+B,A1+B1,C1a),
   45            copy_term(CA+CB,CA1+CB1,CC1a),
   46            sort(C1a, C1),
   47            sort(CC1a, CC1),
   48            (   A1+B1+C1 =@= CA1+CB1+CC1
   49            ->  true
   50            ;   format(user_error, 'Different constraints for ~q~n', [(A1 .\=. B1 -> C1)]),
   51                format(user_error, 'Different constraints for ~q~n', [(CA1 .\=. CB1 -> CC1)])
   52            )
   53        ;   format(user_error, 'Should fail ~p~n', [A .\=. B]),
   54            break
   55        )
   56    ;   (   CA ..\=.. CB
   57        ->  format(user_error, 'Should succeed ~p~n', [A .\=. B])
   58        ;   true
   59        )
   60    ).
   61
   62
   63
   64
   65%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   66%% Constructive Unification %%
   67%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   73..=..(A,B) :-
   74    neg_var(A,NegListA),
   75    nonvar(B), !,
   76    not_unify(B, NegListA),
   77    clean(A),
   78    A = B.
   79
   80..=..(B,A) :-
   81    neg_var(A,NegListA),
   82    nonvar(B), !,
   83    not_unify(A, NegListA),             % JW: BUG!
   84    clean(A),
   85    A = B.

   90..=..(A,B) :-
   91    neg_var(A,NegListA),
   92    neg_var(B,NegListB), !,
   93    ord_union(NegListA,NegListB,NegList),
   94    update(A,NegList),
   95    clean(B),
   96    B = A.

  103..=..([A|As], [B|Bs]) :- true, !,
  104    length(As,N), length(Bs,N),
  105    A ..=.. B,
  106    As ..=.. Bs.
  107
  108..=..(A,B) :-
  109    compound(A),
  110    compound(B), !,
  111    A =.. [Name | La],
  112    B =.. [Name | Lb],
  113    La ..=.. Lb.

  118..=..(A,B) :-
  119    A = B.
  120
  121%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  122%% Constructive disunification %%
  123%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  124
  125..\=..(A,B) :-
  126    ground(A),
  127    ground(B), !,
  128    A \= B.
  129
  130/*
  131..\=..(A,B) :-
  132    is_clpq_var(A), !,
  133    disequality_clpq(A,B).
  134..\=..(A,B) :-
  135    is_clpq_var(B), !,
  136    disequality_clpq(B,A).
  137*/
  138% ..\=..(A,B) :-
  139%       var(A),
  140%       num(B),
  141%       disequality_clpq(A,B).
  142% ..\=..(A,B) :-
  143%       var(B),
  144%       num(A),
  145%       disequality_clpq(B,A).

  151..\=..(A,B) :-
  152    neg_var(A,NegListA),
  153    ground(B), !,
  154    ord_add_element(NegListA,B,NegList),
  155    update(A,NegList).
  156
  157..\=..(B,A) :-
  158    neg_var(A,NegListA),
  159    ground(B), !,
  160    ord_add_element(NegListA,B,NegList),
  161    update(A,NegList).

  167..\=..(A,B) :-
  168    var(A), var(B),
  169    \+ ground(A),
  170    \+ ground(B), !,
  171%       send_silent_signal(error),
  172%       format('ERROR: disunification expect at least one argument to be ground, got:\n~p\n~p\n',[A,B]),
  173    fail.

..\=..([],[]) :- !, fail. ..\=..(ListA, ListB) :- \+ var(ListA), \+ var(ListB), ListA = [A|As], ListB = [B|Bs], !, format('disequality ~p \= ~p\n',[ListA,ListB]), ( format('\tdisequality ~p \= ~p\n',[A,B]), A ..\=.. B ; format('\tdisequality ~p \= ~p\n',[A,B]), As ..\=.. Bs ).

  200% ..\=..(A,B) :-
  201%       \+ var(A),
  202%       \+ var(B),
  203%       struct(A),
  204%       struct(B), !,
  205%       A =.. [NameA | As],
  206%       B =.. [NameB | Bs],
  207%       (
  208%           NameA \= NameB ->
  209%           true
  210%       ;
  211%           As ..\=.. Bs
  212%       ).
  213
  214..\=..(A,B) :-
  215    \+ var(A),
  216    \+ var(B),
  217    compound(A),
  218    compound(B), !,
  219%       format('check_dual(~p \= ~p)\n',[A,B]),
  220    (
  221        unifiable(A,B,Unifier) ->
  222%           format('check_dual(~p)\n',[Unifier]),
  223        check_dual(Unifier)
  224    ;
  225        true
  226    ).
  227
  228% ..\=..(A,B) :-
  229%       print('vars'),
  230%       disequality_clpq(A,B).

  235..\=..(A,B) :-
  236    \+ var(A), \+ var(B),
  237    A \= B.
  238
  239check_dual([A=B|_]) :-
  240    A ..\=.. B.
  241check_dual([_|Ds]) :-
  242    check_dual(Ds).
  243
  244not_unify(_A, []) :- !.
  245not_unify(A, [X|Xs]) :-
  246    A ..\=.. X,
  247    not_unify(A,Xs).
  248
  249neg_var(A,List) :-
  250    (
  251        get_attr(A,diseq_oracle,neg(List)), true ->
  252        true
  253    ;
  254        var(A),
  255        List = [],
  256        put_attr(A,diseq_oracle,neg(List))
  257    ).
  258
  259update(A,List) :- put_attr(A,diseq_oracle,neg(List)).
  260
  261clean(A) :- del_attr(A, diseq_oracle).
  262
  263attr_unify_hook(neg(A),B) :-
  264    (
  265        not_unify(B,A) ->
  266        true
  267    ;
  268        % print('Fail unification between:  '),
  269        % print(B),print('  and the neg list '), print(A),nl,
  270        fail
  271    ).
  272
  273attribute_goals(X) -->
  274    [.\=.(X, G)],
  275    {get_attr(X,diseq_oracle,neg(G))}