%----------------------------------------------------------
% "sciff.pl"
%
% Author: Marco Alberti
% Created: Sept. 29, 2003
%
% Modified by: Federico Chesani
% Modified at: Aug. 30, 2005
%
% Modified by: Federico Chesani
% Modified at: Dec. 01, 2005
%
%
% Version: 1.00.01
%----------------------------------------------------------
%:- multifile(fdet/1).
%:- dynamic(fdet/1).



%----------------------------------------------------------
% CONSULTING THE MODULES
%----------------------------------------------------------




:- use_module(library(terms)).
:- use_module(reified_unif).

:- use_module(prolog_version).
:- (is_dialect(swi) 
	-> use_module(swi_specific),
       [my_chr_extensions] % In SWI, my_chr_extensions must be loaded after reified_unif
	 ;
    is_dialect(sicstus)
    -> ensure_loaded(my_chr_extensions),
       use_module(sicstus_specific)
    ;   write('Unrecognized Prolog System'), nl, fail
    ).

:- use_module(library(chr)).
:- use_module(proof_util).
:- use_module(quantif).
:- use_module(ccopy).
:- use_module(ics_quant).
:- use_module(library(lists)).
%         [append/3,
%          delete/3,
%      		nth/4,
%      		member/2]).
:- use_module(library(terms),
         [term_variables/2]).

%:- ensure_loaded(solver).
:- use_module(solver).
%:- use_module(domains).
:- use_module(history_parser).
:- use_module(sokb_parser).
:- use_module(ics_parser).
:- use_module(sciff_options).
:- use_module(debug).
:- use_module(help).
:- use_module(graphviz).

:- ensure_loaded(defaults).
:- use_module(library(clpfd)).  % used by invert_constraint in SWI, and in old SCIFF code (e.g., block world)
:- [pretty_print].

%----------------------------------------------------------
% DECLARATIONS
%----------------------------------------------------------
%handler society_proof.

%option(already_in_store,on).

