:-op(100,fy,not).
:-op(110,yfx,&).
:-op(120,yfx,v).
:-op(900,yfx,/=).

:- dynamic numatoms/1, theatom/2, option/2.

numatoms(0).
numrows(0).
option(avoid_neg_head,on).
option(verbose,off).



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Countermodels

    I /= (F,G)		:- !, I /= F & G.
    I /= (F;G)		:- !, I /= F v G.
    I /= (G :- F)	:- !, I /= (F -> G).
    I /= (not F)	:- !, I /= (F -> false).

   _I /= true		:- !.
   _I /= false		:- !,fail.
[H|_] /= A		:- number(A),!,holds(A,H).
    I /= F & G		:-  I /= F, I /= G.
    I /= F v G		:-  I /= F,!; I /= G.
  [T] /= (F -> G)	:-  [T] /= G,!; \+ ([T] /= F).
[H,T] /= (F -> G)	:-  [T] /= (F -> G), 
			    ([H,T] /= G,!; \+ ([H,T] /= F)).

countermodel(I,T) :- member(F,T), \+ (I /= F),!.

countermodels(G,Is):-
	all_true_interp(Z),
	findall(T,get_subset(Z,T),Ts),
	all_t_countermodels(Ts,G,[],Is).

all_t_countermodels([],_,Is,Is):-!.
all_t_countermodels([T|Ts],G,Is0,Is):-
	t_countermodels(T,G,Is1),
	append(Is0,Is1,Is2),
	all_t_countermodels(Ts,G,Is2,Is).

% Gets all countermodels [H,T] fixing T
t_countermodels(T,G,Is):-
	  countermodel([T],G),!,
	  findall([H,T],get_subset(T,H),Is)
	; findall([H,T],(get_subset(T,H),H \= T,countermodel([H,T],G)),Is).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Extracting the propositional signature

set_atoms(true,true):-!.
set_atoms(false,false):-!.
set_atoms([],[]):-!.
set_atoms(T,T2):-
	T =.. [F|Args],
	( member(F,[&,v,->,-,not,(,),(;),(:-),(.)]),!,
	  set_atoms_args(Args,Args2),T2 =.. [F|Args2]
	; theatom(I,T),!,T2=I
	; numatoms(N),retract(numatoms(_)),N1 is N+1,assertz(numatoms(N1)),
	  assertz(theatom(N,T)),T2=N	
	).

set_atoms_args([],[]):-!.
set_atoms_args([F|Fs],[G|Gs]):-
	set_atoms(F,G),set_atoms_args(Fs,Gs).	

set_signature(L):-
	(retractall(numatoms(_)),!;true),
	(retractall(theatom(_,_)),!;true),
	asserta(numatoms(0)),
	set_atoms(L,_).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

rebuild(T,P):-
	(retractall(numatoms(_)),!;true),
	(retractall(theatom(_,_)),!;true),
	asserta(numatoms(0)),
	set_atoms(T,T2),
	(option(verbose,on),!,write('Computing countermodels...'),nl; true),
	countermodels(T2,CMs),
	maplist(to_3valued,CMs,CMs2),
	minprogram(CMs2,P).

minimise_program(T,P):-
	(retractall(numatoms(_)),!;true),
	(retractall(theatom(_,_)),!;true),
	asserta(numatoms(0)),
	set_atoms(T,T2),
	(option(verbose,on),!,write('Computing countermodels...'),nl; true),
	get_program_cms(T2,CMs0),
	t_closure(CMs0,CMs),
	minprogram(CMs,P).

:- dynamic cm/3, numcms/1, implicate/5, implic/3, numimplicates/1, i/1.
:- dynamic chart/2.

% implicate(IdCode,NumOfOnes,Labelling,Weight,PrimeMark)

minprogram(CMs,Rs):-
	initialize(CMs),
	findall(r(N,X),implicate(X,N,_,_,_),As),
	sort(As,Bs),
	classify(Bs,S0),
        (option(verbose,on),!,write('Obtaining prime implicates...'),nl;true),
	prime_implicates(S0),
	(option(avoid_neg_head,on),!,remove_neg_heads; true),
	(option(verbose,on),!,write('Getting minimal coverings...'),nl;true),
	get_implicate_countermodels,
	build_chart,
	filter_essential(Es),
	findall(M,chart(M,_),Ms0),sort(Ms0,Ms), % get the uncovered countermodels
	( Ms=[],!,Ts=Es  % all countermodels were covered: Petrick's method unneeded
	
	; findall(Y,chart(_,Y),Ys0),sort(Ys0,Ys), % get the non-essential implicates
	  findall(Ns,(member(W,Ys),findall(N,chart(N,W),Ns)),NsList),
	  petrick(Ms,NsList,Vs),
	  member(V,Vs),	% pick one list among the obtained with Petrick's method
	  findall(Q,(member(J,V),nth0(J,Ys,Q)),Qs),
	  append(Es,Qs,Ts)
	),
	build_rules(Ts,Rs).

