:-T='Arrovian possibility theorem by prolog '
,N='(swf_d.pl, 5-7,21,25 Feb, 2-7 Mar 2006)'
,H='----------------------------------------'
,forall(member(X,[H,T,N,H]),(nl,write(X))),nl.

% References:
% [1] Arrow, K. (1951/1963). 
%  Social Choice and Individual Values.
%  Cowles Foundation Monograph 12.
% [2] Sen, A. (1995). 
%  Rationality and social choice.
%  American Economic Review 85(1):1-24. 
% [3] S. Barbera (1980).
%  Pivotal voters: A new proof of Arrow's theorem.
%  Economic Letters 6: 13-6.

% Definitions
%-------------------------------------------------
% A: a set of social states(alternatives of social choice), 
% N=[1,2,,...,n] : a set of agents(the members of the society). 
% R=[r(1),r(2),...,r(n)]: a profile of weak orderings of individual agents. 

% Def. (unristricted domain; UD)
%   None of the logically possible orderings may be excluded. 
% Def. (social welfare function; SWF) 
%   f: profiles of weak orderings R^n over A -> weak orderings R over A.
% Def. (decisiveness of a group G over (x,y)
%   A subset G of N is decisive if for a pair (x,y) in A^2,
%   the swf r=f(R)is such that r(X,Y)<->r(G,X,Y) for (X,Y) is (x,y) or (y,x).  
% Def. (decisiveness of G)
%   A subset G of N is decisive if for any pair (x,y) in A^2,
%   decisive(G,x,y). 
% Def. (Pareto principle)  N is decisive.
% Def. (dictatorship)  For a member J in N, [J] is decisive.
% Def. (independence of irrelevant alternatives;IIA)
%   If r(x,y) is not depend on any r(j,A,B)
%   such that (A,B) is neither (x,y) or (y,x).

% Theorem(Arrow). Suppose UD and IIA. Then decisive(N)->decisive([J]).
% Lemma. subset(G,N),decisive(G,X,Y)-> decisive(G).
% Lemma. decisive(G)->(partition(G1,G2,G),member(A,[G1,G2]),decisive(A)). 


%-------------------------------------------------
%  Social Choice Model
%-------------------------------------------------
% since: 5 Feb 2006.

% 2 person 3 alternatives example
%-------------------------------------------------

alternative(a).
alternative(b).
alternative(c).

agent(1).
agent(2).

set_of_alternatives([a,b,c]).
set_of_agents([1,2]).

group([1]).
group([2]).
group([1,2]).

counter_group(G,H):-
   set_of_agents(N),
   group(G),
   subtract(N,G,H).


% modeling the weak orderings
% of the 2x3 unrestricted domain
%-------------------------------------------------
% In favor of brevity,
% we will concentrate on the strict part of it. 

possible_preference_ordering( r(1), [a,b,c]).
possible_preference_ordering( r(2), [a,c,b]).
possible_preference_ordering( r(3), [b,a,c]).
possible_preference_ordering( r(4), [b,c,a]).
possible_preference_ordering( r(5), [c,a,b]).
possible_preference_ordering( r(6), [c,b,a]).


possible_preference_of_agent( J, R, O):-
   agent(J),
   possible_preference_ordering(R, O).

strictly_prefer_to(A,B, R):-
   possible_preference_ordering( R, O),
   append( _,[A|C],O),
   member(B,C).

maximal_element( X, R):-
   possible_preference_ordering( R,[X|_O]).


% 2 person 3 alternatives unrestricted domain
%-------------------------------------------------

possible_preference_of_group( G, R, O):-
   group(G),
   possible_preference_of_group_1( G, R, O).

possible_preference_of_group_1( [], [], []).
possible_preference_of_group_1( [J|G], [R1|R], [(J,R1)|P]):-
   possible_preference_of_group_1( G, R, P),
   possible_preference_of_agent( J, R1, _).


possible_preference_pair( urd(2,3), (R1, R2),(O1,O2)):-
   possible_preference_of_group( [1,2], [R1,R2], [O1,O2]).



/*

?- setof(J,A^B^C^D^possible_preference_pair( H, (r(J),r(K)),_),
L),nl,write(H;K;L),fail.

urd(2, 3);1;[1, 2, 3, 4, 5, 6]
urd(2, 3);2;[1, 2, 3, 4, 5, 6]
urd(2, 3);3;[1, 2, 3, 4, 5, 6]
urd(2, 3);4;[1, 2, 3, 4, 5, 6]
urd(2, 3);5;[1, 2, 3, 4, 5, 6]
urd(2, 3);6;[1, 2, 3, 4, 5, 6]

No
?- 

*/


%-------------------------------------------------
%  SWFs for the unrestricted domain
%-------------------------------------------------

%social_welfare_function( urd(2,3), swf(auto)).
social_welfare_function( urd(2,3), swf(1)).
social_welfare_function( urd(2,3), swf(2)).
social_welfare_function( urd(2,3), swf(3)).
%social_welfare_function( urd(2,3), free).
social_welfare_function( urd(2,3), bin).

social_welfare_function( urd(2,3), swf(1),[r(J),R2]->r(J)):-
   possible_preference_of_group( [1,2], [r(J),R2], _).
social_welfare_function( urd(2,3), swf(2),[R1,r(K)]->r(K)):-
   possible_preference_of_group( [1,2], [R1,r(K)], _).
social_welfare_function( urd(2,3), swf(3),[r(J),r(K)]->r(L)):-
   possible_preference_of_group( [1,2], [r(J),r(K)], _),
   L is (K+J) mod 5 + 1.

social_welfare_function( urd(2,3), free,[r(J),r(K)]->r(L)):-
   possible_preference_of_group( [1,2], [r(J),r(K)], _),
   possible_preference_ordering( r(L), _).

% the binary ( added:  2 Mar 2006)

social_welfare_function( urd(2,3), bin,[r(J),r(K)]->r(L)):-
   possible_preference_of_group( [1,2], [r(J),r(K)], _),
   possible_preference_ordering( r(L), _),
   forall(
     swf_xy_0( _, (X,Y), (J,K)),
     strictly_prefer_to(X,Y, r(L))
   ),
   forall(
     strictly_prefer_to(X,Y, r(L)),
     swf_xy_0( _, (X,Y), (J,K))
   ).


%  displaying swfs
%-------------------------------------------------

preprocess_for_display_swf(Swf,F):-
   social_welfare_function( urd(2,3), Swf),
   \+ member(Swf, [free,bin]),
  %W = ([r(J),r(K)]->C),
   G = social_welfare_function( urd(2,3), Swf,W),
   findall( W, G, F).

preprocess_for_display_swf(bin,F):-
   W = ([r(J),r(K)]->C),
   G = social_welfare_function( urd(2,3), bin,W),
   P = possible_preference_of_group( [1,2], [r(J),r(K)], _),
   T = transitivity_in_swf_xy_0((J,K)),
   Pict = (\+ T->C='XXXX';C='----'),
   findall( W, (P,(G->true;Pict)), F).

preprocess_for_display_swf((X,Y),bin,F):-
   W = ([r(J),r(K)]->C),
   G1 = swf_xy_0(_, (X,Y),(J,K)),
   G2 = swf_xy_0(_, (Y,X),(J,K)),
   P = possible_preference_of_group( [1,2], [r(J),r(K)], _),
   findall( W, (P,(G1->C=X;G2->C=Y;C='-')), F).

display_swf((X,Y),Swf):-
   distinct_pair_of_alternatives(X,Y),
   X@<Y,
   preprocess_for_display_swf((X,Y),Swf,F),
   display_auto_swf(F).

display_swf(Swf):-
   preprocess_for_display_swf(Swf,F),
   display_auto_swf(F).

display_swf_n(Swf):-
   preprocess_for_display_swf(Swf,F),
   display_auto_swf_n(F).

/*

?- display_swf(H).

row=1;[r(1), r(1), r(1), r(1), r(1), r(1)]
row=2;[r(2), r(2), r(2), r(2), r(2), r(2)]
row=3;[r(3), r(3), r(3), r(3), r(3), r(3)]
row=4;[r(4), r(4), r(4), r(4), r(4), r(4)]
row=5;[r(5), r(5), r(5), r(5), r(5), r(5)]
row=6;[r(6), r(6), r(6), r(6), r(6), r(6)]

H = swf(1) 

Yes
?- 

*/


%-------------------------------------------------
%  Binary relation based modeling for SWF
%-------------------------------------------------
% added: 2-5 Mar 2006.

swf_xy( pareto,(X,Y),(R1,R2)):-
   strictly_prefer_to(X,Y, r(R1)),
   strictly_prefer_to(X,Y, r(R2)).

same_binary_pattern((X,Y),R,Q):-
   strictly_prefer_to(X,Y, r(R)),
   strictly_prefer_to(X,Y, r(Q)).

same_binary_pattern((X,Y),R,Q):-
   strictly_prefer_to(Y,X, r(R)),
   strictly_prefer_to(Y,X, r(Q)).

included_in_iia_profile_class((X,Y),(J,K),C):-
   distinct_pair_of_alternatives(X,Y),
   possible_preference_of_group( [1,2], [r(J),r(K)], _),
   findall((Q,R),
    (
     same_binary_pattern((X,Y),J,Q),
     same_binary_pattern((X,Y),K,R)
    ),
   C).

% analyzing iia profiles
%-------------------------------------------------

classes_of_iia_profiles((X,Y),C):-
   findall((J,K),
     possible_preference_of_group( [1,2], [r(J),r(K)], _),
   P),
   class_of_iia_profiles_1((X,Y),C,P).

class_of_iia_profiles_1(_,[],[]).

class_of_iia_profiles_1((X,Y),[C|H],[(J,K)|P]):-
   included_in_iia_profile_class((X,Y),(J,K),C),
   subtract( P, C, Q),
   class_of_iia_profiles_1((X,Y),H,Q).

preprocess_for_display_iia((X,Y),F):-
   W = ([r(J),r(K)]->C),
   G = (
     (strictly_prefer_to(X,Y,r(J))->A=X;A=Y),
     (strictly_prefer_to(X,Y,r(K))->B=X;B=Y),
     concat(A,B,C)
   ),
   P = possible_preference_of_group( [1,2], [r(J),r(K)], _),
   findall( W, (P,G), F).

preprocess_for_display_iia_1((X,Y),F):-
   W = ([r(J),r(K)]->M),
   G = (
     classes_of_iia_profiles((X,Y),IIA),
     nth1(M,IIA,S),
     member((J,K),S)
   ),
   P = possible_preference_of_group( [1,2], [r(J),r(K)], _),
   findall( W, (P,G), F).

display_pattern_of_iia_profiles((X,Y)):-
   distinct_pair_of_alternatives(X,Y),
   preprocess_for_display_iia((X,Y),F),
   display_auto_swf(F).

display_pattern_of_iia_profiles((X@<Y)):-
   distinct_pair_of_alternatives(X,Y),
   X@<Y,
   preprocess_for_display_iia((X,Y),F),
   display_auto_swf(F).

% ab.

display_iia(S):-
   display_pattern_of_iia_profiles(S).

/*

?- display_iia((X@<Y)).

row=1;[aa, aa, ab, ab, aa, ab]
row=2;[aa, aa, ab, ab, aa, ab]
row=3;[ba, ba, bb, bb, ba, bb]
row=4;[ba, ba, bb, bb, ba, bb]
row=5;[aa, aa, ab, ab, aa, ab]
row=6;[ba, ba, bb, bb, ba, bb]

X = a
Y = b ;

row=1;[aa, aa, aa, ac, ac, ac]
row=2;[aa, aa, aa, ac, ac, ac]
row=3;[aa, aa, aa, ac, ac, ac]
row=4;[ca, ca, ca, cc, cc, cc]
row=5;[ca, ca, ca, cc, cc, cc]
row=6;[ca, ca, ca, cc, cc, cc]

X = a
Y = c ;

row=1;[bb, bc, bb, bb, bc, bc]
row=2;[cb, cc, cb, cb, cc, cc]
row=3;[bb, bc, bb, bb, bc, bc]
row=4;[bb, bc, bb, bb, bc, bc]
row=5;[cb, cc, cb, cb, cc, cc]
row=6;[cb, cc, cb, cb, cc, cc]

X = b
Y = c ;

No
?- 

*/

%-------------------------------------------------
%  Stepwise Propagation for Social Decision
%-------------------------------------------------

:- dynamic swf_xy_0/2.
:- dynamic swf_xy_0/3.

swf_xy_0( current_step, 0).

gen_swf(K):-
   (K==1;clause(swf_xy_0( current_step, 0),_)),
   K=1,
   abolish( swf_xy_0/3),
   abolish( swf_xy_0/2),
   assert( swf_xy_0( current_step, 1)),
   forall(
     swf_xy( pareto,(X,Y),R),
     assert( swf_xy_0( 1, (X,Y), R))
   ),
   write_number_of_undifined_swf_tuple.

gen_swf(K):-
   clause(swf_xy_0( current_step, K1),_),
   K1 >0,
   iia_propagated_patterns_of_binary_swf(L),
   check_transitivity_in_swf_patterns(L,(X,Y),user),
   update_current_step(_->K),
   forall(
     member(((X,Y),(Q1,Q2)),L),
     assert( swf_xy_0( K, (X,Y), (Q1,Q2)))
   ),
   write_number_of_undifined_swf_tuple.


% swf values which would be propagated via IIA
%-------------------------------------------------

iia_propagated_patterns_of_binary_swf(L):-
   findall(((X,Y),(Q1,Q2)),
    (
     deducible_relation_in_swf_xy_0((X,Y),(R1,R2)),
     same_binary_pattern((X,Y),R1,Q1),
     same_binary_pattern((X,Y),R2,Q2),
     \+ clause(swf_xy_0( _,(X,Y),(Q1,Q2)),_)
    ),
   L).

% inference based on transitivity
%-------------------------------------------------

make_transitive_closure:-
   clause(swf_xy_0(current_step,T),_),
   forall(
    (
     deducible_relation_in_swf_xy_0((X,Z),(J,K)),
     \+ clause(swf_xy_0(_,(X,Z),(J,K)),_)
    ),
     assert( swf_xy_0(T,(X,Z),(J,K)))
   ).


% checking transitivity (1)
%-------------------------------------------------

deducible_relation_in_swf_xy_0((X,Z),(J,K)):-
   possible_preference_of_group( [1,2], [r(J),r(K)],_),
   distinct_pair_of_alternatives(X,Z),
   transitively_related_in_swf_xy_0((X,Z),(J,K)).

transitively_related_in_swf_xy_0((X,Y),(J,K)):-
   swf_xy_0(_,(X,Y),(J,K)),
   !.

transitively_related_in_swf_xy_0((X,Z),(J,K)):-
   swf_xy_0(_,(X,Y),(J,K)),
   swf_xy_0(_,(Y,Z),(J,K)),
   !.

transitivity_in_swf_xy_0((J,K)):-
   \+ intransitivity_in_swf_xy_0(_,(J,K)).

intransitivity_in_swf_xy_0((X,Y),(J,K)):-
   swf_xy_0(_,(X,Y),(J,K)),
   swf_xy_0(_,(Y,X),(J,K)).

intransitivity_in_swf_xy_0((X,Y,Z),(J,K)):-
   swf_xy_0(_,(X,Y),(J,K)),
   swf_xy_0(_,(Y,Z),(J,K)),
   swf_xy_0(_,(Z,X),(J,K)).



% checking transitivity (2)
%-------------------------------------------------

check_transitivity_in_swf_patterns(L,(X,Y)):-
   forall(
     member(((X,Y),(Q,R)),L),
     is_consistent_swf_on_pair_at_profile((X,Y),(Q,R))
   ).

is_consistent_swf_on_pair_at_profile((X,Y),(Q,R)):-
   \+ \+ (
     possible_preference_ordering( r(L), _),
     strictly_prefer_to(X,Y, r(L)),
     forall(
       swf_xy_0( _, (W,Z), (Q,R)),
       strictly_prefer_to(W,Z, r(L))
     )
   ).


check_transitivity_in_swf_patterns(L,(X,Y),user):-
   check_transitivity_in_swf_patterns(L,(X,Y)),
   !.

check_transitivity_in_swf_patterns(L,(X,Y),user):-
   member(((X,Y),(Q,R)),L),
   \+ is_consistent_swf_on_pair_at_profile((X,Y),(Q,R)),
   !,
   nl,
   write(' intransitivity has detected.'),
   nl,
   write(' on pair ': (X,Y)),
   nl,
   write(' at profile ': (Q,R)),
   nl,
   write('go ahead anyway? >:'),
   %fail,
   read(y).



% messages displayed for user during swf generation
%-------------------------------------------------

write_number_of_undifined_swf_tuple:-
   number_of_undifined_swf_tuple(N1),
   N is N1 / 2,
   nl,
   swf_xy_0(current_step, K),
   write(step(K):N: 'items are undifined yet.').


warn_if_not_adjacent(_,K):-
   var(K).

warn_if_not_adjacent(K1,K):-
   \+ var(K),
   K =< K1,
   (K=1->true;write('already updated.')).

warn_if_not_adjacent(K1,K):-
   \+ var(K),
   K > K1 + 1,
   write('cannot be updated.').


% monitoring and updating on swf clauses
%-------------------------------------------------

update_current_step(K1->K):-
   clause( swf_xy_0( current_step, K1),_),
   K1 >= 1,
   warn_if_not_adjacent(K1,K),
   K is K1 + 1,
   retract( swf_xy_0( current_step, K1)),
   assert( swf_xy_0( current_step, K)).

number_of_undifined_swf_tuple(N):-
   findall(1,
     undifined_swf_tuple(_,_),
   L),
   length(L,N).



/*
?- gen_swf(1).
step(1):54:items are undifined yet.

K = 1 

Yes
?- display_swf(bin).

row=1;[r(1), ----, ----, ----, ----, ----]
row=2;[----, r(2), ----, ----, ----, ----]
row=3;[----, ----, r(3), ----, ----, ----]
row=4;[----, ----, ----, r(4), ----, ----]
row=5;[----, ----, ----, ----, r(5), ----]
row=6;[----, ----, ----, ----, ----, r(6)]

Yes
?- swf_xy_0( K1,(X,Y),(R1,R2)),
     same_binary_pattern((X,Y),R1,Q1),
     same_binary_pattern((X,Y),R2,Q2),
     \+ clause(swf_xy_0( K1,(X,Y),(Q1,Q2)),_).

No
?- gen_swf(K).
step(1):54:items are undifined yet.

K = 2 

Yes
?- 

*/

% NOTE: The Paretian profiles are stable 
% with respect to the IIA condition. 
% ( Of course, in order to propagate dicisiveness, 
% the transitivity, with the other properties of preference 
% orderings, is needed.)



% verifying the completeness for generated SWF
%-------------------------------------------------

undifined_swf_tuple((X,Y),(A,B)):-
   possible_preference_of_group( [1,2], [r(A),r(B)],_),
   distinct_pair_of_alternatives(X,Y),
   \+ (
      swf_xy_0(K,(X,Y),(A,B));
      swf_xy_0(K,(Y,X),(A,B))
   ).

is_complete_swf_at_profile( (R1,R2)):-
   possible_preference_of_group( [1,2], [r(R1),r(R2)],_),
   forall(
     distinct_pair_of_alternatives(X,Y),
     (
      swf_xy_0(K,(X,Y),(R1,R2));
      swf_xy_0(K,(Y,X),(R1,R2))
     )
   ).

is_almost_complete_swf_except_for_pair( (X,Y),(R1,R2)):-
   swf_undefined_pairs_at_profile( [(X,Y)],(R1,R2)).

swf_undefined_pairs_at_profile( P,(R1,R2)):-
   possible_preference_of_group( [1,2], [r(R1),r(R2)],_),
   findall((X,Y),
    (
     distinct_pair_of_alternatives(X,Y),
     X @< Y,
     \+ (
      swf_xy_0(K,(X,Y),(R1,R2));
      swf_xy_0(K,(Y,X),(R1,R2))
     )
    ),
   P).

/*

?- gen_swf(K).
step(1):54:items are undifined yet.

K = 1 

Yes
?- display_swf(bin).

row=1;[r(1), ----, ----, ----, ----, ----]
row=2;[----, r(2), ----, ----, ----, ----]
row=3;[----, ----, r(3), ----, ----, ----]
row=4;[----, ----, ----, r(4), ----, ----]
row=5;[----, ----, ----, ----, r(5), ----]
row=6;[----, ----, ----, ----, ----, r(6)]

Yes
?- display_swf(A,bin).

row=1;[a, a, -, -, a, -]
row=2;[a, a, -, -, a, -]
row=3;[-, -, b, b, -, b]
row=4;[-, -, b, b, -, b]
row=5;[a, a, -, -, a, -]
row=6;[-, -, b, b, -, b]

A = a, b ;

row=1;[a, a, a, -, -, -]
row=2;[a, a, a, -, -, -]
row=3;[a, a, a, -, -, -]
row=4;[-, -, -, c, c, c]
row=5;[-, -, -, c, c, c]
row=6;[-, -, -, c, c, c]

A = a, c ;

row=1;[b, -, b, b, -, -]
row=2;[-, c, -, -, c, c]
row=3;[b, -, b, b, -, -]
row=4;[b, -, b, b, -, -]
row=5;[-, c, -, -, c, c]
row=6;[-, c, -, -, c, c]

A = b, c ;

No
?- is_complete_swf_at_profile(A).

A = 1, 1 ;

A = 2, 2 ;

A = 3, 3 ;

A = 4, 4 ;

A = 5, 5 ;

A = 6, 6 ;

No
?- swf_undefined_pairs_at_profile( P,O).

P = []
O = 1, 1 ;

P = [ (b, c)]
O = 2, 1 ;

P = [ (a, b)]
O = 3, 1 ;

P = [ (a, b), (a, c)]
O = 4, 1 

Yes
?- is_almost_complete_swf_except_for_pair( X,Y),nl,write(X-Y),fail.

(b, c)- (2, 1)
(a, b)- (3, 1)
(b, c)- (1, 2)
(a, c)- (5, 2)
(a, b)- (1, 3)
(a, c)- (4, 3)
(a, c)- (3, 4)
(b, c)- (6, 4)
(a, c)- (2, 5)
(a, b)- (6, 5)
(b, c)- (4, 6)
(a, b)- (5, 6)

No
?- 

% to be continued.

*/


% testing consistency for generated swf: Are
% swf_0s not violated against transitivity?
%-------------------------------------------------

is_consistent_swf_for_all_profile:-
   forall(
     possible_preference_of_group( [1,2], [r(J),r(K)], _),
     is_consistent_swf_at_profile((J,K)->_)
   ).

is_consistent_swf_at_profile((J,K)->L):-
   possible_preference_of_group( [1,2], [r(J),r(K)], _),
   possible_preference_ordering( r(L), _),
   forall(
     distinct_pair_of_alternatives(X,Y),
     is_consistent_swf_on_pair((X,Y),(J,K)->L)
   ).

is_consistent_swf_on_pair((X,Y),(J,K)->L):-
   possible_preference_of_group( [1,2], [r(J),r(K)], _),
   distinct_pair_of_alternatives(X,Y),
   possible_preference_ordering( r(L), _),
   forall(
     swf_xy_0( _, (X,Y), (J,K)),
     strictly_prefer_to(X,Y, r(L))
   ).
%   forall(
%     strictly_prefer_to(X,Y, r(L)),
%     swf_xy_0( _, (X,Y), (J,K))
%   ).  

%  % completeness is not needed here.


% delegate/drop decisiveness
%-------------------------------------------------

delegate( J,X,A):-
%   clause( swf_xy_0( current_step, K),_),
%   (K=4->trace;true),
   is_almost_complete_swf_except_for_pair( X,A),
   is_xy_decisive_at_profile( J, X,A),
%   (K=4->read(y);true),
   \+ it_has_been_known_as_nogood( J,X,A),
   add_xy_decisiveness(J,X,A),
   record_delegation(J,X,A),
   warn_user_delegation(J,X,A),
   rollback_delegation_if_intransitive,
%   display_swf(bin),
   !.



% feudalizing or depriving local decisiveness 
% to the agent at an almost-defined profile
%-------------------------------------------------

is_xy_decisive_at_profile( 1, (X,Y), (R,Q)):-
   strictly_prefer_to(X,Y, r(R)),
   \+ strictly_prefer_to(X,Y, r(Q)),
   is_consistent_swf_at_profile((R,Q)->R).

is_xy_decisive_at_profile( 2, (X,Y), (R,Q)):-
   strictly_prefer_to(X,Y, r(Q)),
   \+ strictly_prefer_to(X,Y, r(R)),
   is_consistent_swf_at_profile((R,Q)->Q).

add_xy_decisiveness(J,(X,Y),(A,B)):-
   clause( swf_xy_0( current_step, K), _),
   undifined_swf_tuple((X,Y),(A,B)),
   is_xy_decisive_at_profile( J, (X,Y), (A,B)),
   assert( swf_xy_0( K, (X,Y), (A,B))).

record_delegation(J,X,A):-
   clause( swf_xy_0( current_step, K),_),
   assert( swf_xy_0( delegate(K), (J,X,A))).

warn_user_delegation(J,X,A):-
   nl,
   write( ' put decisiveness on ':X),
   write( ' at ':A),
   write( ' to ':J).

deprive_current_decisiveness(K,(J,X,A)):-
   clause( swf_xy_0( current_step, K),_),
   retract( swf_xy_0( delegate(K), (J,X,A))),
   retract( swf_xy_0( K, X,A)),
   assert( swf_xy_0( nogood, (K,J,X,A))).  % `nogood' memorized

it_has_been_known_as_nogood( J,X,A):-
   clause( swf_xy_0( current_step, K),_),
   clause( swf_xy_0( nogood, (K,J,X,A)),_).

warn_user_deprivation(J,X,A):-
   nl,
   write( ' deprived decisiveness on ':X),
   write( ' at ':A),
   write( ' from ':J).


% role-back operations
%-------------------------------------------------

rollback_delegation_if_intransitive:-
   iia_propagated_patterns_of_binary_swf(L),
   check_transitivity_in_swf_patterns(L,_,user),
   !.

rollback_delegation_if_intransitive:-
   rollback_delegation,
   fail.

rollback_delegation:-
   rollback_delegation(_,_,_,_).

rollback_delegation(K,J,X,A):-
   deprive_current_decisiveness(K,(J,X,A)),
   warn_user_deprivation(J,X,A).

rollback_swf_step(K->K1):-
   clause( swf_xy_0( K, _, _),true),
   forall( retract( swf_xy_0( K, _, _)),true),
   retract( swf_xy_0( current_step,K)),
   K1 is K -1,
   assert( swf_xy_0( current_step,K1)),
   nl,
   write(rollback(K->K1)).



%-------------------------------------------------
%  Script for Iteratively Generating Swf 
%-------------------------------------------------


gen_complete_swf:-
   gen_swf(1),
   display_swf(bin),
   delegate( _,_X,_A),
   gen_swf(_K),
   display_swf(bin),
   fail.

gen_complete_swf:-
   undifined_swf_tuple(_,_),
   gen_swf(_K),
   display_swf(bin),
   fail.

gen_complete_swf:-
   \+ undifined_swf_tuple(_,_),
   nl,
   write(' complete'),
   !.

gen_complete_swf:-
   nl,
   write(' I could not complete it.').






% demo
%-------------------------------------------------


/*

?- [swf_d].

----------------------------------------
Arrovian possibility theorem by prolog 
(swf_d.pl, 5-7,21,25 Feb, 2-6 Mar 2006)
----------------------------------------
% swf_d compiled 0.03 sec, -164 bytes

Yes
?- gen_swf(1),display_swf(bin).

step(1):54:items are undifined yet.
row=1;[r(1), ----, ----, ----, ----, ----]
row=2;[----, r(2), ----, ----, ----, ----]
row=3;[----, ----, r(3), ----, ----, ----]
row=4;[----, ----, ----, r(4), ----, ----]
row=5;[----, ----, ----, ----, r(5), ----]
row=6;[----, ----, ----, ----, ----, r(6)]

Yes
?- delegate(J,X,A),display_swf(bin).

 put decisiveness on : (b, c) at : (2, 1) to :2
row=1;[r(1), ----, ----, ----, ----, ----]
row=2;[r(1), r(2), ----, ----, ----, ----]
row=3;[----, ----, r(3), ----, ----, ----]
row=4;[----, ----, ----, r(4), ----, ----]
row=5;[----, ----, ----, ----, r(5), ----]
row=6;[----, ----, ----, ----, ----, r(6)]

J = 2
X = b, c
A = 2, 1 

Yes
?- gen_swf(K),display_swf(bin).

step(2):45:items are undifined yet.
row=1;[r(1), ----, ----, ----, ----, ----]
row=2;[r(1), r(2), ----, ----, ----, ----]
row=3;[----, ----, r(3), ----, ----, ----]
row=4;[----, ----, ----, r(4), ----, ----]
row=5;[----, ----, ----, ----, r(5), ----]
row=6;[----, ----, ----, r(4), ----, r(6)]

K = 2 

Yes
?- gen_swf(K),display_swf(bin).

step(3):27:items are undifined yet.
row=1;[r(1), ----, r(3), ----, ----, ----]
row=2;[r(1), r(2), r(3), ----, ----, ----]
row=3;[----, ----, r(3), ----, ----, ----]
row=4;[----, ----, r(3), r(4), ----, ----]
row=5;[r(1), r(2), r(3), r(4), r(5), r(6)]
row=6;[----, ----, r(3), r(4), ----, r(6)]

K = 3 

Yes
?- gen_swf(K),display_swf(bin).

step(4):9:items are undifined yet.
row=1;[r(1), ----, r(3), r(4), ----, ----]
row=2;[r(1), r(2), r(3), r(4), r(5), r(6)]
row=3;[r(1), ----, r(3), r(4), ----, ----]
row=4;[r(1), ----, r(3), r(4), ----, ----]
row=5;[r(1), r(2), r(3), r(4), r(5), r(6)]
row=6;[r(1), r(2), r(3), r(4), r(5), r(6)]

K = 4 

Yes
?- gen_swf(K),display_swf(bin).

step(5):0:items are undifined yet.
row=1;[r(1), r(2), r(3), r(4), r(5), r(6)]
row=2;[r(1), r(2), r(3), r(4), r(5), r(6)]
row=3;[r(1), r(2), r(3), r(4), r(5), r(6)]
row=4;[r(1), r(2), r(3), r(4), r(5), r(6)]
row=5;[r(1), r(2), r(3), r(4), r(5), r(6)]
row=6;[r(1), r(2), r(3), r(4), r(5), r(6)]

K = 5 

Yes
?- 

?- gen_swf(1),display_swf(XY,bin).

step(1):54:items are undifined yet.
row=1;[a, a, -, -, a, -]
row=2;[a, a, -, -, a, -]
row=3;[-, -, b, b, -, b]
row=4;[-, -, b, b, -, b]
row=5;[a, a, -, -, a, -]
row=6;[-, -, b, b, -, b]

XY = a, b ;

row=1;[a, a, a, -, -, -]
row=2;[a, a, a, -, -, -]
row=3;[a, a, a, -, -, -]
row=4;[-, -, -, c, c, c]
row=5;[-, -, -, c, c, c]
row=6;[-, -, -, c, c, c]

XY = a, c ;

row=1;[b, -, b, b, -, -]
row=2;[-, c, -, -, c, c]
row=3;[b, -, b, b, -, -]
row=4;[b, -, b, b, -, -]
row=5;[-, c, -, -, c, c]
row=6;[-, c, -, -, c, c]

XY = b, c 

Yes
?- delegate(J,X,A),display_swf(XY,bin).

 put decisiveness on : (b, c) at : (2, 1) to :2
row=1;[a, a, -, -, a, -]
row=2;[a, a, -, -, a, -]
row=3;[-, -, b, b, -, b]
row=4;[-, -, b, b, -, b]
row=5;[a, a, -, -, a, -]
row=6;[-, -, b, b, -, b]

J = 2
X = b, c
A = 2, 1
XY = a, b ;

row=1;[a, a, a, -, -, -]
row=2;[a, a, a, -, -, -]
row=3;[a, a, a, -, -, -]
row=4;[-, -, -, c, c, c]
row=5;[-, -, -, c, c, c]
row=6;[-, -, -, c, c, c]

J = 2
X = b, c
A = 2, 1
XY = a, c ;

row=1;[b, -, b, b, -, -]
row=2;[b, c, -, -, c, c]
row=3;[b, -, b, b, -, -]
row=4;[b, -, b, b, -, -]
row=5;[-, c, -, -, c, c]
row=6;[-, c, -, -, c, c]

J = 2
X = b, c
A = 2, 1
XY = b, c 

Yes
?- gen_swf(K),display_swf(XY,bin).

step(2):45:items are undifined yet.
row=1;[a, a, -, -, a, -]
row=2;[a, a, -, -, a, -]
row=3;[-, -, b, b, -, b]
row=4;[-, -, b, b, -, b]
row=5;[a, a, -, -, a, -]
row=6;[-, -, b, b, -, b]

K = 2
XY = a, b ;

row=1;[a, a, a, -, -, -]
row=2;[a, a, a, -, -, -]
row=3;[a, a, a, -, -, -]
row=4;[-, -, -, c, c, c]
row=5;[-, -, -, c, c, c]
row=6;[-, -, -, c, c, c]

K = 2
XY = a, c ;

row=1;[b, -, b, b, -, -]
row=2;[b, c, b, b, c, c]
row=3;[b, -, b, b, -, -]
row=4;[b, -, b, b, -, -]
row=5;[b, c, b, b, c, c]
row=6;[b, c, b, b, c, c]

K = 2
XY = b, c ;

No
?- gen_swf(K),display_swf(XY,bin).

step(3):27:items are undifined yet.
row=1;[a, a, b, b, a, b]
row=2;[a, a, b, b, a, b]
row=3;[-, -, b, b, -, b]
row=4;[-, -, b, b, -, b]
row=5;[a, a, b, b, a, b]
row=6;[-, -, b, b, -, b]

K = 3
XY = a, b ;

row=1;[a, a, a, -, -, -]
row=2;[a, a, a, -, -, -]
row=3;[a, a, a, -, -, -]
row=4;[a, a, a, c, c, c]
row=5;[a, a, a, c, c, c]
row=6;[a, a, a, c, c, c]

K = 3
XY = a, c ;

row=1;[b, -, b, b, -, -]
row=2;[b, c, b, b, c, c]
row=3;[b, -, b, b, -, -]
row=4;[b, -, b, b, -, -]
row=5;[b, c, b, b, c, c]
row=6;[b, c, b, b, c, c]

K = 3
XY = b, c ;

No
?- gen_swf(K),display_swf(XY,bin).

step(4):9:items are undifined yet.
row=1;[a, a, b, b, a, b]
row=2;[a, a, b, b, a, b]
row=3;[a, a, b, b, a, b]
row=4;[a, a, b, b, a, b]
row=5;[a, a, b, b, a, b]
row=6;[a, a, b, b, a, b]

K = 4
XY = a, b ;

row=1;[a, a, a, c, c, c]
row=2;[a, a, a, c, c, c]
row=3;[a, a, a, c, c, c]
row=4;[a, a, a, c, c, c]
row=5;[a, a, a, c, c, c]
row=6;[a, a, a, c, c, c]

K = 4
XY = a, c ;

row=1;[b, -, b, b, -, -]
row=2;[b, c, b, b, c, c]
row=3;[b, -, b, b, -, -]
row=4;[b, -, b, b, -, -]
row=5;[b, c, b, b, c, c]
row=6;[b, c, b, b, c, c]

K = 4
XY = b, c ;

No
?- gen_swf(K),display_swf(XY,bin).

step(5):0:items are undifined yet.
row=1;[a, a, b, b, a, b]
row=2;[a, a, b, b, a, b]
row=3;[a, a, b, b, a, b]
row=4;[a, a, b, b, a, b]
row=5;[a, a, b, b, a, b]
row=6;[a, a, b, b, a, b]

K = 5
XY = a, b ;

row=1;[a, a, a, c, c, c]
row=2;[a, a, a, c, c, c]
row=3;[a, a, a, c, c, c]
row=4;[a, a, a, c, c, c]
row=5;[a, a, a, c, c, c]
row=6;[a, a, a, c, c, c]

K = 5
XY = a, c ;

row=1;[b, c, b, b, c, c]
row=2;[b, c, b, b, c, c]
row=3;[b, c, b, b, c, c]
row=4;[b, c, b, b, c, c]
row=5;[b, c, b, b, c, c]
row=6;[b, c, b, b, c, c]

K = 5
XY = b, c ;

No
?- 
*/


%-------------------------------------------------
%  modeling Arrovian SWF : list-based preferences
%-------------------------------------------------

% The modeling below had completed until 25 Feb 2006.

% pattern of preferences on binary comparisons
%-------------------------------------------------

bit_profile_of_preference_on_pair(_, [],[]).
bit_profile_of_preference_on_pair((X,Y), [Rj|R],[Bj|B]):-
   bit_profile_of_preference_on_pair((X,Y),R,B),
   (strictly_prefer_to(X,Y,Rj)->Bj=1;Bj=0).



% group/social choice set
%-------------------------------------------------
% It would be used for satisfies_Pareto_principle_2/2 below.

social_preference_profile(N, Rn, On):-
   set_of_agents(N), 
   possible_preference_of_group( N, Rn, On).

socially_choosing_maximals(R,Rn,C,Cn):-
   social_preference_profile(N, Rn,_),
   group_choice_set(N, Rn,Cn),
   possible_preference_ordering(R,_),
   group_choice_set(_,[R],C),
   subset(C,Cn).

group_choice_set(G,Rn,Cn):-
   % group(G) both in full or not.
   (\+ var(Rn) ->true
     ;possible_preference_of_group( G, Rn, _)
   ),
   findall( X,
    (
     member( Ra, Rn),
     maximal_element( X, Ra)
    ),
   Cn0),
   sort(Cn0,Cn).

/*

?- is_socially_choosing_maximals(R,Rn,C,Cn),Cn=[a],
nl,write(R;Rn;C;Cn),fail.

r(1);[r(1), r(1)];[a];[a]
r(2);[r(1), r(1)];[a];[a]
r(1);[r(2), r(1)];[a];[a]
r(2);[r(2), r(1)];[a];[a]
r(1);[r(1), r(2)];[a];[a]
r(2);[r(1), r(2)];[a];[a]
r(1);[r(2), r(2)];[a];[a]
r(2);[r(2), r(2)];[a];[a]

No
?- 

*/


% unanimity within a group
%-------------------------------------------------

solid_support_by_group( G, (X > Y), Rz):-
   support_members_in_group( G, G, (X > Y), Rz).

support_members_in_group( G, S, (X > Y), Rz):-
   group(G),
   alternative(X),
   alternative(Y),
   findall( J,
    (
     member(J,G),
     member((J,R),Rz),
     strictly_prefer_to(X,Y, R)
    ),
   S).

distinct_pair_of_alternatives(X,Y):-
   alternative(X),
   alternative(Y),
   X \= Y.


%  decisiveness for pair of alternatives
%-------------------------------------------------

is_decisive( urd(2,3), G, (X > Y), swf(K)):-
   social_welfare_function( urd(2,3), swf(K)),
   group(G),
   distinct_pair_of_alternatives(X,Y),
   forall(
    ( 
     social_welfare_function( urd(2,3), swf(K), [R1,R2]->R),
     solid_support_by_group( G, (X > Y), [(1,R1),(2,R2)])
    ),
    (
     strictly_prefer_to(X,Y, R)
    )
   ).

is_decisive( urd(2,3), G, (X, Y), swf(K)):-
   is_decisive( urd(2,3), G, (X > Y), swf(K)),
   is_decisive( urd(2,3), G, (Y > X), swf(K)).

/*

?- is_decisive( urd(2,3), [1,2], X, swf(1)),
X=(_,_),tab(2),write([X]),fail.
  [ (a, b)]  [ (a, c)]  [ (b, a)]  [ (b, c)]  [ (c, a)]  [ (c, b)]

No
?- is_decisive( urd(2,3), [1], X, swf(1)),
X=(_>_),tab(2),write([X]),fail.
  [a>b]  [a>c]  [b>a]  [b>c]  [c>a]  [c>b]

No
?- is_decisive( urd(2,3), [1], X, swf(1)),
X=(_,_),tab(2),write([X]),fail.
  [ (a, b)]  [ (a, c)]  [ (b, a)]  [ (b, c)]  [ (c, a)]  [ (c, b)]

No
?- is_decisive( urd(2,3), [2], X, swf(1)).

No
?-

*/

%  decisiveness of group
%-------------------------------------------------

is_decisive( urd(2,3), G, swf(K)):-
   group(G),
   social_welfare_function( urd(2,3), swf(K)),
   forall(
    (
     distinct_pair_of_alternatives(X,Y)
    ),
    (
     is_decisive( urd(2,3),G, (X, Y), swf(K))
    )
   ).

/*

?- is_decisive( urd(2,3), G, Swf).

G = [1]
Swf = swf(1) ;

G = [2]
Swf = swf(2) ;

G = [1, 2]
Swf = swf(1) ;

G = [1, 2]
Swf = swf(2) ;

No
?-

*/


%  dictatorship as decisiveness of singlton
%-------------------------------------------------

dictator_for_swf(Domain, Swf, J):-
   is_decisive( Domain, [J], Swf). 


%  the Pareto principle as decisiveness of everyone
%-------------------------------------------------

satisfies_Pareto_principle( Domain, Swf):-
   set_of_agents(N),
   is_decisive( Domain, N, Swf). 


/*

?- dictator_for_swf(Domain, swf(K), J).

Domain = urd(2, 3)
K = 1
J = 1 ;

Domain = urd(2, 3)
K = 2
J = 2 ;

No
?- satisfies_Pareto_principle( Domain, swf(K)).

Domain = urd(2, 3)
K = 1 ;

Domain = urd(2, 3)
K = 2 ;

No
?-

*/

%  another definition for the Pareto principle :
%  restriction to the socially maximal set
%-------------------------------------------------

satisfies_Pareto_principle_2( Domain, Swf):-
   social_welfare_function( Domain, Swf),
   forall(
    (
     possible_preference_pair( urd(2,3), (R1, R2),_)
    ),
    (
     social_welfare_function( Domain, Swf, [R1,R2]->R),
     is_subset_of_maximals( [R1,R2]->R)
    )
   ).


is_subset_of_maximals( Rn->R):-
   socially_choosing_maximals(R,Rn,_,_).


/*

?- satisfies_Pareto_principle( Domain, swf(K)),
\+ satisfies_Pareto_principle_2( Domain, swf(K)).

No
?- satisfies_Pareto_principle_2( Domain, swf(K)),
\+ satisfies_Pareto_principle( Domain, swf(K)).

No
?-

*/



% independent from irrelevant alternatives (IIA)
%-------------------------------------------------

iia_condition_of_swf(Swf,(X,Y)):-
   social_welfare_function( urd(2,3), Swf),
   distinct_pair_of_alternatives(X,Y),
   findall(B,
    (
     social_welfare_function( urd(2,3), Swf,R->F),
     bit_profile_of_preference_on_pair( (X,Y),[F|R],B)
    ),
   Lb),
   \+ \+ setof(Bf, member( [Bf|_],Lb),[_]).


iia_condition_of_swf(Swf):-
   social_welfare_function( urd(2,3), Swf),
   forall(
    (
     distinct_pair_of_alternatives(X,Y)
    ),
    (
     iia_condition_of_swf(Swf,(X,Y))
    )
   ).


/*

?- iia_condition_of_swf(Swf).

Swf = swf(1) ;

Swf = swf(2) ;

No
?- iia_condition_of_swf(swf(3),(X,Y)).

No
?- 

*/



%  automated designing SWFs recursively for the 2x3 
%  unrestricted domain with the IIA condition 
%-------------------------------------------------

:- dynamic auto_swf_0/4.
:- dynamic pivotal_0/4.

all_preference_pairs_in_urd23( Poss):-
   findall([R1,R2],
     possible_preference_pair( urd(2,3), (R1, R2),_),
   Poss).

auto_swf( urd(2,3), FL,Property):-
   abolish(auto_swf_0/4),
   abolish(pivotal_0/4),
   all_preference_pairs_in_urd23( L),
   auto_swf( urd(2,3), FL, L, Property).

auto_swf( _, [],[], _).

auto_swf( Domain, [R->F | H], [R|Q], free):-
   auto_swf( Domain, H,Q,free),
   possible_preference_ordering(F, _).

auto_swf( Domain, [R->F | H], [R|Q], pareto):-
   auto_swf( Domain, H,Q,pareto),
   possible_preference_ordering(F, _),
   is_subset_of_maximals( R->F).

auto_swf( Domain, [R->F | H], [R|Q], iia(1)):-
   auto_swf( Domain, H,Q,iia(1)),
   possible_preference_ordering(F, _),
   \+ violates_iia( R->F, H, _).

auto_swf( Domain, H, [R], iia(2)):-
   auto_swf( Domain, H,[R],pareto).

auto_swf( Domain, [R->F | H], [R|Q], iia(2)):-
   auto_swf( Domain, H,Q,iia(2)),
   Q\=[],
   possible_preference_ordering(F, _),
   \+ violates_iia( R->F, H, _).

auto_swf( Domain, H, [R], iia(3)):-
   auto_swf( Domain, H,[R],pareto).

auto_swf( Domain, [R->F | H], [R|Q], iia(3)):-
   auto_swf( Domain, H,Q,iia(3)),
   Q\=[],
   possible_preference_ordering(F, _),
   is_subset_of_maximals( R->F),
   \+ violates_iia( R->F, H, _).

auto_swf( Domain, [R->F], [R], iia(4)):-
   auto_swf( Domain, [R->F],[R],pareto),
   record_pivotal_agents( R->F,[],[],iia(4)),
   assert( auto_swf_0(Domain,[R->F],[R],iia(4))).

auto_swf( Domain, [R->F | H], [R|Q], iia(4)):-
   auto_swf( Domain, H,Q,iia(4)),
   Q\=[],
   possible_preference_ordering(F, _),
   \+ violates_iia( R->F, H, _),
   %is_subset_of_maximals( R->F),
   is_weak_Paretian( R->F ),
   record_pivotal_agents( R->F,H,Q,iia(4)),
   assert( auto_swf_0(Domain,[R->F|H],[R|Q],iia(4))).

record_pivotal_agents( R->F,H,Q,iia(4)):-
   forall(
     is_positively_xy_pivotal( J, (X,Y),R->F,H),
     assert(
       pivotal_0((J,X,Y),[R->F|H],[R|Q],iia(4))
     )
   ).

is_positively_xy_pivotal( 1, (X,Y),[R1,R2]->R,H):-
   is_xy_pivotal( 1, (X,Y),[R1,R2]->R,H),
   forall(
    (
     strictly_prefer_to(X,Y, Q1),
     member( [Q1,R2]->Q, H)
    ),
     strictly_prefer_to(X,Y, Q)
   ).

is_positively_xy_pivotal( 2, (X,Y),[R1,R2]->R,H):-
   is_xy_pivotal( 2, (X,Y),[R1,R2]->R,H),
   forall(
    (
     strictly_prefer_to(X,Y, Q2),
     member( [R1,Q2]->Q, H)
    ),
     strictly_prefer_to(X,Y, Q)
   ).

is_xy_pivotal( 1, (X,Y),[_R1,R2]->R,H):-
%  distinct_pair_of_alternatives(X,Y),
   strictly_prefer_to(X,Y, R),
   member( [_Q1,R2]->Q, H),
   strictly_prefer_to(Y,X, Q),
   !.

is_xy_pivotal( _, (X,Y),_->R,[]):-
   distinct_pair_of_alternatives(X,Y),
   \+ strictly_prefer_to(X,Y, R),
   !.

is_xy_pivotal( 1, (X,Y),[R1,R2]->R,H):-
   distinct_pair_of_alternatives(X,Y),
   \+ strictly_prefer_to(X,Y, R),
   member( [_Q1,R2]->Q, [[R1,R2]->R|H]),
   \+ strictly_prefer_to(Y,X, Q),
   !.

is_xy_pivotal( 2, (X,Y),[R1,_R2]->R,H):-
%  distinct_pair_of_alternatives(X,Y),
   strictly_prefer_to(X,Y, R),
   member( [R1,_Q2]->Q, H),
   strictly_prefer_to(Y,X, Q),
   !.

is_xy_pivotal( 2, (X,Y),[R1,R2]->R,H):-
   distinct_pair_of_alternatives(X,Y),
   \+ strictly_prefer_to(X,Y, R),
   member( [R1,_Q2]->Q, [[R1,R2]->R|H]),
   \+ strictly_prefer_to(Y,X, Q),
   !.


is_weak_Paretian( [R1,R2]->R):-
   set_of_agents(N),
   forall(
    (
     distinct_pair_of_alternatives(X,Y),
     solid_support_by_group( N, (X > Y), [(1,R1),(2,R2)])
    ),
     strictly_prefer_to(X,Y, R)
   ).

violates_iia( R->F, H, [(X,Y), B, B1]):-
   distinct_pair_of_alternatives(X,Y),
   bit_profile_of_preference_on_pair( (X,Y),[F|R],[B|Br]),
   member( R1->F1, H),
   bit_profile_of_preference_on_pair( (X,Y),[F1|R1],[B1|Br]),
   B  \= B1.



/*

?- auto_swf( Domain, H, free),
display_auto_swf(H).

row=1;[r(1), r(1), r(1), r(1), r(1), r(1)]
row=2;[r(1), r(1), r(1), r(1), r(1), r(1)]
row=3;[r(1), r(1), r(1), r(1), r(1), r(1)]
row=4;[r(1), r(1), r(1), r(1), r(1), r(1)]
row=5;[r(1), r(1), r(1), r(1), r(1), r(1)]
row=6;[r(1), r(1), r(1), r(1), r(1), r(1)]

Domain = urd(2, 3)
H = [ ([r(1), r(1)]->r(1)), ([r(2), r(1)]->r(1)), ([r(3), r(1)]->r(1)), ([r(4), r(1)]->r(1)), ([r(5), r(1)]->r(1)), ([r(6), r(...)]->r(1)), ([r(...)|...]->r(1)), ([...|...]->r(...)), (... ->...)|...] 

Yes
?- auto_swf( Domain, H, pareto),
display_auto_swf(H).

row=1;[r(1), r(1), r(1), r(1), r(1), r(1)]
row=2;[r(1), r(1), r(1), r(1), r(1), r(1)]
row=3;[r(1), r(1), r(3), r(3), r(3), r(3)]
row=4;[r(1), r(1), r(3), r(3), r(3), r(3)]
row=5;[r(1), r(1), r(3), r(3), r(5), r(5)]
row=6;[r(1), r(1), r(3), r(3), r(5), r(5)]

Domain = urd(2, 3)
H = [ ([r(1), r(1)]->r(1)), ([r(2), r(1)]->r(1)), ([r(3), r(1)]->r(1)), ([r(4), r(1)]->r(1)), ([r(5), r(1)]->r(1)), ([r(6), r(...)]->r(1)), ([r(...)|...]->r(1)), ([...|...]->r(...)), (... ->...)|...] 

Yes
?- auto_swf( Domain, H, iia(1)),
display_auto_swf(H).

row=1;[r(1), r(1), r(1), r(1), r(1), r(1)]
row=2;[r(1), r(1), r(1), r(1), r(1), r(1)]
row=3;[r(1), r(1), r(1), r(1), r(1), r(1)]
row=4;[r(1), r(1), r(1), r(1), r(1), r(1)]
row=5;[r(1), r(1), r(1), r(1), r(1), r(1)]
row=6;[r(1), r(1), r(1), r(1), r(1), r(1)]

Domain = urd(2, 3)
H = [ ([r(1), r(1)]->r(1)), ([r(2), r(1)]->r(1)), ([r(3), r(1)]->r(1)), ([r(4), r(1)]->r(1)), ([r(5), r(1)]->r(1)), ([r(6), r(...)]->r(1)), ([r(...)|...]->r(1)), ([...|...]->r(...)), (... ->...)|...] 

Yes
?- auto_swf( Domain, H, iia(3)),
display_auto_swf(H).

row=1;[r(1), r(1), r(1), r(1), r(1), r(1)]
row=2;[r(2), r(2), r(2), r(2), r(2), r(2)]
row=3;[r(3), r(3), r(3), r(3), r(3), r(3)]
row=4;[r(4), r(4), r(4), r(4), r(4), r(4)]
row=5;[r(5), r(5), r(5), r(5), r(5), r(5)]
row=6;[r(6), r(6), r(6), r(6), r(6), r(6)]

Domain = urd(2, 3)
H = [ ([r(1), r(1)]->r(1)), ([r(2), r(1)]->r(2)), ([r(3), r(1)]->r(3)), ([r(4), r(1)]->r(4)), ([r(5), r(1)]->r(5)), ([r(6), r(...)]->r(6)), ([r(...)|...]->r(1)), ([...|...]->r(...)), (... ->...)|...] ;

row=1;[r(1), r(2), r(3), r(4), r(5), r(6)]
row=2;[r(1), r(2), r(3), r(4), r(5), r(6)]
row=3;[r(1), r(2), r(3), r(4), r(5), r(6)]
row=4;[r(1), r(2), r(3), r(4), r(5), r(6)]
row=5;[r(1), r(2), r(3), r(4), r(5), r(6)]
row=6;[r(1), r(2), r(3), r(4), r(5), r(6)]

Domain = urd(2, 3)
H = [ ([r(1), r(1)]->r(1)), ([r(2), r(1)]->r(1)), ([r(3), r(1)]->r(1)), ([r(4), r(1)]->r(1)), ([r(5), r(1)]->r(1)), ([r(6), r(...)]->r(1)), ([r(...)|...]->r(2)), ([...|...]->r(...)), (... ->...)|...] ;

No
?- 

*/


%  displaying generated swfs
%-------------------------------------------------


display_auto_swf_n(F):-
   forall(
     setof((K,C),member([r(J),r(K)]->C,F),L),
     (nl,write(row=J;L))
   ).

display_auto_swf(F):-
   \+ var(F),
   length(F,_),
   forall(
     bagof(C,K^member([r(J),r(K)]->C,F),L),
     (nl,write(row=J;L))
   ).




%  saving swf_0s and pivotal_0s into csv file
%-------------------------------------------------

save_swf:- tell_goal( 'swf_c.csv',(
   auto_swf_0( urd(2,3), [R->F|H], [R|_],iia(4)),
   R=[r(K),r(J)],F=r(W),length(H,N),nl,write((N,K,J,W)),fail
)).

save_pivotal:- tell_goal( 'swf_c_pivot.csv', (
   pivotal_0( (J,X,Y), [R->F|H],_, iia(4)),
   (is_a_part_of_complete_swf( [R->F|H],_, iia(4))->S=1;S=0),
   R=[r(K),r(L)],F=r(W),length(H,N),
   nl,write((N,K,L,W,J,X,Y,S)),fail
)).

is_a_part_of_complete_swf([R->F|H],SWF, iia(4)):-
   length(SWF,36),
   auto_swf_0( urd(2,3), SWF, _,iia(4)),
   append( _, [R->F|H],SWF),
   !.

/*

?- [menu].
% menu compiled 0.02 sec, 18,120 bytes

Yes
?- auto_swf( Domain, H, iia(4)),
display_auto_swf(H).

...
?- save_swf.

Yes
?- findall(1,auto_swf( Domain, H,[R],pareto),L),length(L,N).

Domain = _G163
H = _G164
R = _G160
L = [1, 1, 1, 1, 1, 1, 1, 1, 1|...]
N = 120 

Yes
?- findall((K,J,W),(H=[[r(K),r(J)]->r(W)|_],
auto_swf( Domain, H,[R],pareto)),L),nth1(Q,L,(6,6,6)).

K = _G163
J = _G160
W = _G161
H = _G184
Domain = _G190
R = _G187
L = [ (1, 1, 1), (2, 1, 1), (3, 1, 1), (4, 1, 1), (5, 1, 1), (6, 1, 1), (1, 2, 1), (2, ..., ...), (..., ...)|...]
Q = 120 

Yes


*/

% end of the program