1:- module(scasp_clp_disequality,
    2          [ get_neg_var/2,
    3            not_unify/2,
    4            (.=.)/2,
    5            (.\=.)/2,
    6            '\u2209'/2,                 % ?X, +G
    7            loop_term/2,
    8
    9            op(700, xfx, .=.),
   10            op(700, xfx, .\=.),
   11            op(700, xfx, '\u2209')      % Not an element of
   12          ]).   13:- use_module(library(debug)).   14:- use_module(library(lists)).   15:- use_module(library(ordsets)).   16:- use_module(library(dif), [dif/2]).   % use in :- if
   17
   18:- use_module('../verbose').   19:- use_module(clpq).   20
   21:- encoding(utf8).

   36		 /*******************************
   37		 *   CONSTRUCTIVE UNIFICATION   *
   38		 *******************************/

 .=.(A, B)

Constructive unification of a negatively constrained variable with a non- variable value will succeed if the non-variable value does not constructively unify with any element in the variable’s prohibited value list.

   47:- if(\+((dif(A,b), unifiable(a(A), a(b), _)))).   48:- format(user_error, 'ERROR: unifiable/3 validates constraints~n', []),
   49   halt(1).   50:- endif.   51
   52.=.(A,B) :-
   53    unifiable(A,B,U),
   54    unify(U).
   55
   56unify([]).
   57unify([Var=Value|T]) :-
   58    unify2(Var, Value),
   59    unify(T).
   60
   61unify2(A, B) :-
   62    nonvar(B),
   63    !,
   64    (   get_neg_var(A,NegListA)
   65    ->  not_unify(B, NegListA),
   66        clean(A)
   67    ;   true
   68    ),
   69    A = B.
   70% - Constructive unification of two negatively constrained variables
   71% will always succeed, setting their shared prohibited value list to
   72% the union of their original lists.
   73unify2(A, B) :-
   74    get_neg_var_or_empty(A,NegListA),
   75    get_neg_var_or_empty(B,NegListB),
   76    !,
   77    ord_union(NegListA,NegListB,NegList),
   78    update(A,NegList),
   79    clean(B),
   80    B = A.
   81% - In cases where neither argument contains a negatively constrained
   82% variable, the result is identical to that of traditional
   83% unification.
   84unify2(A,B) :-
   85    A = B.
   86
   87		 /*******************************
   88		 *  CONSTRUCTIVE DISUNIFICATION	*
   89		 *******************************/

 .\=.(A, B)

   93.\=.(A,B) :-
   94    (   unifiable(A,B,U0)
   95    ->  reverse(U0, U),
   96        member(Var=Value, U),
   97        not_unify2(Var, Value)
   98    ;   true
   99    ).
  100
  101% - in accordance with the restrictions given in Section 3.1.5,
  102% constructive disunification of two non ground variables will
  103% produce an error
  104not_unify2(_,B) :-
  105    var(B),
  106    !,
  107    fail.
  108not_unify2(A, B) :-
  109    is_clpq_var(A), !,
  110    disequality_clpq(A,B).
  111% - Constructive disunification of a negatively constrained variable
  112% and a non- variable value will always succeed, adding the
  113% "ground" value to the variable’s prohibited value list.
  114not_unify2(A, B) :-
  115    ground(B),
  116    neg_var(A, NegListA),
  117    ord_add_element(NegListA, B, NegList),
  118    update(A, NegList).

 not_unify(+Term, +List)

True when Term cannot unify with any of the elements in List

  124not_unify(_A, []) :- !.
  125not_unify(A, [X|Xs]) :-
  126    A .\=. X,
  127    not_unify(A,Xs).

 loop_term(+Goal1, +Goal2)

  133loop_term(Goal1, Goal2) :-
  134    functor(Goal1, Name, Arity),
  135    assertion(functor(Goal2, Name, Arity)),
  136    loop_term(1, Arity, Goal1, Goal2).
  137
  138loop_term(I, Arity, Goal1, Goal2) :-
  139    I =< Arity,
  140    arg(I, Goal1, A),
  141    arg(I, Goal2, B),
  142    (   loop_var_disequality(A,B)
  143    ->  true
  144    ;   A .=. B,
  145        I2 is I+1,
  146        loop_term(I2, Arity, Goal1, Goal2)
  147    ).

 loop_var_disequality(?A, ?B)

???

  154loop_var_disequality(A, B) :-
  155    neg_var(A, ListA),
  156    neg_var(B, ListB),
  157    (   ListA == [],
  158        ListB \== []
  159    ->  loop_var_disequality_(A, ListB)
  160    ;   ListB == [],
  161        ListA \== []
  162    ->  loop_var_disequality_(B, ListA)
  163    ).
  164loop_var_disequality(A, B) :-
  165    verbose(format('\t\tLoop_var_disequality( ~p , ~p )\n',[A,B])),
  166    A .\=. B.
  167
  168loop_var_disequality_(A, [NegB|_]) :-
  169    A .=. NegB.
  170loop_var_disequality_(A, [_|NegBs]) :-
  171    loop_var_disequality_(A, NegBs).
  172
  173
  174		 /*******************************
  175		 *     AUXILIAR PREDICATES      *
  176		 *******************************/
  177
  178neg_var(A, List) :-
  179    (   get_attr(A, scasp_clp_disequality, neg(List))
  180    ->  true
  181    ;   var(A)
  182    ->  List = [],
  183        put_attr(A, scasp_clp_disequality, neg(List))
  184    ).
  185
  186get_neg_var(A,List) :-
  187    get_attr(A, scasp_clp_disequality, neg(List)).
  188
  189get_neg_var_or_empty(A,List) :-
  190    var(A),
  191    (   get_attr(A,scasp_clp_disequality,neg(List))
  192    ->  true
  193    ;   List = []
  194    ).
  195
  196clean(A) :-
  197    del_attr(A, scasp_clp_disequality).
  198
  199update(A,List) :-
  200    put_attr(A,scasp_clp_disequality,neg(List)).

 ∉(?X, +G)

Constraint that expresses that X is not a member of the list of ground elements in G.

  207'\u2209'(X, G) :-
  208    ground(X),
  209    \+ memberchk(X, G).
  210'\u2209'(X, G) :-
  211    get_neg_var(X, List),
  212    sort(G, GS),
  213    ord_union(List, GS, NewList),
  214    update(X, NewList).
  215'\u2209'(X, G) :-
  216    var(X),
  217    !,
  218    sort(G, GS),
  219    update(X, GS).
  220
  221
  222attr_unify_hook(neg(A),B) :-
  223    not_unify(B, A).
  224
  225attribute_goals(X) -->
  226    { get_neg_var(X, G)
  227    },
  228    (   {current_prolog_flag(scasp_unicode, true)}
  229    ->  [ '\u2209'(X, G) ]
  230    ;   [.\=.(X, G)]
  231    ).
  232
  233attr_portray_hook(neg(List), Var) :-
  234    (   current_prolog_flag(scasp_unicode, true)
  235    ->  format("~p \u2209 ~p",[Var,List])
  236    ;   format("~p .\\=. ~p",[Var,List])
  237    )