initialize(CMs):-
	(retractall(cm(_,_,_)),!; true),
	(retractall(numcms(_)),!; true),
	(retractall(implicate(_,_,_,_,_)),!; true),
	(retractall(numimplicates(_)),!; true),
	(retractall(implic(_,_,_)),!; true),
	(retractall(i(_)),!; true),
	(retractall(chart(_,_)),!; true),
	asserta(numcms(0)),
	asserta(i(0)),
	repeat, (
	  member(X,CMs),
	  numcms(N),
	  assertz(cm(N,X,[])),
	  count(1,X,Ones),
	  assertz(implicate(N,Ones,X,0,prime)),
	  retractall(numcms(_)),
	  N1 is N+1,
	  asserta(numcms(N1)),
	  fail
	; true
	),!,numcms(M),asserta(numimplicates(M)),
	compute_submodels.
	
compute_submodels:-
	repeat, (
	  cm(X,Rx,[]),compute_submodels(X,Rx),fail
	; true
	),!.
	
compute_submodels(X,Rx):-
	( is_total(Rx),!,findall(Y,(submodel(Rx,M),cm(Y,M,_)),Ys),
	  sort(Ys,Ws),Zs=Ws
	; Zs=[X]
	),
	retract(cm(X,Rx,_)),asserta(cm(X,Rx,Zs)).

classify([],[]):-!.
classify([r(N,X)],[r(N,[X])]):-!.
classify([r(N,X)|Rs],Es):-
	classify(Rs,Cs),Cs=[r(M,Ys)|Ds],
	(N=M,!,Es=[r(M,[X|Ys])|Ds]
	;Es=[r(N,[X]),r(M,Ys)|Ds]
	).

prime_implicates([]):-!.
prime_implicates(S):-
	i(I),I1 is I+1,
	(option(verbose,on),!,write(I),write(' ************'),nl,write_classes(S);true),
	match_consec_classes(S),
	match_intra_classes(S),
	findall(r(N,X),implicate(X,N,_,I1,_),As),
	sort(As,Bs),
	classify(Bs,S1),
	retractall(i(_)),asserta(i(I1)),
	% remove previous nonprime implicates
	I0 is I-1,
	(retractall(implicate(_,_,_,I0,nonprime)),!;true),
	prime_implicates(S1).

match_consec_classes([]):-!.
match_consec_classes([_]):-!.
match_consec_classes([r(N,Xs),r(M,Ys)|Cs]):-
	N1 is N+1, M=N1,!,
	match_pairs(a,N,Xs,Ys),
	match_consec_classes([r(M,Ys)|Cs]).
match_consec_classes([_,r(M,Ys)|Cs]):-match_consec_classes([r(M,Ys)|Cs]).

match_pairs(Type,N,Xs,Ys):-
	i(I),I1 is I+1,
	repeat,
	( member(X,Xs), member(Y,Ys),
	  implicate(X,_,Rx,I,_),implicate(Y,_,Ry,I,_),
	  adj(Type,Rx,Ry,Rz,Pre,Suf),
	  insert_newimp(N,Rz,I1),
	  mark_nonprime(Type,X,Y,Pre,Suf),
	  fail
	; true),!.

insert_newimp(N,R,I):-implicate(_,N,R,I,_),!.
insert_newimp(N,R,I):-numimplicates(M),retractall(numimplicates(_)),
	assertz(implicate(M,N,R,I,prime)),
	M1 is M+1, asserta(numimplicates(M1)).

% if matching of type a, Y has more ones
mark_nonprime(a,_X,Y,_Pre,_Suf):-
	mark_implicate_num(Y).
mark_nonprime(b,X,Y,Pre,Suf):-
	mark_implicate_num(X),mark_implicate_num(Y),
	append(Pre,[0|Suf],A),append(Pre,[2|Suf],B),
	mark_implicate(A),mark_implicate(B).