:- chr_option(debug,on). % Se lo metto on mi da` un errore




%----------------------------------------------------------
% IMPOSING IC/PSIC
%
% Quantify the variables in an imposed IC, and impose the result as a
% PSIC
%----------------------------------------------------------
:- chr_constraint
	ic/2, psic/2.
impose_ics @
    ic(Body1,Head1)
    ==>
    %unfold_nonrecursive(psic(Body1,Head1),PSIC),
    %impose_psic(PSIC).
    convert_to_psic(ic(Body1,Head1),PSIC),
    call(PSIC).
    %psic(BodyPSIC,HeadPSIC).

convert_to_psic(ic(Body1,Head1),PSIC):-
    unfold_nonrecursive(psic(Body1,Head1),NewPSIC),
    (NewPSIC = psic(BodyUnf,HeadUnf)
        ->  quantify_variables_in_ics(ics(BodyUnf,HeadUnf),
                  ics(Body2,Head2)),
            rewrite_body_terms(Body2,Body3),
            BodyPSIC=Body3, HeadPSIC=Head2,
            PSIC=psic(BodyPSIC,HeadPSIC)
        ;   PSIC=true).


%----------------------------------------------------------
% IMPOSING VARIOUS CONSTRAINTS
%----------------------------------------------------------
:- chr_type functarity ---> [any,int].
:- chr_type posexp ---> e(functarity,?,int).
:- chr_type list(T) --->    [] ; [T | list(T)].
:- chr_constraint
    h/3, en/3, note/2, noten/2, fulf/1, viol/1, pending/1, abd/3,
    e/3.
    %e(+functarity,?,?int).
    %ground_time/0.

get_functor(do(_,_,Main,_),[F,A]):- !, functor(Main,F,A).
get_functor(do(_,_,_,Main,_),[F,A]):- !, functor(Main,F,A).
get_functor(Main,[F,A]):- !, functor(Main,F,A).

h(Event,Time):-
    get_functor(Event,F),
    h(F,Event,Time).

e(Event,Time):-
    get_functor(Event,F),
    e(F,Event,Time).

en(Event,Time):-
    get_functor(Event,F),
    en(F,Event,Time).

abd(Event,Time):-
    get_functor(Event,F),
    abd(F,Event,Time).

% In SICStus 4 there is no remove_constraint, so we remove constraints
% with simpagation rules
fulf(e(F,EEvent,ETime)) \ pending(e(F,EEvent,ETime)) <=> true.
viol(en(F,EEvent,ETime)) \ pending(en(F,EEvent,ETime)) <=> true.
viol(e(F,EEvent,ETime)) \ pending(e(F,EEvent,ETime)) <=> true.  
viol(gt_current_time(e(F,Event,Time), _)) \ pending(e(F,Event,Time)) <=> true.


% Adds the [functor,arity] term to expectations & happened events
% in the body of ICs.
rewrite_body_terms([H,NotH,E,NotE,En,NotEn,Abd,A],[H1,NotH,E1,NotE,En1,NotEn,Abd1,A]):-
    rewrite_body_atom(H,H1),
    rewrite_body_atom(E,E1),
    rewrite_body_atom(Abd,Abd1),
    rewrite_body_atom(En,En1).
    
rewrite_body_atom([],[]).
rewrite_body_atom([h(E,T)|LH],[h(F,E,T)|LH1]):-
    get_functor(E,F),
    rewrite_body_atom(LH,LH1).
rewrite_body_atom([e(E,T)|LH],[e(F,E,T)|LH1]):-
    get_functor(E,F),
    rewrite_body_atom(LH,LH1).
rewrite_body_atom([en(E,T)|LH],[en(F,E,T)|LH1]):-
    get_functor(E,F),
    rewrite_body_atom(LH,LH1).
rewrite_body_atom([abd(E,T)|LH],[abd(F,E,T)|LH1]):-
    get_functor(E,F),
    rewrite_body_atom(LH,LH1).







%----------------------------------------------------------
% EVENT CALCULUS and FACTORING
%
% To carefully think about it...
%----------------------------------------------------------
% Questo andrebbe messo come IC.
% Non posso avere 2 eventi nello stesso tempo
sequential_act @
    e([act,1],act(E1),T1) \
    e([act,1],act(E2),T2)
    <=> sciff_option(seq_act,on),
    T2=T1 | E1=E2.


% factoring
% This factoring is specilised for the abductive event calculus
% Questo factoring va legato ad una regola che toglie uno degli abd
% se ce ne sono 2 identici. Nel caso dell'EC c'e` gia` (che vieta 2 eventi
% nello stesso tempo).

%factoring_ec @
%    e(act(X1),T1), e(act(X2),T2)
%    ==>
%    sciff_option(factoring,on),
%    nonvar(X1), nonvar(X2) |
%    reif_unify(e(act(X1),T1),e(act(X2),T2),B),
%    (B=1 ; B=0).


%% Secondo tentativo: fa l'unificazione dei tempi solo se l'azione
%% e` gia` ground
factoring2 @
    e(F,X,T1), e(F,X,T2)
    ==>
    sciff_option(factoring,on),
    ground(X) |
    (eq(T1,T2) ;
    neq(T1,T2), when(?=(T1,T2),T1\==T2)).
% La seconda serve perche' cosi` se e` la stessa var fallisce
% senza dover usare la (poca) propagazione del diverso.
%%    T1 #= T2 #<=> B,
%%    (B=1 ; B=0).






%----------------------------------------------------------
% ITERATIVE DEEPENING: max number of e(act(...)).
%----------------------------------------------------------
:- chr_constraint 
	max_depth/1.
max_depth_e_act @
e([act,1],act(_),_), max_depth(DepthMax) ==>
    %findall_constraints(e(_,act(_),_),L), length(L,N), N>DepthMax | fail.
    max_constraints(e(_,act(_),_),DepthMax).


%%%MARCOM
max_depth_e_act @
h([sono,4],sono(_,_,_,_),_), max_depth(DepthMax) ==>
    findall_constraints(h(_,sono(_,_,_,_),_),L), length(L,N), N>DepthMax | writeln(ciao(N)),fail.
    %max_constraints(e(_,sono(_,_,_,_),_),DepthMax).



%----------------------------------------------------------
% ITERATIVE DEEPENING: max number of violation
%----------------------------------------------------------
:- chr_constraint
	max_viol/1.
max_violations @
viol(_), max_viol(MaxViol) ==> 
    findall_constraints(viol(_),L), %write(L), 
    length(L,N), 
    write(N) 
    | 
    lt(MaxViol,1000), 
    leq(N,MaxViol).





e_consistency @
    e(F,EEvent,ETime),
    en(F,ENEvent,ENTime)
    ==>
    %findall_constraints(gen_phase,[]) |
    %add_arc_graph('E-consistency',e(EEvent,ETime)\=en(ENEvent,ENTime)),
    check_unification(p(EEvent,ETime),p(ENEvent,ENTime),0,e,en).



%
pending_en @
    en(F,Event,Time)
    ==>
    pending(en(F,Event,Time)).


:- chr_constraint
	nondeterministic/1, phase/1, remove_phase/0.

propagation_h @
    h(F,Event1,Time1),
    psic([[h(F,Event2,Time2)|MoreH],NotH,E,NotE,En,NotEn,Abd,A],Head)
    ==>
    fn_ok(Event1,Event2)
    |
    ccopy(p([[h(Event2,Time2)|MoreH],NotH,E,NotE,En,NotEn,Abd,A],Head),
      p([[h(Event2a,Time2a)|MoreHa],NotHa,Ea,NotEa,Ena,NotEna,Abda,Aa],Heada)),
    (subsumeschk(p(Event2a,Time2a),p(Event1,Time1)),
     is_term_quantified(h(Event2a,Time2a),forall)
     ->    %reif_unify(p(Event1,Time1),p(Event2a,Time2a),1),
            (Event1=Event2a, Time1=Time2a
                ->  psic([MoreHa,NotHa,Ea,NotEa,Ena,NotEna,Abda,Aa],Heada)
                ;   true)
     ;  reif_unify(p(Event1,Time1),p(Event2a,Time2a),B),
        PSIC=psic([MoreHa,NotHa,Ea,NotEa,Ena,NotEna,Abda,Aa],Heada),
        (B==1 -> call(PSIC) ;
         B==0 -> true ;
        nondeterministic((B=1, call(PSIC);
        B=0))
        )
    ).

propagation_e @
    e(F,Event1,Time1),
    psic([[],NotH,[e(F,Event2,Time2)|MoreE],NotE,En,NotEn,Abd,A],Head)
    ==>
    fn_ok(Event1,Event2)
    |
    ccopy(p([[],NotH,[e(Event2,Time2)|MoreE],NotE,En,NotEn,Abd,A],Head),
      p([[],NotHa,[e(Event2a,Time2a)|MoreEa],NotEa,Ena,NotEna,Abda,Aa],Heada)),
   reif_unify(p(Event1,Time1),p(Event2a,Time2a),B),
   status(S,F),
       (draw_graph(S,propagation_e,e(Event1,Time1)=e(Event2,Time2)),
       B=1, psic([[],NotHa,MoreEa,NotEa,Ena,NotEna,Abda,Aa],Heada)
       ;
       draw_graph(S,propagation_e,e(Event1,Time1)\=e(Event2,Time2)),
       B=0).
% End modification
% Original version:
/*
propagation_e @
    e(Event1,Time1),
    psic([H,NotH,[e(Event2,Time2)|MoreE],NotE,En,NotEn,Abd,A],Head)
    ==>
    fn_ok(Event1,Event2)
    |
    ccopy(p([H,NotH,[e(Event2,Time2)|MoreE],NotE,En,NotEn,Abd,A],Head),
      p([Ha,NotHa,[e(Event2a,Time2a)|MoreEa],NotEa,Ena,NotEna,Abda,Aa],Heada)),
   reif_unify(p(Event1,Time1),p(Event2a,Time2a),B),
   status(S,F),
       (draw_graph(S,propagation_e,e(Event1,Time1)=e(Event2,Time2)),
       B#=1, psic([Ha,NotHa,MoreEa,NotEa,Ena,NotEna,Abda,Aa],Heada)
       ;
       draw_graph(S,propagation_e,e(Event1,Time1)\=e(Event2,Time2)),
       B#=0).
*/
% End Original version



% Modified by Federico Chesani
% Date 20060404 1230
propagation_note @
    note(Event1,Time1),
    psic([[],NotH,[],[note(Event2,Time2)|MoreNotE],En,NotEn,Abd,A],Head)
    ==>
    fn_ok(Event1,Event2)
    |
    ccopy(p([[],NotH,[],[note(Event2,Time2)|MoreNotE],En,NotEn,Abd,A],Head),
    
p([[],NotHa,[],[note(Event2a,Time2a)|MoreNotEa],Ena,NotEna,Abda,Aa],Heada)),
   reif_unify(p(Event1,Time1),p(Event2a,Time2a),B),
       (B=1, psic([[],NotHa,[],MoreNotEa,Ena,NotEna,Abda,Aa],Heada);
       B=0).
% End Modification       
% Original Version:
/*
propagation_note @
    note(Event1,Time1),
    psic([[],NotH,[],[note(Event2,Time2)|MoreNotE],En,NotEn,Abd,A],Head)
    ==>
    fn_ok(Event1,Event2)
    |
    ccopy(p([H,NotH,E,[note(Event2,Time2)|MoreNotE],En,NotEn,Abd,A],Head),
    
p([Ha,NotHa,Ea,[note(Event2a,Time2a)|MoreNotEa],Ena,NotEna,Abda,Aa],Heada)),
   reif_unify(p(Event1,Time1),p(Event2a,Time2a),B),
       (B#=1, psic([Ha,NotHa,Ea,MoreNotEa,Ena,NotEna,Abda,Aa],Heada);
       B#=0).
*/

/*
propagation_e @
    e(F,Event1,Time1),
    psic([[],NotH,[e(F,Event2,Time2)|MoreE],NotE,En,NotEn,Abd,A],Head)
    ==>
    fn_ok(Event1,Event2)
    |
    ccopy(p([[],NotH,[e(Event2,Time2)|MoreE],NotE,En,NotEn,Abd,A],Head),
      p([[],NotHa,[e(Event2a,Time2a)|MoreEa],NotEa,Ena,NotEna,Abda,Aa],Heada)),
   reif_unify(p(Event1,Time1),p(Event2a,Time2a),B),
   status(S,F),
       (draw_graph(S,propagation_e,e(Event1,Time1)=e(Event2,Time2)),
       B#=1, psic([[],NotHa,MoreEa,NotEa,Ena,NotEna,Abda,Aa],Heada)
       ;
       draw_graph(S,propagation_e,e(Event1,Time1)\=e(Event2,Time2)),
       B#=0).
*/

propagation_en @
    en(F,Event1,Time1),
    psic([[],NotH,[],[],[en(F,Event2,Time2)|MoreEn],NotEn,Abd,A],Head)
    ==>
    fn_ok(Event1,Event2)
    |
    ccopy(p([[],NotH,[],[],[en(Event2,Time2)|MoreEn],NotEn,Abd,A],Head),
      p([[],NotHa,[],[],[en(Event2a,Time2a)|MoreEna],NotEna,Abda,Aa],Heada)),
    ccopy( p(  Event1,  Time1),
           p( Event1a, Time1a)),
     reif_unify(p(Event1a,Time1a),p(Event2a,Time2a),B),
       (B=1, psic([[],NotHa,[],[],MoreEna,NotEna,Abda,Aa],Heada);
       B=0).

propagation_noten @
    noten(Event1,Time1),
    psic([[],NotH,[],[],[],[noten(Event2,Time2)|MoreNotEn],Abd,A],Head)
    ==>
    fn_ok(Event1,Event2)
    |
    ccopy( p([[], NotH, [], [], [], [noten(Event2, Time2)| MoreNotEn], Abd,A], Head),
           p([[],NotHa,[],[],[],[noten(Event2a,Time2a)|MoreNotEna],Abda,Aa],Heada)),
    ccopy( p(  Event1,  Time1),
           p( Event1a, Time1a)),
	reif_unify(p(Event1a,Time1a),p(Event2a,Time2a),B),
    (	B=1, psic([[],NotHa,[],[],[],MoreNotEna,Abda,Aa],Heada)
    	;
       	B=0).
  

propagation_abd @
    abd(F,Event1,Time1),
    psic([[],NotH,[],[],[],[],[abd(F,Event2,Time2)|MoreAbd],A],Head)
    ==>
    fn_ok(Event1,Event2)
    |
    %ccopy(p([[],NotH,[],[],[],[],[abd(Event2,Time2)|MoreAbd],A],Head),
	%				p([[],NotHa,[],[],[],[],[abd(Event2a,Time2a)|MoreAbda],Aa],Heada)),
	ccopy(p(NotH, Event2, Time2, MoreAbd, A, Head),
		  p(NotHa,Event2a,Time2a,MoreAbda,Aa,Heada)),
    (subsumeschk(p(Event2a,Time2a),p(Event1,Time1)),
     is_term_quantified(abd(Event2a,Time2a),forall)
     -> (Event2a = Event1, Time2a=Time1
            ->  psic([[],NotHa,[],[],[],[],MoreAbda,Aa],Heada)
            ;   true)
     ;  reif_unify(p(Event1,Time1),p(Event2a,Time2a),B),
        (B=1, psic([[],NotHa,[],[],[],[],MoreAbda,Aa],Heada);
        B=0)
    ).





propagation_violated @
    viol(Event1),
    psic([[],NotH,[],[],[],[],[abd([viol,1],viol(Event2),_Time2)|MoreAbd],A],Head)
    ==>
    sciff_option(violation_causes_failure,no),
    fn_ok(Event1,Event2)
    |
    ccopy(p([[],NotH,[],[],[],[],[viol(Event2)|MoreAbd],A],Head),
    
p([[],NotHa,[],[],[],[],[viol(Event2a)|MoreAbda],Aa],Heada)),
    reif_unify(p(Event1),p(Event2a),B),
%       (B#=1, psic([[],NotHa,[],NotEa,ENa,NotEna,MoreAbda,Aa],Heada);
       (B=1, psic([[],NotHa,[],[],[],[],MoreAbda,Aa],Heada);
       B=0).

% Two terms may be unifiable.
% Profiled version, nearly twice as fast

fn_ok(Term1,Term2):- Term1 == Term2,!. % either if they are identical
fn_ok(Term1,Term2):- \+(?=(Term1,Term2)). % or if they are syntactically unifiable

/* old version 
fn_ok(Term1,Term2):-
    nonvar(Term1),
    nonvar(Term2),
    !,
    Term1=..[H|T1],
    Term2=..[H|T2],
    fn_ok_list(T1,T2).
fn_ok(_,_).
*/


fn_ok_list([],[]).
fn_ok_list([H1|T1],[H2|T2]):-
    fn_ok(H1,H2),
    fn_ok_list(T1,T2).


split_list(List,1,[],List):-
    !.
split_list([Head|Tail],N,[Head|Tail1],Rest):-
    N1 is N-1,
    split_list(Tail,N1,Tail1,Rest).

type_position(h,1).
type_position(noth,2).
type_position(e,3).
type_position(note,4).
type_position(en,5).
type_position(noten,6).
  


logical_equivalence @
%    psic(true,Head) MarcoG: questa mi sembra obsoleta ...
    psic([[],[],[],[],[],[],[],[]],Head)
    <=>
    add_arc_graph(logical_equivalence,(true->Head)),
    impose_head1(Head).

naf(Goal):-
    commas_to_list(Goal,GoalList),
    ics_quant:split_body(GoalList,Body),
    psic(Body,[]).


unfold_psic @
    psic([[],[],[],[],[],[],[],Atoms],Head)
    <=>
    %status(S,F),
    %draw_graph(S, unfolding_psic, Atoms),
    unfold([psic(Atoms,Head)]).

unfold([]):-
    !.
unfold([psic([],Head)|MorePSICS]):- !, 
    % MarcoG Bug fix: the cut was after the call to psic.
    % psic is a CHR constraint, that is rewritten to a Prolog predicate
    % that embeds in its definitions the CHR rules that involve the constraint psic.
    % So, by adding a cut after this, we are cutting the choice points inside
    % the rules that involve psic, so sometimes it cuts alternatives in the
    % head!!  
    %psic([[],[],[],[],[],[],[],[]],Head),
    impose_head1(Head),
    unfold(MorePSICS).
unfold([psic([naf(Goal)|Body],Head)|PSICS]):- !,
    commas_to_list(Goal,GoalList),
    append(Head,[GoalList],NewHead),
    psic([[],[],[],[],[],[],[],Body],NewHead),
    unfold(PSICS).
unfold([psic([clp_constraint(Constraint)|MoreBodyAtoms],Head)|MorePSICS]):-
    call(Constraint),
    unfold([psic(MoreBodyAtoms,Head)|MorePSICS]).
unfold([psic([clp_constraint(Constraint)|_MoreBodyAtoms],_Head)|MorePSICS]):- !,
% MarcoG: metto una pezza, perche' il vincolo a volte e` una restriction
% e non riesce a fare st(C) #<=> 0, pero` si puo` fare st(C) #<=> 0
    invert_constraint(Constraint),
    unfold(MorePSICS).
