:- set_flag(output_options, [depth(full)]).
:- lib(fd).
%%%%%%%%% parameters %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
size(5,5).
start(1,1).
%%%%%%%%% implementation part %%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%% flux interpreter for ALP %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
:- op(700, fy, not).
:- op(800, xfy, and).
:- op(900, xfy, or).
:- local reference(state).
run(P) :- init(Z), setval(state, Z-s0), call(P),
getval(state, _-S), write_canonical(S).
?(F1 and F2) :- ?(F1), ?(F2), !.
?(F1 or F2) :- ?(F1); ?(F2), !.
?(not not F) :- ?(F), !.
?(not (F1 and F2)) :- ?(not F1 or not F2), !.
?(not (F1 or F2)) :- ?(not F1 and not F2), !.
?(not F) :- getval(state,Z-_), \+ holds(F,Z), !.
?(F) :- getval(state,Z-_), holds(F,Z), !.
do(A) :- getval(state,Z-S), poss(A,Z), state_update(Z,A,Z1),
setval(state,Z1-do(A,S)).
%%%%%%%%% special flux %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
holds(F, [F|_]).
holds(F, Z) :- Z=[F1|Z1], F\==F1, holds(F, Z1).
holds(F, [F|Z], Z).
holds(F, Z, [F1|Zp]) :- Z=[F1|Z1], F\==F1, holds(F, Z1, Zp).
minus_(Z, [], Z).
minus_(Z, [F|Fs], Zp) :-
(\+ holds(F, Z) -> Z1=Z ; holds(F, Z, Z1)),
minus_(Z1, Fs, Zp).
plus_(Z, [], Z).
plus_(Z, [F|Fs], Zp) :-
(\+ holds(F, Z) -> Z1=[F|Z] ; holds(F, Z), Z1=Z),
plus_(Z1, Fs, Zp).
update(Z1, ThetaP, ThetaN, Z2) :-
minus_(Z1, ThetaN, Z), plus_(Z, ThetaP, Z2).