mark_implicate_num(X):-implicate(X,Nx,Rx,I,prime),!,
	retract(implicate(X,Nx,Rx,I,prime)),assert(implicate(X,Nx,Rx,I,nonprime)).
mark_implicate_num(_).
mark_implicate(Rx):-implicate(X,Nx,Rx,I,prime),!,
	retract(implicate(X,Nx,Rx,I,prime)),assert(implicate(X,Nx,Rx,I,nonprime)).
mark_implicate(_).


match_intra_classes([]):-!.
match_intra_classes([r(N,Xs)|Cs]):-
	match_all(N,Xs),
	match_intra_classes(Cs).
	
match_all(_,[]):-!.
match_all(N,[X|Xs]):-match_pairs(b,N,[X],Xs),match_all(N,Xs).

test([(p->q)->r]).
test2([(not p->q)->p]).
test3([(r -> not p v s), (p -> q v not r)]).
test4([(not p -> q) -> not r;p]).

% adj(Type,implicate1,implicate2,resulting_implicate,preffix,suffix)
adj(_,[],[],[],[],[]):-!.
adj(Type,[X|Xs],[X|Ys],[X|Zs],[X|Pre],Suf):-!,adj(Type,Xs,Ys,Zs,Pre,Suf).
adj(Type,[X|Xs],[Y|Xs],[Z|Xs],[],Xs):-adj_val(Type,X,Y,Z),!.

adj_val(a,0,1,n).
adj_val(a,1,0,n).
adj_val(a,1,2,p).
adj_val(a,2,1,p).
adj_val(b,n,p,-).
adj_val(b,p,n,-).

write_classes([]):-!.
write_classes([r(_N,Xs)|Cs]):-write_implicates(Xs),write_classes(Cs).
write_implicates([]):-!.
write_implicates([X|Xs]):-
	implicate(X,_,Rx,_,_),concat_atom(Rx,A),write(A),nl,write_implicates(Xs).


get_cms(L,S):-
	findall(Xs,(get_cm(L,M),cm(_,M,Xs)),S0),
	appendall(S0,S1),sort(S1,S).
	
appendall([],[]).
appendall([X|Xs],Z):-appendall(Xs,Y),append(X,Y,Z).

is_total([]):-!.
is_total([X|Xs]):-X=0,!,is_total(Xs); X=2,is_total(Xs).

submodel([],[]):-!.
submodel([0|Xs],[0|Ys]):-!,submodel(Xs,Ys).
submodel([2|Xs],[Y|Ys]):-(Y=2;Y=1),submodel(Xs,Ys).

get_cm([],[]).
get_cm([X|Xs],[V|Ys]):-label_values(X,Vs),member(V,Vs),get_cm(Xs,Ys).
label_values(0,[0]).
label_values(1,[1]).
label_values(2,[2]).
label_values(n,[0,1]).
label_values(p,[1,2]).
label_values(-,[0,1,2]).

t_closure([],[]):-!.
t_closure([M|Ms],S):-
	is_total(M),!,findall(P,submodel(M,P),Ps),sort(Ps,Ps1),
	t_closure(Ms,Qs),merge_set(Ps1,Qs,S).
t_closure([M|Ms],S):-
	t_closure(Ms,Qs),merge_set([M],Qs,S).

remove_neg_heads:-
	repeat, (
	  implicate(X,Nx,Rx,I,prime),
	  has_neg_head(Rx),
	  retract(implicate(X,Nx,Rx,I,prime)),
	  fail
	; true),!.
	
has_neg_head(Rx):-
	member(p,Rx),                      % it has some 'not p' in the head
	\+ member(1,Rx), \+ member(n,Rx).  % but doesn't have positive lit's in the head

get_implicate_countermodels:-
	repeat, (
	  implicate(X,Nx,Rx,I,prime),
	  get_cms(Rx,CMs),
	  retract(implicate(X,Nx,Rx,I,prime)),
	  assertz(implic(X,Rx,CMs)),
	  fail
	; true),!.

build_chart:-
	repeat, (
	  implic(X,_Rx,CMs),
	  member(M,CMs),
	  asserta(chart(M,X)),
	  fail
	; true),!.
	
filter_essential(Es):-
	findall(X,(chart(M,X),is_essential(M,X)),Es0),sort(Es0,Es),
	remove_covered(Es).
	
remove_covered([]):-!.
remove_covered([X|Xs]):-
	% remove all countermodels covered by X
	findall(M,chart(M,X),Ms),
	repeat, (
	  member(A,Ms),
	  retractall(chart(A,_)),
	  fail
	; true),!,
	remove_covered(Xs).
	