% MarcoG 12 jul 2006: Sometimes the clause generated with
% unfolding contains the explicit quantification of a
% variable. The quantification is different in PSICs.
% I ignore it for the moment, but maybe it should be
% considered better ...
unfold([psic([quant(_,_)|Body],Head)|MorePSICS]):- !,
    unfold([psic(Body,Head)|MorePSICS]).

% Federico 08 Jun 2007: Managing abducibles introduced by previous unfolding
unfold([psic([AnAtom|Body],Head)|PSICS]):-
	is_SCIFF_RESERVED(AnAtom),
	!,
	ic([AnAtom|Body],Head),
	unfold(PSICS).
	
	
%%% MARCOM: Aggiunta ad-hoc per trattare la negazione di holds_at in mutua esclusione %%%
unfold([psic([not_holdsat(F,T)|Body],Head)|PSICS]):- !,
	append_naf(Head, holds_at(F, T), ExtHead),
    append(ExtHead,[[test_holds_at(F, T)]],NewHead),
    %end modified part
    psic([[],[],[],[],[],[],[],Body],NewHead),
    unfold(PSICS).    
    
append_naf([],Goal,[]).
append_naf([Conjunct|MoreConjuncts], Goal, [[naf(Goal)|Conjunct]|MoreExtConjuncts]):-
	append_naf(MoreConjuncts, Goal, MoreExtConjuncts).	
		



unfold([PSIC|MorePSICS]):-
    PSIC=psic([BodyAtom|_],_),
    predicate_property(BodyAtom, dynamic),
    !,
    get_candidate_clauses(BodyAtom,Clauses),
    check_forall(Clauses),
    get_unfolded_psics(Clauses,PSIC,UnfoldedPSICS),
    append(UnfoldedPSICS,MorePSICS,NewPSICS),
    unfold(NewPSICS).

unfold([PSIC|MorePSICS]):-
    PSIC=psic([BodyAtom|_],_),
    is_sicstus_predicate(BodyAtom),!,
    findall(clause(BodyAtom,[]),BodyAtom,Clauses),
    get_unfolded_psics(Clauses,PSIC,UnfoldedPSICS),
    append(UnfoldedPSICS,MorePSICS,NewPSICS),
    unfold(NewPSICS).

% totally unknown predicate: undefined, not built-in.
unfold([PSIC|MorePSICS]):-
    PSIC=psic([BodyAtom|_],_),
    \+predicate_property(BodyAtom, _),!,unfold(MorePSICS).

% MarcoG: The current atom in the PSIC is not a
% defined predicate, nor a built-in. It must have come
% out from unfolding, and must be an H, or an abducible.
% Let us just re-state the IC, so it will be re-parsed
% and quantified by impose_ics. Hope the quantification
% is correct (to do: check if the quantification is correct)


unfold([psic(_,_)|_]):-
    writeln('An error occured while applying unfolding transition.'),
    writeln('Please communicate this error to SCIFF developers as soon as possible!'),
    writeln('Many Thanks!'),
    fail.


unfold_nonrecursive([],[]):- !. % The PSIC could not have any fact matching it
% ie., the PSIC can be removed. We represent this fact with the emptylist
% it is used by the recursive call (get_unfolded_nonrecursive can return
% the emptylist)
unfold_nonrecursive(psic(Body,Head),UnfoldedPSIC):-
    select(Atom,Body,BodyRest),
    predicate_property(Atom,dynamic),
    is_unquantified(Atom), % This way, I am ure it is not invoked by unfolding
    %copy_term(Atom,Atom1), does not strip constraints
    functor(Atom,F,Arity),
    functor(Atom1,F,Arity),  %this strips constraints, in case the IC was called not in the beginning, e.g., by unfold.
    findall((Atom1,BodyClause),clause(Atom1,BodyClause),Clauses),
    nonrecursive(Clauses),!,
    get_unfolded_nonrecursive(Atom,BodyRest,Head,Clauses,[UnfoldedPSIC1]),
    unfold_nonrecursive(UnfoldedPSIC1,UnfoldedPSIC).
