:- lib(fd).
:- lib(chr).
:- chr('4_fluent').
 

ab_res([],Z) :- init(Z).
ab_res([[A,Y]|S],Z) :- ab_res(S,Z1),
                       ( state_update(Z1,A,Z,Y)
                         ;
                         ab_state_update(Z1,A,Z,Y) ).

execute(A,Z1,Z2) :-
   perform(A,Y)  -> ( nonvar(Z1), Z1=[sit(S)|Z], ! ; S=[], Z=Z1 ),
                    ( state_update(Z,A,Z3,Y) ; ab_res([[A,Y]|S],Z3) ),
                    !, Z2=[sit([[A,Y]|S])|Z3].

holds(F, [F|_]).
holds(F, Z) :- nonvar(Z), Z=[F1|Z1], F\==F1, holds(F, Z1).

holds(F, [F|Z], Z).
holds(F, Z, [F1|Zp]) :- nonvar(Z), Z=[F1|Z1], F\==F1, holds(F, Z1, Zp).

minus_(Z, [], Z).
minus_(Z, [F|Fs], Zp) :-
   ( \+ not_holds(F, Z) -> holds(F, Z, Z1) ;
     \+ holds(F, Z)     -> Z1 = Z
                         ; cancel(F, Z, Z1), not_holds(F, Z1) ),
   minus_(Z1, Fs, Zp).

plus_(Z, [], Z).
plus_(Z, [F|Fs], Zp) :-
   ( \+ holds(F, Z)     -> Z1=[F|Z] ;
     \+ not_holds(F, Z) -> Z1=Z
                         ; cancel(F, Z, Z2), not_holds(F, Z2), Z1=[F|Z2] ),
   plus_(Z1, Fs, Zp).

cancel(F,Z1,Z2) :-
   var(Z1)    -> cancel(F,Z1), cancelled(F,Z1), Z2=Z1 ;
   Z1 = [G|Z] -> ( F\=G -> cancel(F,Z,Z3), Z2=[G|Z3]
                         ; cancel(F,Z,Z2) ) ;
   Z1 = []    -> Z2 = [].

update(Z1, ThetaP, ThetaN, Z2) :-
   minus_(Z1, ThetaN, Z), plus_(Z, ThetaP, Z2).

knows(F, Z) :- \+ not_holds(F, Z).

knows_not(F, Z) :- \+ holds(F, Z).

knows_val(X, F, Z) :- holds(F, Z), knows_val(X).

:- dynamic known_val/1.

knows_val(X) :- dom(X), \+ nonground(X), ambiguous(X) -> false.
knows_val(X) :- retract(known_val(X)).

dom([]).
dom([X|Xs]) :- dom(Xs), ( is_domain(X) -> indomain(X)
                                        ; true ).

ambiguous(X) :- retract(known_val(_)) -> true
                ;
                assert(known_val(X)), false.