is_essential(M,X):-chart(M,Y),Y \= X,!,fail.
is_essential(_,_).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Building the rules from a set of implicates

build_rules([],[]):-!.
build_rules([X|Xs],[R|Rs]):-
	numatoms(N),
	implic(X,Rx,_),
	build_rule(N,Rx,([] :- []),(H :- B)),
	commas(B,B1),semis(H,H1),
	(H1=false,!,
	  (B1=true,!,R=false
	  ;B1=false,!,R=true
	  ;R=(:-B1)
	  )
	;B1=true,!,R=(H1)
	;R=(H1 :- B1)	),
	build_rules(Xs,Rs).

commas(L,E):-rbinop((,),true,L,E).
semis(L,E):-rbinop((;),false,L,E).

build_rule(_,[],R,R):-!.
build_rule(N,[V|Vs],R0,R):-	
	N1 is N-1,
	theatom(N1,P),add_atom(P,V,R0,R1),build_rule(N1,Vs,R1,R).
	
add_atom(_P,-,R,R):-!.
add_atom(P,n,(H :- B),([P|H] :- B)):-!.
add_atom(P,p,(H :- B),([not P|H] :- B)):-!.
add_atom(P,1,(H :- B),([P,not P|H] :- B)):-!.
add_atom(P,2,(H :- B),(H :- [P|B])):-!.
add_atom(P,0,(H :- B),(H :- [not P|B])):-!.

% rbinop(F,Neut,Xs,E).
rbinop(_F,Neut,[],Neut):-!.
rbinop(_F,_Neut,[X],X):-!.
rbinop(F,Neut,[X|Xs],E):-rbinop(F,Neut,Xs,E0),E =.. [F,X,E0].
	
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
:-dynamic prog_num/1.

main:-
      option(verbose,off),
      set_signature([p,q]),tell('162.txt'),
      asserta(prog_num(1)),
	repeat,
	(generate_countermodels(CMs),	 
	 prog_num(N),retract(prog_num(_)),N1 is N+1,asserta(prog_num(N1)),
	 maplist(to_3valued,CMs,CMs2),
	 write('--- P'),write(N),write(' ---'),nl,
	 write_min_programs(CMs2),nl,
	 fail
	 ; true),!,told.

% write_min_programs(CMs):-
	% minprogram(CMs,P),!,write_program(P).

write_min_programs(CMs):-
	findall(P,minprogram(CMs,P),Ps),write_min_progs(Ps).
	
write_min_progs([X]):-!,write_program(X).
write_min_progs([X|Xs]):-
	write_program(X),nl,write('other choice:'),nl,nl,
	write_min_progs(Xs).

generate_countermodels(CMs):-
	all_true_interp(Z),
	findall(Y,get_subset(Z,Y),Ys),
	generate_countermodels(Ys,[],CMs).
	
generate_countermodels([],CMs,CMs).
generate_countermodels([Y|Ys],CMs0,CMs):-
        findall([X,Y],get_subset(Y,X),CMs1),
	( append(CMs0,CMs1,CMs2) % option 1, include [Y,Y] and all [X,Y]'s
	; extract([Y,Y],CMs1,CMs1b), % otherwise, take any possibility but [Y,Y]
	  sublist(CMs1b,CMs1c),
	  append(CMs0,CMs1c,CMs2)
	),
	generate_countermodels(Ys,CMs2,CMs).

sublist([],[]).
sublist([_|Xs],Ys):-sublist(Xs,Ys).
sublist([X|Xs],[X|Ys]):-sublist(Xs,Ys).

write_program(Rs):-member(R,Rs),write(R),write('.'),nl,fail;true.

extract(X,L,L2):-append(Pre,[X|Suf],L),append(Pre,Suf,L2).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

get_program_cms([],[]):-!.
get_program_cms([R|Rs],CMs):-
	rule_cms(R,CMs1),
	get_program_cms(Rs,CMs2),
	append(CMs1,CMs2,CMs3),sort(CMs3,CMs).

	