unfold_nonrecursive(X,X).

% Currently unfolds eagerly only predicates consisting of exactly one fact.
nonrecursive([(_,true)]).
get_unfolded_nonrecursive(Atom,BodyRest,Head,[(Atom1,_BodyClause)],[UnfoldedPSIC1]):-
    (Atom = Atom1
     ->    UnfoldedPSIC1 = psic(BodyRest,Head)
     ;     UnfoldedPSIC1 = [] % The atom in the body of PSIC does not unify with
                              % the only fact defining it -> the PSIC is removed
    ).

% We assume that all predicates imported from some module are built-in
is_sicstus_predicate(Pred) :- 
    predicate_property(Pred,Prop),
    % Added also interpreted and compiled, so we can invoke predicates defined in
    % SCIFF itself
    memberchk(Prop,[built_in,imported_from(_),interpreted,compiled]).

%is_sicstus_predicate(Pred) :- member(Pred, [ground, var, nonvar, write, nl, =, memberchk, last_state]).
%is_sicstus_predicate(Pred) :- member(Pred, [ground, var, nonvar, write, nl, =, memberchk]).
% End modification

% ORIGINAL VERSION:
/*
unfold([PSIC|MorePSICS]):-
    PSIC=psic([BodyAtom|_],_),
    get_candidate_clauses(BodyAtom,Clauses),
  
    write('Unfolding: BodyAtom:'), nl,
    write(BodyAtom), nl,
    write('Unfolding: Clauses:'), nl,
    write(Clauses), nl,
  
    check_forall(Clauses),
    get_unfolded_psics(Clauses,PSIC,UnfoldedPSICS),
    append(UnfoldedPSICS,MorePSICS,NewPSICS),
    unfold(NewPSICS).
*/
% End original version
% End Modification
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

invert_constraint(st(reif_unify(X,Y,B))):- !,
    Bneg in 0..1,
    Bneg #= 1-B,
    reif_unify(X,Y,Bneg).
invert_constraint(reif_unify(X,Y,B)):- !,
    Bneg in 0..1,
    Bneg #= 1-B,
    reif_unify(X,Y,Bneg).
invert_constraint(Constraint):-
    (Constraint = st(Restriction)
        ->  once(opposite(Restriction,Opp)),
            st(Opp)
        ;   once(opposite(Constraint,Opp)),
            call(Opp)
    ).

check_forall(Term):-
    term_variables(Term,Variables),
    quantify_unquantified(Variables,forall).

quantify_unquantified([],_).
quantify_unquantified([Var|MoreVars],Quant):-
    get_quant(Var,_),
    !,
    quantify_unquantified(MoreVars,Quant).
quantify_unquantified([Var|MoreVars],Quant):-
    set_quant(Var,Quant),
    quantify_unquantified(MoreVars,Quant).


get_unfolded_psics([],_,[]).
get_unfolded_psics([clause(CHead,CBody)|MoreClauses],
           PSIC,
           UnfoldedPSICS):-
    (MoreClauses = []
        ->  PSIC=psic([Atom1|MoreAtoms1],Head1)
        ;   ccopy(PSIC,psic([Atom1|MoreAtoms1],Head1)) % MG 16 feb 2008: 
                                                % Mi sembra che la ccopy sia necessaria solo se
                                                % ci sono altre clausole
    ),
    (is_term_quantified(Atom1,forall)
     -> (Atom1=CHead
            ->  append(CBody,MoreAtoms1,NewAtoms),
                UnfoldedPSICS=[psic(NewAtoms,Head1)|MoreUnfoldedPSICS]
            ;   UnfoldedPSICS=MoreUnfoldedPSICS
        )
    ;   reif_unify(CHead,Atom1,B),
        (B==1 ->    append(CBody,MoreAtoms1,NewAtoms),
                    UnfoldedPSICS=[psic(NewAtoms,Head1)|MoreUnfoldedPSICS] ;
         B==0 ->    UnfoldedPSICS=MoreUnfoldedPSICS ;
        (
            (B=1,
            append(CBody,MoreAtoms1,NewAtoms),
            UnfoldedPSICS=[psic(NewAtoms,Head1)|MoreUnfoldedPSICS])
        ;
            (B=0,
            UnfoldedPSICS=MoreUnfoldedPSICS)
        ))
    ),
    get_unfolded_psics(MoreClauses,PSIC,MoreUnfoldedPSICS).
       


get_candidate_clauses(Atom,Clauses):-
    functor(Atom,F,N),
    findall(clause(Head,Body),
        (
          functor(Head,F,N),
          clause(Head,Body1),
          fn_ok(Atom,Head),
          (Body1=true->
              Body=[];
              commas_to_list(Body1,Body))
        ),
        Clauses).



impose_head1(Head):-
    quantify_unquantified(Head),
    term_variables(Head,Variables),
    flag_variables(Variables),
    (Head=[Disj]-> impose_head_disjunct(Disj) ;
     Head=[] -> fail ;
        nondeterministic(impose_head(Head))).


quantify_unquantified(Head):-
    ics_scan_head(Head,[],HV1),
    adjust_variable_list(HV1,HV),
    % No more repeated variables now (eliminated when SICS were loaded)
    quantify_unquantified_variables(HV).

quantify_unquantified_variables([]).
quantify_unquantified_variables([variable(Variable,_)|MoreVariables]):-
    get_quant(Variable,_),
    !,
    quantify_unquantified_variables(MoreVariables).
quantify_unquantified_variables([Variable|MoreVariables]):-
    decide_variable_quantification(Variable,Quantification),
    attach_variable_quantification(Variable,Quantification),
    quantify_unquantified_variables(MoreVariables).

  
%impose_head([]):- fail.
impose_head([H|_]):-
    impose_head_disjunct(H).
impose_head([_|T]):-
    impose_head(T).

impose_head_disjunct([]).
impose_head_disjunct([clp_constraint(C)|Tail]):- !,
    st(C), impose_head_disjunct(Tail).
impose_head_disjunct([Head|Tail]):-
    %Head=..[Functor|Arguments],
    %length(Arguments,NofArgs),
    %functor(Head,Functor,NofArgs),
    isabducible(Head),
    !,
    abduce(Head),
    impose_head_disjunct(Tail).
impose_head_disjunct([Head|Tail]):-
    call(Head),
    impose_head_disjunct(Tail).

% duplicated both with 2 and 3 arguments, because they might occur in both ways
isabducible(h(_,_)).
isabducible(h(_,_,_)).  
isabducible(e(_,_,_)).
isabducible(e(_,_)).
isabducible(en(_,_,_)).
isabducible(en(_,_)).
isabducible(note(_,_)).
isabducible(noten(_,_)).
isabducible(abd(_,_,_)).
isabducible(abd(_,_)).

is_SCIFF_RESERVED(noth(_,_)) :- !.
is_SCIFF_RESERVED(noth(_,_,_)) :- !.
is_SCIFF_RESERVED(X) :-
	isabducible(X).


