%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%
%% simple constraint solver for inequalities between variables
%% thom fruehwirth ECRC 950519, LMU 980207, 980311
%%
%% ported to hProlog by Tom Schrijvers 
%% translated into AR by N.F. Zhou, March 2006

main :-
	main(60).
%	main(25).

main(N):-
	cputime(X),
	length(L,N),
	genleq(L,Last),
	L=[First|_],
       writeln(posting(last)),
	leq(Last,First),
       writeln(L),
	cputime( Now),
	Time is Now-X,
	write(bench(leq ,N,Time,0,bp_ar)), write('.'),nl.

genleq([Last],Last) :- ! .
genleq([X,Y|Xs],Last):-
	leq(X,Y),
	genleq([Y|Xs],Last).

%%% reflexivity  @ leq(X,X) <=> true.   % Occ 1
%%% antisymmetry @ leq(X,Y), leq(Y,X) <=> X = Y. % Occ 2 and 3, combined 23
%%% idempotence  @ leq(X,Y) \ leq(X,Y) <=> true. % Occ 4 and 5, combined 45
%%% transitivity @ leq(X,Y), leq(Y,Z) ==> leq(X,Z). % Occ 5 6
leq(X,Y):-
    new_constr_num(Cno),
    Constr=leq(Cno,Flag,X,Y),  
    %
    leq_2_1(Flag,X,Y),
    %
    % A1XCh?: All constraints that have X as the first argument 
    % A2XCh?: All constraints that have X as the second argument 
    % A1YCh?: All constraints that have Y as the first argument 
    % A2YCh?: All constraints that have Y as the second argument 
    Channels=chs(A1XCh2,A1XCh3,A1XCh4,A2XCh2,A2XCh3,A2XCh4,A1YCh2,A1YCh3,A1YCh4,A2YCh2,A2YCh3,A2YCh4),
    get_channels(leq_3_arg1,X,chs(A1XCh2,A1XCh3,A1XCh4)),
    get_channels(leq_3_arg2,X,chs(A2XCh2,A2XCh3,A2XCh4)),
    get_channels(leq_3_arg1,Y,chs(A1YCh2,A1YCh3,A1YCh4)),
    get_channels(leq_3_arg2,Y,chs(A2YCh2,A2YCh3,A2YCh4)),

    %
    leq_2_23(Cno,A1XCh2,A2YCh2,Flag,X,Y),    
    %
    leq_2_45(Cno,A1XCh3,A2YCh3,Flag,X,Y),
     %
    new_hashtable(History),
    leq_2_56(Cno,A1XCh4,A2YCh4,Flag,History,X,Y),
    %
    post_leq_3(Flag,Channels,Constr,X,Y).

%%    Called when either variable in leq(X,Y) is instantiated
post_leq_3(Flag,Channels,Constr,X,Y),var(Flag),
    {generated,ins(Flag),ins(X),ins(Y)} 
=>
    Channels=chs(A1XCh2,A1XCh3,A1XCh4,A2XCh2,A2XCh3,A2XCh4,A1YCh2,A1YCh3,A1YCh4,A2YCh2,A2YCh3,A2YCh4),
    get_channels(leq_3_arg1,X,chs(A1XCh2,A1XCh3,A1XCh4)),
    get_channels(leq_3_arg2,X,chs(A2XCh2,A2XCh3,A2XCh4)),
    get_channels(leq_3_arg1,Y,chs(A1YCh2,A1YCh3,A1YCh4)),
    get_channels(leq_3_arg2,Y,chs(A2YCh2,A2YCh3,A2YCh4)),
    %
    (var(Flag)->post_event(A1YCh2/\A2XCh2,Constr);true), % to agents leq(Y,X)
    %
    (var(Flag)->post_event(A1XCh3/\A2YCh3,Constr);true), % to agents leq(X,Y) 
     %
    (var(Flag)->post_event_df(A1YCh4\/A2XCh4,Flag,Constr);true). % to agents leq(Y,_) or leq(_,X)
post_leq_3(Flag,Channels,Constr,X,Y) => true.

leq_2_1(Flag,X,Y),var(Flag),
    {generated,ins(Flag),ins(X),ins(Y)} 
=> 
    (X==Y->Flag=1;true).
leq_2_1(Flag,X,Y) => true.

%%% antisymmetry @ leq(X,Y), leq(Y,X) <=> X = Y.
leq_2_23(Cno,C1,C2,Flag,X,Y),var(Flag),{event(C1,Q),event(C2,Q),ins(Flag)} =>
     Q=leq(CnoQ,FlagQ,U,V),
     (CnoQ\==Cno,var(FlagQ)->  
         (X==V,Y==U -> Flag=1,FlagQ=1,X=Y;true)
      ;
          true
      ).
leq_2_23(Cno,C1,C2,Flag,X,Y) => true.

%%% idempotence  @ leq(X,Y) \ leq(X,Y) <=> true.
leq_2_45(Cno,C1,C2,Flag,X,Y),var(Flag),{event(C1,Q),event(C2,Q),ins(Flag)} =>
     Q=leq(CnoQ,FlagQ,U,V),
     (CnoQ\==Cno,var(Flag),var(FlagQ)->
          (X==U,Y==V -> FlagQ=1;true)
      ;
          true
      ).
leq_2_45(Cno,C1,C2,Flag,X,Y) => true.

%%% transitivity @ leq(X,Y), leq(Y,Z) ==> leq(X,Z).
% no instance can be fired more than once
leq_2_56(Cno,C1,C2,Flag,History,X,Y),var(Flag),{event(C1,Q),event(C2,Q),ins(Flag)} =>
     Q=leq(CnoQ,FlagQ,U,V),
     (CnoQ\==Cno,var(FlagQ)->
        (hashtable_get(History,CnoQ,_)-> 
            true
         ;Y==U->
%              writeln((leq(Cno,X,Y),leq(CnoQ,U,V)=>leq(X,V))),
            hashtable_put(History,CnoQ,_),
            leq(X,V)
          ;X==V->
%            writeln((leq(CnoQ,U,V),leq(Cno,X,Y)=>leq(U,Y))),
            hashtable_put(History,CnoQ,_),
            leq(U,Y)
	   ; 
            true
          )
      ;
          true
      ).
leq_2_56(Cno,C1,C2,Flag,History,X,Y) => true.


:-include('chr_lib.pl').