rule_cms(R,CMs):-
	transform_rule(R,Hp,Hn,Bp,Bn),
	% gets rid of tautologies
	( intersection(Bp,Bn,A1),A1 \= [],!, CMs=[]
	; intersection(Hp,Bp,A2),A2 \= [],!, CMs=[]
	; intersection(Hn,Bn,A3),A3 \= [],!, CMs=[]
	; % If it's not a tautology, remove redundant info 
	  subtract(Hp,Bn,Hp1), subtract(Hn,Bp,Hn1), 
	  get_labelling(Hp1,Hn1,Bp,Bn,L),
	  findall(M,get_cm(L,M),CMs)
	).
	
transform_rule((H :- B),Hp,Hn,Bp,Bn):-!,
	transform_head(H,Hp,Hn),transform_body(B,Bp,Bn).
transform_rule((:- B),[],[],Bp,Bn):-!,transform_body(B,Bp,Bn).
transform_rule(H,Hp,Hn,[],[]):-!,transform_head(H,Hp,Hn).

transform_head(H,Hp,Hn):-transform_binop((;),H,Hp0,Hn0),sort(Hp0,Hp),sort(Hn0,Hn).
transform_body(B,Bp,Bn):-transform_binop((,),B,Bp0,Bn0),sort(Bp0,Bp),sort(Bn0,Bn).

transform_binop(F,E,Ep,En):-
	E =.. [F,Lit,E1],!,
	transform_binop(F,E1,Ep0,En0),
	( Lit = (not P),!,Ep=Ep0,En=[P|En0]
	; Ep=[Lit|Ep0],En=En0
	).
transform_binop(_F,not P,[],[P]):-!.
transform_binop(_F,P,[P],[]).

get_labelling(Hp,Hn,Bp,Bn,Rx):-numatoms(N),get_labelling(N,Hp,Hn,Bp,Bn,Rx).

get_labelling(0,_Hp,_Hn,_Bp,_Bn,[]):- !.
get_labelling(N,Hp,Hn,Bp,Bn,[V|L]):- 
	P is N-1,
	( member(P,Hp),!,
	  (member(P,Hn),!,V=1
	  ; V=n
	  )
	; member(P,Hn),!, V=p
	; member(P,Bp),!, V=2
	; member(P,Bn),!, V=0
	; V=(-)
	),
	get_labelling(P,Hp,Hn,Bp,Bn,L).
	
%%%%%%%%%%%%%

set_option(OP,VAL):-
	(retractall(option(OP,_)),!;true),
	asserta(option(OP,VAL)).
	
:-write('Type help(minlp) for instructions on use.'),nl.
help(minlp):-
  write('rebuild(T,P)      gets a minimal program P strongly equivalent to an arbitary'),nl,
  write('                  theory T. This theory is a list of formulas using operators:'),nl,
  write('                    ,  &     for conjunction'),nl,
  write('                    ;  v     for disjunction'),nl,
  write('                    not      for (default) negation'),nl,
  write('                    ->       for implication left to right'),nl,
  write('                    :-       for implication right to left'),nl,
  write('                  Example:'),nl,
  write('                  ?- rebuild([(p->q)->r],P),write_program(P).'),nl,
  nl,
  write('write_program(P)  writes a program.'),nl,
  nl,
  write('minimise_program(T,P)'),nl,  
  write('                  works like rebuild but T is restricted to a set of logic'),nl,
  write('                  program rules only allowing the the operators below:'),nl,
  write('                     ,  ;  :-  not'),nl,  
  write('                  Example:'),nl,
  write('                  ?- minimise_program([(p;q :- not p),(q; not q)],P).'),nl,
  nl,
  write('set_option(OP,VAL) sets an option OP to value VAL where:'),nl,
  write('                  OP=verbose          sets verbose mode. VAL can be on or off.'),nl,
  write('                  OP=avoid_neg_head   when VAL=on, implicates without positive'),nl,
  write('                                      head literals are ruled out in favour of'),nl,
  write('                                      constraints.'),nl,
  true.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Petrick's method

ex2(Sol):- petrick([0,1,2,5,6,7],
	[[0,1],
	 [0,2],
	 [1,5],
	 [2,6],
	 [5,7],
	 [6,7]],
	 Sol).
	 
ex3(Sol):- petrick([9,12,13,15],
	[[9,13],
	 [12,13],
	 [9,12,13],
	 [13,15],
	 [9,13,15],
	 [12,13,15]],
	 Sol).

ex4(P):-
	petrick([0,1,2,3],
	[[0,2,3],
	 [1,2],
	 [0,1],
	 [2,3]
        ],P). 
	
petrick(Is,Rs,P4):-
	get_p_funct(Is,Rs,P0),
	findall(T,expand(P0,T),P1),
	sort_by_length(P1,[],P2),
	remove_supersets(P2,P3),
	P3=[L|_],length(L,N),sublist(has_length(N),P3,P4).