violation @
    h(F,HEvent,HTime),
    pending(en(F,EEvent,ETime)) # _pending
    ==>
    fn_ok(HEvent,EEvent)
    |
    %ccopy(p(EEvent,ETime),p(EEvent1,ETime1)),  MA QUESTA CCOPY E` NECESSARIA?
    case_analysis_violation(F,HEvent,HTime,EEvent,ETime,_pending).
/* Old version
case_analysis_violation(HEvent,HTime,EEvent,ETime,
              EEvent1,ETime1,_pending):-
    reif_unify(p(HEvent,HTime),p(EEvent1,ETime1),1),
    remove_constraint(_pending),
    viol(en(EEvent,ETime)).
case_analysis_violation(HEvent,HTime,_,_,EEvent1,ETime1,_):-
    reif_unify(p(HEvent,HTime),p(EEvent1,ETime1),0).
*/
% New version, more efficient
case_analysis_violation(F,HEvent,HTime,EEvent1,ETime1,_):- 
    get_option(violation_causes_failure, OptFail),
    (OptFail = yes
        ->  reif_unify(p(HEvent,HTime),p(EEvent1,ETime1),0)
        ;   reif_unify(p(HEvent,HTime),p(EEvent1,ETime1),B),
            (   B=0
            ;   B=1,
                %remove_constraint(_pending),
                viol(en(F,EEvent1,ETime1))
            )
    ).





load_ics:-
    findall(ic(Head,Body),
        ics(Head,Body),
        ICSs),
    call_list(ICSs).

history:-
    history_is_empty(yes),
    !.
history:-
    findall(h(Event,Body),
        hap(Event,Body),
        History),
    set_term_quantification(History, existsf),
    call_list(History).


call_list([]).
call_list([IC|MoreICs]):-
    call(IC),
    call_list(MoreICs).


/* Abduction */



abduce(Abducible):-
    term_variables(Abducible,Variables),
    flag_variables(Variables),
    call(Abducible).

 
flag_variables([]).  
flag_variables([Var|MoreVars]):-
    get_quant(Var,Q),
    ((Q=forallf ; Q=existsf) -> true
    ;   flag_quant(Q,NewQ),
        set_quant(Var,NewQ)
    ),
    flag_variables(MoreVars).

flag_quant(exists,existsf).
flag_quant(forall,forallf).

/* old version, less efficient
flag_variables([]). 
flag_variables([Var|MoreVars]):-
    get_quant(Var,existsf),
    !,
    flag_variables(MoreVars).
flag_variables([Var|MoreVars]):-
    get_quant(Var,forallf),
    !,
    flag_variables(MoreVars).
flag_variables([Var|MoreVars]):-
    get_quant(Var,exists),
    !,
    quant(Var,existsf),
    flag_variables(MoreVars).
flag_variables([Var|MoreVars]):-
    get_quant(Var,forall),
    quant(Var,forallf),
    flag_variables(MoreVars).
*/



%MarcoG 9 may 2005
% The 1st clause used to be:
%check_unification(T1,T2,B,_,_):-
%    ccopy(p(T1,T2),p(U1,U2)),
%    reif_unify(U1,U2,B),
%    reif_unify(T1,T2,B),!.
% but in this case
% ?- existsf(U1), U1 #< P, e(un(a),U1), forallf(X), forallf(U2), st(U2,U2#<U1), st(U2,U2#>0), en(un(X),U2).
% results in X=a!!
% I only unify the copies.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Modified by Federico, 30-10-2006
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Old version:
/*


check_unification(T1,T2,B,_,_):-
    ccopy(p(T1,T2),p(U1,U2)),
    reif_unify(U1,U2,B),!.
 check_unification(T1,T2,_,S1,S2):-
    T1=..[_|A1],
    T2=..[_|A2],
    R1=..[S1|A1],
    R2=..[S2|A2],
    inconsistent(R1,R2),
    (	current_predicate(printConstraints/0)
     	->	printConstraints
     	;		true
    ),
    fail.
*/


% New Version:
% DANGER!!! This predicate is defined also in sciff_java_gui.pl
% PLEASE DO NOT MODIFY IT UNLESS YOU REALLY KNOW WHAT ARE YOU DOING!
% KEEP COHERENT THE TWO VERSIONS OF THIS PREDICATE !!!
:- chr_constraint
   inconsistent/2.

check_unification(T1,T2,B,e,note):- !,
    reif_unify(T1,T2,B).
check_unification(T1,T2,B,e,en):- !,
    ccopy(T2,U2),
    reif_unify(T1,U2,B).
check_unification(T1,T2,B,_,_):-
    ccopy(p(T1,T2),p(U1,U2)),
    reif_unify(U1,U2,B).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%



not_consistency_e @
    e(_,EEvent,ETime),
    note(NotEEvent,NotETime)
    ==>
    check_unification(p(EEvent,ETime),p(NotEEvent,NotETime),0,e,note).


not_consistency_en @
    en(_,EnEvent,EnTime),
    noten(NotEnEvent,NotEnTime)
    ==>
    check_unification(p(EnEvent,EnTime),p(NotEnEvent,NotEnTime),0,en,noten).

:- chr_constraint
	close_history/0.



/*  version SICStus 3.9
propagation_noth @
    close_history,
    psic([[],[NotH|MoreNotH],[],[],[],[],[],A],Head) # _psic
    ==>
    true
    &
    Body=[[],[NotH|MoreNotH],[],[],[],[],[],A],
    ccopy(p(Body,Head),p(Body1,Head1)),
    propagate_noth(Body1,Body2)
    |
    psic(Body2,Head1).
%    pragma
%    passive(_psic).
*/

% Version for SICStus 4. No more tell guards: Check if it is correct!!!
propagation_noth @
    close_history,
    psic([[],[NotH|MoreNotH],[],[],[],[],[],A],Head)
    ==>
    Body=[[],[NotH|MoreNotH],[],[],[],[],[],A],
    ccopy(p(Body,Head),p(Body1,Head1)),
    propagate_noth(Body1,Body2)
    |
    psic(Body2,Head1).



propagate_noth([H,NotH,E,NotE,EN,NotEN,Abd,A],
           [H,NewNotH,E,NotE,EN,NotEN,Abd,A]):-
    noth_propagation(NotH,NewNotH).

noth_propagation([NotH|MoreNotHs],NewNotH):-
    noth_success(NotH),
    !,
    noth_propagation1(MoreNotHs,NewNotH).
noth_propagation([NotH|MoreNotHs],[NotH|MoreNewNotHs]):-
    noth_propagation(MoreNotHs,MoreNewNotHs).

noth_propagation1([],[]).
noth_propagation1([NotH|MoreNotHs],NewNotH):-
    noth_success(NotH),
    !,
    noth_propagation1(MoreNotHs,NewNotH).
noth_propagation1([NotH|MoreNotHs],[NotH|MoreNewNotHs]):-
    noth_propagation1(MoreNotHs,MoreNewNotHs).

noth_success(noth(Event,Time)):-
    universal_variables_in_term(noth(Event,Time),UnivVariables),
    (UnivVariables=[] ->
        \+(has_happened(Event,Time));
        universal_variables_happened(Event,Time,TermList), % In realta` il D8 dice che 
        % dovrei rendere universali tutte le variabili, escluse le esistenziali non flagged. 
        PUniv=..[p|UnivVariables],
        % Qui devo rendere flagged tutte le variabili che sono universali (in teoria tutte escluse le exist non flagged)
        flag_variables(UnivVariables),
        impose_noth_not_unif(TermList,PUniv)).

impose_noth_not_unif([],_).
impose_noth_not_unif([Term|MoreTerms],PUniv):-
    set_restriction(reified_unif:reif_unify(Term,PUniv,0)),
    %reif_unify(Term,PUniv,0),
    impose_noth_not_unif(MoreTerms,PUniv).

universal_variables_in_term(Term,UnivVariables):-
    term_variables(Term,Vars),
    keep_universals(Vars,UnivVariables).

keep_universals([],[]).
keep_universals([Var|MoreVars],[Var|MoreUnivVars]):-
    is_universal(Var),
    !,
    keep_universals(MoreVars,MoreUnivVars).
keep_universals([_|MoreVars],UnivVars):-
    keep_universals(MoreVars,UnivVars).

universal_variables_happened(Event,Time,TermList):-
    findall(Term,
        (
          ccopy(p(Event,Time),p(Event1,Time1)),
          universal_variables_in_term(p(Event1,Time1),UnivVars),
          has_happened(Event1,Time1),
          Term=..[p|UnivVars]
          ),
        TermList).

has_happened(Event,Time):-
    find_constraint(h(_,Event,Time),_).

%% COMPLIANT HISTORY GENERATION: 20 JUL 04

/* versione MarcoA
fulfiller1 @
    close_history,
    pending(e(Event,Time))
    ==>
%    write('Inserted '),write(h(Event,Time)),nl,
  %  write_history,
    h(Event,Time).
*/

pending_e @
    e(F,Event,Time)
    ==>
    pending(e(F,Event,Time)).

%----------------------------------------------------------
% FULFILLMENT RULES
%----------------------------------------------------------
%new fdet version
fulfillment @
    h(F,HEvent,HTime),
    pending(e(F,EEvent,ETime)) # _pending
    ==>
    fn_ok(HEvent,EEvent)
    |
    %ccopy(p(EEvent,ETime),p(EEvent1,ETime1)), Non necessary: all variables existentially quant.
    case_analysis_fulfillment(F,HEvent,HTime,EEvent,ETime,_pending).

