:- dynamic(fdet/1).
:- dynamic(society_goal/0).

:- dynamic(pirati_sokb/5).

:- dynamic(voting/4).

:- dynamic(abduci/5).

:- dynamic(my_sumlist/2).

:- dynamic(my_maximize/2).

:- use_module(library(clpfd)).

:- use_module(library(lists)).

society_goal :- 
    M=9,
    N=4,
    h(start(M,N),0),
    pirati_sokb(Lmon,Lvoti,N,M,1),
    write(mone(Lmon)),
    nl,
    write(voti(Lvoti)),
    nl.

pirati_sokb([],[],N,_,T) :- 
    T>N.

pirati_sokb(Lmon,Lvoti,N,M,T) :- 
    T=<N,
    length(Lmon,N),
    length(Lvoti,N),
    domain(Lmon,0,M),
    domain(Lvoti,0,1),
    Ndead is T-1,
    length(Ldead,Ndead),
    append(Ldead,Lalive,Lmon),
    sum(Lmon,#=,M),
    nth(T,Lmon,MonPir),
    length(ALIVE,N),
    nth(T,ALIVE,Win),
    my_sumlist(Lvoti,Nvoti),
    clp_constraint(Nvoti*2#>N-T+1#<=>Win),
    clp_constraint(MoneteOttenute#=Win*MonPir),
    my_maximize((T1 is T+1,pirati_sokb(_,_,N,M,T1),abduci(Lmon,Lvoti,ALIVE,N,T),labeling([],Lmon),labeling([],Lvoti)),MoneteOttenute).

voting(T,N,[V],Ntot) :- 
    quant(T,existsf),
    quant(N,existsf),
    quant(V,existsf),
    quant(_,existsf),
    clp_constraint(N-1#=Ntot-T),
    e(pirate(N,V,_),T).

voting(T,N,[V|LV],Ntot) :- 
    quant(T,existsf),
    quant(N,existsf),
    quant(V,existsf),
    quant(_,existsf),
    clp_constraint(T#=<Ntot),
    clp_constraint(T#>0),
    clp_constraint(N-1#<Ntot-T),
    N1 is N+1,
    voting(T,N1,LV,Ntot),
    e(pirate(N,V,_),T).

abduci([],[],[],0,_) :- 
    !.

abduci([Mon|Lmon],[V|LV],[Alive|Lalive],N,T) :- 
    quant(Mon,existsf),
    quant(V,existsf),
    quant(Alive,existsf),
    quant(N,existsf),
    quant(T,existsf),
    !,
    N>0,
    e(pirate(N,V,Mon,Alive),T),
    Alive in 0..1,
    N1 is N-1,
    abduci(Lmon,LV,Lalive,N1,T).

my_sumlist(L,N) :- 
    sum(L,#=,N).

my_maximize(Goal,F) :- 
    maximize(Goal,F),
    call(Goal),
    !.