has_length(N,L):-length(L,N).
	
get_p_funct([],_,[]):-!.
get_p_funct([I|Is],Rs,Es):-	
	length(Rs,N),
	row_nums(N,I,Rs,E0),
	sort(E0,E),
	get_p_funct(Is,Rs,Es0),
	add_term(Es0,E,Es).

row_nums(0,_I,_Rs,[]):-!.
row_nums(N,I,Rs,Es):-
	M is N-1,
	row_nums(M,I,Rs,Es0),
	nth0(M,Rs,NRowIs),
	(member(I,NRowIs),!,Es=[M|Es0]
	;Es=Es0).

expand([],[]).
expand([L|Ls],Xs):-member(X,L),expand(Ls,Xs0),merge_set([X],Xs0,Xs).

sort_by_length([],Ms,Ms):-!.
sort_by_length([L|Ls],Ms,Ns):-
	insert_by_length(L,Ms,Ms1),sort_by_length(Ls,Ms1,Ns).
insert_by_length(L,[],[L]):-!.
insert_by_length(L1,[L2|Ls],Ms):-
	length(L1,N1),length(L2,N2),
	(N1<N2,!,Ms=[L1,L2|Ls]
	;L1=L2,!,Ms=[L2|Ls]
	;insert_by_length(L1,Ls,Ms0),Ms=[L2|Ms0]
	).

remove_supersets([],[]):-!.
remove_supersets([X|Xs],[X|Ys]):-
	sublist(nonsubset(X),Xs,Xs1),remove_supersets(Xs1,Ys).
nonsubset(A,B):- \+ subset(A,B).
		
% Adds a new subterm, but checks whether it is subsumed by or it
% subsumes other subterms
add_term(A,B,A):-member(S,A),subset(S,B),!.
add_term(A,B,C):-sublist(nonsubset(B),A,A2),merge_set(A2,[B],C).

write_p_funct(P):-get_p_term(*,P,T),write(T),nl.
get_p_term(_Op,P,P):- \+ is_list(P),!.
get_p_term(*,P,T):-maplist(get_p_term(+),P,T0),lbinop(*,false,T0,T).
get_p_term(+,P,T):-maplist(get_p_term(*),P,T0),lbinop(+,true,T0,T).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Handling sets as lists of bits

nbits(30).

holds(N,Xs):-
	nbits(B),
	Pos is N // B,		% compute which int the list
	nth0(Pos,Xs,X),		% take the integer X at position Pos in the list
	M is N mod B,		% which bit inside X
	Z is 2 ** M /\ X, Z \= 0.

write_atoms:-theatom(_,A),write(A),fail; true.

write_set(X):-
	numatoms(N),write_set2(0,N,X).
write_set2(M,N,_X):-
	M=N,!.
write_set2(M,N,X):-
	(holds(M,X),!,write(1);write(0)),
	M1 is M+1,
	write_set2(M1,N,X).	

get_subset([],[]):-!.
get_subset([X|Xs],[Y|Ys]):-
	nbits(B),M is 2 ** (B-1),get_subset_elem(M,X,Y),get_subset(Xs,Ys).

get_subset_elem(0,X,X):-!.
get_subset_elem(Mask,X,Y):-
	Z is Mask /\ X,
	( Z=0, X1=X
	; Z \= 0,(X1=X; X1 is X /\ (\ Mask))
	), 
	Mask2 is (Mask >> 1),
	get_subset_elem(Mask2,X1,Y).
	
all_true_interp(I):-nbits(B),numatoms(N),all_true_interp(N,B,I).
all_true_interp(N,B,[X]):-N<B,!,X is 2^N - 1.
all_true_interp(N,B,[X|Xs]):-
	X is 2^B - 1,M is N-B,all_true_interp(M,B,Xs).


to_3valued(I,J):- numatoms(N),to_3valued(N,I,J).
to_3valued(0,_,[]):-!.
to_3valued(N,[X,Y],[V|Vs]):-
	N1 is N-1,
	(holds(N1,X),!,V=2
	;holds(N1,Y),!,V=1
	;V=0),
	to_3valued(N1,[X,Y],Vs).

count(_X,[],0):-!.
count(X,[X|Xs],N):-!,count(X,Xs,M),N is M+1.
count(X,[_|Xs],N):-count(X,Xs,N).