case_analysis_fulfillment(F,HEvent,HTime,EEvent,ETime,_):-
    % HEvent=EEvent, HTime=ETime,
    % If we use unification, it triggers all the CHR constraints involving the variables
    % before terminating the execution. With g-SCIFF, it will trigger fulfiller before
    % removing the pending expectation. Better use reif_unify.
    % 4 Aug 07: Actually even with reif_unify fulfiller is triggered too early.
    % Let us anticipate remove_constraint
    %remove_constraint(_pending),
    %term_unify(HEvent,EEvent),
    %eq(HTime,ETime),
    reif_unify(p(HEvent,HTime),p(EEvent,ETime),1),
    (
    	fdet(e(Term,Time)),
    	subsumeschk(e(Term,Time),e(EEvent,ETime))
    ->
    	!
    ;
    	true
    ),
    fulf(e(F,EEvent,ETime)).
case_analysis_fulfillment(_,HEvent,HTime,EEvent1,ETime1,_):-
    reif_unify(p(HEvent,HTime),p(EEvent1,ETime1),0).


fulfillment_allows @
    h(F,do(HX,HRec,HAction,HD),HT),
    pending(e(F,do(Expecter,EX,ERec,EAction,ED),ET)) # _pending
    ==>
    fn_ok(p(do(HX,HRec,HAction,HD),HT),p(do(EX,ERec,EAction,ED),ET))
    |
    %ccopy(p(EEvent,ETime),p(EEvent1,ETime1)), Non necessary: all variables existentially quant.
    case_analysis_fulfillment(F,do(Expecter,HX,HRec,HAction,HD),HT,do(Expecter,EX,ERec,EAction,ED),ET,_pending).

/*
fulfillment @
    h(HEvent,HTime),
    pending(e(EEvent,ETime)) # _pending
    ==>
    fn_ok(HEvent,EEvent)
    |
    %ccopy(p(EEvent,ETime),p(EEvent1,ETime1)), Non necessary: all variables existentially quant.
    case_analysis_fulfillment(HEvent,HTime,EEvent,ETime,_pending).

case_analysis_fulfillment(HEvent,HTime,HEvent,HTime,_pending):-
    remove_constraint(_pending),
    %reif_unify(p(HEvent,HTime),p(EEvent,ETime),1),
    (sciff_option(fdet,on)->!;true),
    fulf(e(EEvent,ETime)).
case_analysis_fulfillment(HEvent,HTime,EEvent1,ETime1,_):-
    reif_unify(p(HEvent,HTime),p(EEvent1,ETime1),0).
*/


/* versione MarcoG */
fulfiller1 @
    (close_history)
    \
    (pending(e(F,Event,Time)))
    <=>
%        write('Inserted '),write(h(Event,Time)),
    sciff_option(fulfiller,on)
    %findall_constraints(nondeterministic(_),[]) bug fix: fulfilment does not use nondeterinistic
    |
    fulf(e(F,Event,Time)),
    h(F,Event,Time),
    %%%MARCOM
    writeln(h(Event,Time)).

%Constraints used by AlLoWS
:- chr_constraint
	gen_phase/0, end_gen_phase/0, remove_exp/0.

fulfiller_rationality @
    (gen_phase) \
    pending(e(F,do(X,X,Rec,Action,D),T))
    <=>
    %sciff_option(fulfiller_rationality,on) |
    fulf(e(F,do(X,X,Rec,Action,D),T)),
    h(F,do(X,Rec,Action,D),T).

fulfiller_chor @
    (gen_phase),
    pending(e(F,do(chor,X,Rec,Action,D),T)) % # _pending
    ==>
    %sciff_option(fulfiller_rationality,on) |
    testing(WS), set_term_quantification(WS,existsf),
    reif_unify(WS,X,Bool),
    (Bool=0;Bool=1),
    (Bool=0
      ->    %remove_constraint(_pending),
            fulf(e(F,do(chor,X,Rec,Action,D),T)),
            h(F,do(X,Rec,Action,D),T)
      ;     true).

end_gen_phase @
    end_gen_phase \
    gen_phase <=> true.

write_history:-
    %findall_constraints(h(send(_,_,_,_),_),L), MarcoG: why only send?
    findall_constraints(h(_,_,_),L),
    print_chr_list(L,'\n').

write_normal_abducibles:-
		findall_constraints(abd(_,_,_),L),
    print_chr_list(L,'\n').

write_positive_expectations:-
		findall_constraints(e(_,_,_),L),
    print_chr_list(L,'\n').

write_violations:-
		findall_constraints(viol(_,_,_),L),
    print_chr_list(L,'\n').

write_events_not_expected:-
		findall_constraints(not_expected(_,_,_),L),
    print_chr_list(L,'\n').

/*
closure_e @
    (close_history)
    \
    (pending(e(Event,Time)) # _pending)
    <=>
    viol(e(Event,Time))
    pragma
    passive(_pending).
*/


closure_e @
    (close_history),
    (pending(e(F,Event,Time)) ) %# _pending)
    ==>
    true | % this guard has been added to avoid a mis-interpretation of the chr compiler
    (get_option(violation_causes_failure, yes)
    		->	fail
    		; 	(%remove_constraint(_pending),
    				 viol(e(F,Event,Time))
    				)
    ).
    %pragma passive(_pending). Does not work with violation_causes_failure -> no

/*
closure_e @
    (close_history)
    \
    (pending(e(Event,Time)) # _pending)
    <=>
    get_option(violation_causes_failure, no)
    |
    viol(e(Event,Time))
    pragma passive(_pending).
*/

:- chr_constraint
	not_expected/1.


not_expected_gen @
		(h(F,HEvent,HTime))
		==>
		sciff_option(allow_events_not_expected, no)
		|
		not_expected(h(F,HEvent,HTime)).



not_expected_remove @
		fulf(e(F,Event, Time))
		\
		not_expected(h(F,Event, Time))
		<=>
		true.

% If an event is expected both by the WS and the Chor,
% then it is no longer not_expected
not_expected_remove_allows1 @
		(fulf(e(F,do(chor,EX,ERec,EAction,ED),ET)),
		fulf(e(F,do(WS,EX,ERec,EAction,ED),ET)))
		\
		not_expected(h(F,do(EX,ERec,EAction,ED),ET))
		<=> testing(WS) |
		true.

% If an event is expected only by the choreography,
% and it does not involve the WS under test, then
% the event is expected
not_expected_remove_allows2 @
		fulf(e(F,do(chor,EX,ERec,EAction,ED),ET))
		\
		not_expected(h(F,do(EX,ERec,EAction,ED),ET))
		<=> %write('******** TRYING ***************'),
            testing(WS), nonvar(EX), EX \= WS, nonvar(ERec), ERec \= WS |
		true.


% violation is imposed only if the corresponding flag is set to true
protocol_e @
		(close_history) \
    (not_expected(h(F,Event,Time)) # _not_expected)
    <=>
    true %added to avoid a possible chr bug
    |
    (	get_option(violation_causes_failure, yes)
    	->	fail
    	;		%remove_constraint(_not_expected),
    			viol(not_expected(h(F,Event,Time)))
    )
    pragma passive(_not_expected).
    

% End Modification
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


closure_en @
    (close_history)
    \
    (pending(en(F,Event,Time)) # _pending)
    <=>
    fulf(en(F,Event,Time))
    pragma
    passive(_pending).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% MODIFIED BY FEDERICO
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Removed because of an optimization introduced by MarcoG
% If violation causes failure then failure is imposed immediately
% without adding the chr_constraint viol(_).
% Otherwise the chr_constraint viol(_) is imposed, and no failment is imposed.
%
% Violations are generated by the following chr_rules:
% - case_analysis_violation (EN with a corresponding H)
% - closure_e (close_history, and E without H)
% - ct_time_constraint (E and due to the current_time, no H is possible anymore)
% - protocol_e (H without E)
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
/*
failure_for_violation @
    viol(_)
    ==>
    (	current_predicate(printConstraints/0)
     	->	printConstraints
     	;		true
    ),
   get_option(violation_causes_failure, no).
   */
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%






%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% CURRENT TIME MANAGEMENT
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
:- chr_constraint
    current_time/1.

current_time_update @
    (h(_,current_time,CT))
    \
    (current_time(_OldCT) # _current_time)
    <=>
    current_time(CT)
    pragma
    passive(_current_time).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Modified by Federico, 20061102
%
% Original version:
/*
ct_time_constraint @
    current_time(CT),
    pending(e(Event,Time)) # _pending
    ==>
    impose_time_constraint(Time,CT)
    pragma
    passive(_pending).

constraints
    gt_current_time/2.

impose_time_constraint(Time,CT):-
    Time #>= CT,
    !.
impose_time_constraint(Time,CT):-
    gt_current_time(Time,CT),
    (	current_predicate(printConstraints/0)
     	->	printConstraints
     	;		true
    ),
    fail.
*/

ct_time_constraint @
    current_time(CT),
    pending(e(F,Event,Time)) # _pending
    ==>
    impose_time_constraint(Time,CT, e(F,Event,Time), _pending)
    pragma
    passive(_pending).

impose_time_constraint(Time,CT, e(F,Event,Time), _):-
    ( geq(Time,CT)
    	->	true
    	;		( get_option(violation_causes_failure, yes)
    				->	fail
    				;	%remove_constraint(_pending),	
                        viol(gt_current_time(e(F,Event,Time), failed_to_impose_greater_than(Time, CT)))
    			)
    ).


%end @ phase(deterministic) <=> findall_constraints(nondeterministic(_),[]) | true.
switch2nondet @ phase(deterministic) <=> phase(nondeterministic).
/*switch2det @ phase(nondeterministic) \ nondeterministic(G) <=>
    call(G).
    %phase(deterministic).*/

switch2det @ phase(nondeterministic) , nondeterministic(G) <=>
    call(G),
    phase(deterministic).


remove_phase \ phase(_) <=> true.
remove_phase <=> true.

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



build(SOKB,ICS,History):-
   translate_sokb(SOKB,'./sokb.pl'),
    translate_ics(ICS,'./ics.pl'),
    translate_history(History,'./history.pl').

build(ExampleName):-
    atom_concat(ExampleName,'/',A1),
    atom_concat(A1,ExampleName,A2),
    atom_concat(A2,'_sokb.pl',SOKB),
    atom_concat(A2,'_ics.txt',ICS),
    atom_concat(A2,'_history.txt',History),
    build(SOKB,ICS,History).
build(ExampleName,SubExample):-
    atom_concat(ExampleName,'/',A1),
    atom_concat(A1,ExampleName,A2),
    atom_concat(A2,'_sokb.pl',SOKB),
    atom_concat(A2,'_ics.txt',ICS),
    atom_concat(A2,'_history_',A3),
    atom_concat(A3,SubExample,A4),
    atom_concat(A4,'.txt',History),
    build(SOKB,ICS,History).

build1(ExampleName):-
    atom_concat('../examples/',ExampleName,A0),
    atom_concat(A0,'/',A1),
    atom_concat('../protocols/',ExampleName,B0),
    atom_concat(B0,'/',B1),
    atom_concat(A1,ExampleName,A2),
    atom_concat(B1,ExampleName,B2),
    atom_concat(B2,'_sokb.pl',SOKB),
    atom_concat(B2,'_ics.txt',ICS),
    atom_concat(A2,'_history.txt',History),
    build(SOKB,ICS,History).
build1(ExampleName,SubExample):-
    atom_concat('../examples/',ExampleName,A0),
    atom_concat(A0,'/',A1),
    atom_concat('../protocols/',ExampleName,B0),
    atom_concat(B0,'/',B1),
    atom_concat(B1,ExampleName,B2),
    atom_concat(A1,ExampleName,A2),
    atom_concat(B2,'_sokb.pl',SOKB),
    atom_concat(B2,'_ics.txt',ICS),
    atom_concat(A2,'_history_',A3),
  
    atom_concat(A3,SubExample,A4),
    atom_concat(A4,'.txt',History),
    build(SOKB,ICS,History).

build2(ExampleName):-
    atom_concat('../examples/',ExampleName,A0),
    atom_concat(A0,'/',A1),
    atom_concat('../protocols/',ExampleName,B0),
    atom_concat(B0,'/',B1),
    atom_concat(A1,ExampleName,_A2),
    atom_concat(B1,ExampleName,B2),
    atom_concat(B2,'_sokb.pl',SOKB),
    atom_concat(B2,'_ics.txt',ICS),
    build3(SOKB,ICS).
  
build3(SOKB,ICS):-
   translate_sokb(SOKB,'./sokb.pl'),
    translate_ics(ICS,'./ics.pl').
/*
 
:- dynamic(numero_soluzioni/1).
 
conta_soluzioni :-
    retractall(numero_soluzioni(X)),
    assert(numero_soluzioni(0)),
    run,
    numero_soluzioni(N),
    N1 is N + 1,
    write('trovata una soluzione ('),write(N1),write(')'),nl,
    retract(numero_soluzioni(N)),
    assert(numero_soluzioni(N1)),
    fail.
  */
run:-
    load_ics,
    current_time(0),
    society_goal,
    history,
    phase(deterministic),
    close_history.

run_no_close:-
    load_ics,
    current_time(0),
    society_goal,
    history,
    phase(deterministic).

try_number(0).
try_number(X):-
    try_number(Y),
    X is Y+1,
    max_bound(B),
    X < B.

iterative_deepening(Goal):-
    try_number(Depth),
    write('***************'), writeln(depth(Depth)),
    max_depth(Depth),
    call(Goal).

iter:-
    init_graph('proof.dot',_Stream),
    statistics(runtime,_),
    load_ics,
    iterative_deepening(
        (society_goal,
        history,
        phase(deterministic),
        once((
            write('grounding time\n'),  
            ground_time,
            write('grounding 1\n'),
            make_choice
            
            ))
        )),
    statistics(runtime,[_,Time]),
    writeln(runtime(Time)).

iter_gsciff:-
    init_graph('proof.dot',_Stream),
    statistics(runtime,_),
    load_ics,
    society_goal,
    N in 0..1000,
    indomain(N), write('************************* new happen ******************************'),
        writeln(N),
    add_history_el(N),
    phase(deterministic),
    close_history,
    write('grounding\n'),
    make_choice,
    statistics(runtime,[_,Time]),
    writeln(runtime(Time)).

iter_gsciff_hist:-
    init_graph('proof.dot',_Stream),
    statistics(runtime,_),
    load_ics,
    society_goal,
    history,
    phase(deterministic),
    N in 0..1000,
    indomain(N), write('************************* new happen ******************************'),
        writeln(N),
    add_history_el_sym(N,_),
    close_history,
    statistics(runtime,[_,Time]),
    writeln(runtime(Time)).


% Questo predicato e` per verificare la proprieta` delle aste combinatorie:
% "Esiste un insieme di bid t.c. io ottengo uno solo fra i due elementi 1 e 2?"
% E` da raffinare, questo e` solo uno sketch di come si potrebbe fare.
iter_gsciff_auction:-
    statistics(runtime,_),
    load_ics,
    society_goal,
    N in 0..1000,
    indomain(N), write('************************* new happen ******************************'),
        writeln(N),
    add_history_el(N),
    \+((
        e(deliver(_Item1)), e(deliver(_Item2))
      )),
    close_history,
    statistics(runtime,[_,Time]),
    writeln(runtime(Time)).

% Qual e` la bid che devo fare per vincere, sapendo che
% 1. voglio minimizzare la cifra che pago
% 2. ipotizzo che l'altro faccia una bid di 5
% 3. io voglio pagare al massimo 10
best_bid(Bid):-
    statistics(runtime,_),
    load_ics,
    history,
    Price in 0..10,
            existsf(Bid), existsf(Tbid),
            e(tell(i,auc,bid(i1,Bid),auction1),Tbid),
            existsf(Price), existsf(Tpay),
            e(tell(i,auc,pay(Price),auction1),Tpay),
            add_history_el(2), make_choice,
    minimize(
        (   % Metto esplicitamente il society goal, perche' altrimenti
            % non posso accedere alle variabili

            indomain(Price),
            close_history, write(Price), nl
        )
        ,Price),
    statistics(runtime,[_,Time]),
    writeln(runtime(Time)).

% Explanation in help.pl
min_viol_closed(Num,OutList):-
    max_viol(Num),
    minimize(
        (   load_ics,
            society_goal,
            history,
            close_history,
            indomain(Num),
            findall_constraints(_,OutList)
        ),Num).


% Explanation in help.pl
min_viol_open(Num,OutList):-
    max_viol(Num),
    minimize(
        (   load_ics,
            society_goal,
            history,
            indomain(Num),
            findall_constraints(_,OutList)
        ),Num).

get_ics_quantified(PSICs):-
    findall(ic(Head,Body),
        ics(Head,Body),
        ICSs),
    convert_to_psic_list(ICSs,PSICs).

convert_to_psic_list([],[]).
convert_to_psic_list([IC|ICs],[PSIC|PSICs]):-
    convert_to_psic(IC,PSIC),
    convert_to_psic_list(ICs,PSICs).

allows(Param):-
    (var(Param) -> Param = false ; true), % Default behaviour: fail if not conformant
    % load_ics, I re-write the impose_ics because I don't want to redo it for
    %           each possible history (since it is expensive), so I redo only
    %           the necessary parts
    get_ics_quantified(PSICs),
    call_list(PSICs),
    %current_time(0),
    gen_phase,  % activates rationality
    history,
    society_goal,
    phase(deterministic),
    end_gen_phase,  % deactivates rationality, backtrackable
    (Param = verbose -> nl, writeln_debug('Trying history'),
    										write_history, write_normal_abducibles,
    										write_positive_expectations,
    										write_violations,
    										write_events_not_expected
        ;   true),
    (remove_exp,
     society_goal, % reactivate ics, doing a SCIFF (no g-SCIFF) computation
     %load_ics,
     %phase(deterministic), MG: Adding this (together with remove_phase) performs
                % stronger reasoning. However, in some instances
                % it can slow down very much the computation.
                % Better perform stronger reasoning in the early stages (generate)
                % and faster in other stages. Remember that in the first stages
                % we look for all solutions (where deterministic checking is
                % useful), while in the second we look for one solution
     call_list(PSICs),
     
     close_history
     -> fail   % causes backtracking
      ; writeln_debug('AlLoWS failed: no fulfilment for possible history'),nl,
        (get_option(sciff_debug, on) -> write_history,write_normal_abducibles ; true), 
        !, Param=true % deep failure
    ).
allows(_):-
    writeln_debug('AlLoWS succeded: all possible histories compliant'),
    (get_option(allow_events_not_expected, yes)
      ->    writeln_debug('Feeble conformance proven')
      ;     writeln_debug('Strong conformance proven')
    ).


remove_exp_pending @ remove_exp \ pending(_) <=> true.
remove_exp_e  @ remove_exp \ e(_,_,_) <=> true.
remove_exp_en @ remove_exp \ en(_,_,_) <=> true.
remove_exp_fulf @ remove_exp \ fulf(_) <=> true.
remove_exp_ic @ remove_exp \ ic(_,_) <=> true.
remove_exp_psic @ remove_exp \ psic(_,_) <=> true.
%remove_exp_en @ remove_exp \ not_expected(_) <=> true.
end_remove_exp @ remove_exp <=> true.

%iter_gsciff_vickrey:-
%    statistics(runtime,_),
%    load_ics,
%    society_goal,
%    N in 0..1000,
%    indomain(N), write('************************* new happen ******************************'),
%        writeln(N),
%    add_history_el(N),
%    close_history,
%    statistics(runtime,[_,Time]),
%    writeln(runtime(Time)).

add_history_el:-
    existsf(X), existsf(T),
    h(X,T).
add_history_el:-
    existsf(X), existsf(T),
    h(X,T), writeln('************************* new happen ******************************'),
    add_history_el.

add_history_el(0):- !.
add_history_el(N):-
    existsf(X), existsf(T),
    h(X,T),
    N1 is N-1,
    add_history_el(N1).

% generates N happened events ordered in time
add_history_el_sym(0,_):- !.
add_history_el_sym(N,T1):-
    existsf(X), existsf(T),
    h(X,T), T in 0..1000, T #=< T1,
    N1 is N-1,
    add_history_el_sym(N1,T).


proof:-
    init_graph('proof.dot',_Stream),
    statistics(runtime,_),
    load_ics,
    society_goal,
    history,
    once((
        write('grounding time\n'),  
        ground_time,
        write('grounding 1\n'),
        make_choice,
        true
        )),
    statistics(runtime,[_,Time]),
    writeln(runtime(Time)).


test(Pred,Mem,Time):-
    statistics(walltime,[T1,_]),
    call_always_success(Pred),
    statistics(walltime,[T2,_]),
    Time is T2 - T1,
    statistics(memory,[Mem,_]).
  
call_always_success(Pred):-
    call(Pred),
    !.
call_always_success(_).




clp_constraint(A):-
    call(A).


:- chr_constraint
	cug/1.
cug(X) <=> ground(X)|call(X).




/*
constraints novis/0.

firstfail @
    e(X1,T1), e(X2,T2), ground_time
    ==> fd_var(T1), fd_var(T2), fd_size(T1,S1), fd_size(T2,S2), S1<S2 |
        write(size(S1)),
        indomain(T1).

novisual @ ground_time, novis,
    e(X,T) ==> fd_var(T) | T in -1000..1000, indomain(T).      

visual @ e(X,T), ground_time
    ==> fd_var(T) |  T in -1000..1000,
    fd_min(T,Min),fd_max(T,Max), write(T in Min..Max), indomain(T), nl,
write(T), novis.
*/

:- chr_constraint all_e/1, get_list_e/1.

e(F,X,T) \ all_e(L) <=> notmember(e(F,X,T),L) | all_e([e(F,X,T)|L]).

all_e(L1), get_list_e(L2) <=> L1=L2.

findall_e(L):-
    all_e([]), get_list_e(L), !.

notmember(_,[]).
notmember(A,[H|_]):- A==H, !, fail.
notmember(A,[_|T]):- notmember(A,T).

% MG 9 Feb 2008: I don't use the findall_constraints implemented in my_chr_extensions,
% because it does not retain the variables (it is due to the implementation of
% findall in SICStus)
ground_time:- 
    findall_e(L),
    get_time(L,LT),
    solver_search(LT).

get_time([],[]).
get_time([e(_,_,T)|R],[T|RT]):-
    add_default_domain(T),
    get_time(R,RT).
    


build_and_run(SOKB, ICS, History, noclose) :-
	build(SOKB, ICS, History),
	consult(sokb),
	use_module(history),
	use_module(ics),
	run_no_close.

build_and_run(SOKB, ICS, History, close) :-
	build(SOKB, ICS, History),
	consult(sokb),
	use_module(history),
	use_module(ics),
	run.

project(Project):-
   default_dir(Dir),
   atom_concat(Dir,Project,Path),
   atom_concat(Path,'/',PathSlash),
   retractall(prjDir(_)),
   assert(prjDir(PathSlash)),
   atom_concat(PathSlash,'project.pl',PrjFile),
   compile(PrjFile),
   build_prj(PathSlash).

append_path(_,[],[]):- !.
% If the file is actually a URL, do not change it
append_path(Path,[File|Rest],[FullPath|Rest1]):-
    atom_concat('http://',_,File),!,FullPath=File,
    append_path(Path,Rest,Rest1).
append_path(Path,[File|Rest],[FullPath|Rest1]):-
    atom_concat(Path,File,FullPath),
    append_path(Path,Rest,Rest1).

convert_sokb([],_).
convert_sokb([SOKB|Rest],File):-
    write_debug('Parsing file '), write_debug(SOKB),
    translate_sokb(SOKB,File,write), % for the 1st, write, the others are in append
    writeln_debug(' --> OK'),
    convert_sokb1(Rest,File).
convert_sokb1([],_).
convert_sokb1([SOKB|Rest],File):-
    write_debug('Parsing file '), write_debug(SOKB),
    translate_sokb(SOKB,File,append),
    writeln_debug(' --> OK'),
    convert_sokb1(Rest,File).
    
/*
build(SOKB,ICS,History):-
   translate_sokb(SOKB,'./sokb.pl'),
    translate_ics(ICS,'./ics.pl'),
    translate_history(History,'./history.pl').

build(ExampleName):-
    atom_concat(ExampleName,'/',A1),
    atom_concat(A1,ExampleName,A2),
    atom_concat(A2,'_sokb.pl',SOKB),
    atom_concat(A2,'_ics.txt',ICS),
    atom_concat(A2,'_history.txt',History),
    build(SOKB,ICS,History).
*/