/********************************/
/*       Indigo Executor        */
/*        version 1.0.1         */
/*         January 1996         */
/*      (c) Roman Bart‡k        */
/********************************/

% implements executing phase of the constraint hierarchy solver
% based on interval arithmetics from the Indigo algorithm
% consult GCP.pr and InterArithmetics.pr before
%  usage: ?-execute.

tighten(A,B,C,R):-
  A=ALÉAU,B=BLÉBU,
  (lt(AU,BL) -> C=AUÉAU ;
   lt(BU,AL) -> C=ALÉAL ;
                intersection(A,B,C)),
  (A=C -> R=no ; R=yes).

eval(A+B,C):-
  eval(A,EA),eval(B,EB),plus(EA,EB,C).
eval(A-B,C):-
  eval(A,EA),eval(B,EB),minus(EA,EB,C).
eval(A*B,C):-
  eval(A,EA),eval(B,EB),times(EA,EB,C).
eval(A/B,C):-
  eval(A,EA),
  (number(B) -> true ; print('division error'),nl,fail),
  num_divide(EA,B,C).
eval(N,NÉN):-
  number(N).
eval(V,I):-
  atom(V),
  (val(V,I) ; I= -inf É +inf),!.

normalize(Ex,V,NOp,Norm):-
  Ex=..[Op,A,B],
  extr_var(A,V,CoefA,RestA),
  extr_var(B,V,CoefB,RestB),
  eval(CoefA-CoefB,Coef),
  ((Coef=DÉD , D\=0) -> true ; print('error in division'),nl,fail),
  (D=1 -> Norm=RestB-RestA ; Norm=(RestB-RestA)/D),
  (D<0 -> switch_oper(Op,NOp) ; NOp=Op).

switch_oper('=','=').
switch_oper('=<','>=').
switch_oper('>=','=<').

extr_var(A+B,V,CoefA+CoefB,RestA+RestB):-
  extr_var(A,V,CoefA,RestA),
  extr_var(B,V,CoefB,RestB).
extr_var(A-B,V,CoefA-CoefB,RestA-RestB):-
  extr_var(A,V,CoefA,RestA),
  extr_var(B,V,CoefB,RestB).
extr_var(A*B,V,CoefA*RestB+CoefB*RestA,RestA*RestB):-
  extr_var(A,V,CoefA,RestA),
  extr_var(B,V,CoefB,RestB),
  eval(CoefA*CoefB,I),
  (I=0É0 -> true ; print('non-linear expression'),nl,fail).
extr_var(V,V,1,0).
extr_var(V1,V,0,V1):-
  atom(V1), V1\=V.
extr_var(N,V,0,N):-
  number(N).

comp(X,Op,Ex,R):-
  eval(Ex,EV),EV=LÉU,eval(X,I),
  (Op='='    -> tighten(I,EV,NI,R) ;
   Op='=<'   -> tighten(I,-infÉU,NI,R) ;
   Op='>='   -> tighten(I,LÉ +inf,NI,R) ;
                print('>>error operation'-Op),nl),
  set_val(X,NI).

comp_var(V,Fnc,R):-
  normalize(Fnc,V,Op,Ex),comp(V,Op,Ex,R).

comp_var_list([V|T],Fnc,NVs):-
  comp_var(V,Fnc,R),
  (R=yes -> NVs=[V|NT] ; NVs=NT),
  comp_var_list(T,Fnc,NT).
comp_var_list([],_,[]).

set_val(V,I):-
  (retract(val(V,_)) ; true),
  assert(val(V,I)),!.

show_vals:-
  val(V,I),
  nl,print(V=I),fail.
show_vals:-nl.

clear_vals:-
  retractall(val(_,_)).

exec_plan(List):-
  clear_vals,
  propagate(List),
  show_vals.

propagate([V-C|T]):-
  comp_var(V,C,_),
  propagate(T).
propagate([]).

execute:-
  clear_vals,
  retractall(visited(_)),
  retractall(usat(_)),
  traverse_net,
  show_vals.

traverse_net:-
  next_covered(ID),!,
  exec_node(ID),
  traverse_net.
traverse_net.

next_covered(ID):-
  c(ID,In,_,_),
  not visited(ID),
  visited_list(In).
visited_list([H|T]):-
  visited(H),
  visited_list(T).
visited_list([]).

exec_node(ID):-
  c(ID,_,_,C),
  ((C=V-v;C=V-_-gv)              -> set_val(V,-infÉ +inf) ;
    C=(_,_,[V],[Fnc],_)-_-f      -> comp_var(V,Fnc,_) ;
    C=(_,Consts)-_-t             -> eval_geners([],Consts);
    C=(_,_,OutVs,Consts,_)-_-g   -> eval_geners(OutVs,Consts);
     fail),  % unknown node
  assert(visited(ID)),
  set_usat(ID).

set_usat(ID):-  % decides whether the node is uniquely satisfiable
  c(ID,_,_,C),
  retractall(usat(ID)),
  (is_unique(C) -> assert(usat(ID)) ; true),!.

is_unique(_-v).
is_unique(_-_-gv).
is_unique((Vs,_)-_-t):-
  Vs=[_] ; unique_vars(Vs).
is_unique((_,InVs,OutVs,_,_)-_-_):-
  InVs=[],OutVs=[_] ; unique_vars(InVs),unique_vars(OutVs).

unique_vars([V|T]):-
  val(V,AÉA),
  unique_vars(T).
unique_vars([]).

eval_geners(OutVs,[C|Cs]):-
  generate(OutVs,C),
  eval_geners(OutVs,Cs).
eval_geners(_,[]).

generate(OutVs,Const):-
  collect_vars(Const,[],Vs),
  minus(Vs,OutVs,Vs2,Vs1),
  comp_var_list(Vs1,Const,_),         % evaluate output variables
  comp_var_list(Vs2,Const,ChangedVs), % re-evaluate input variables
  propagate_changes(ChangedVs,[]),!. % propagate changes of input variables throught net

propagate_changes([V|Vs],Finished):-
  recomp_var(V,Vs,Finished,NVs),
  propagate_changes(NVs,[V|Finished]).
propagate_changes([],_).

recomp_var(V,NextVs,Finished,Vs):-
  collect_var_const(V,ConstsList),
  reexec_consts(ConstsList,[V|Finished],NextVs,Vs).

collect_var_const(V,List):-
  v(V,ID,_),
  c(ID,_,Out,C),                   % node that determinates variable V
  find_out_star(Out,V,ID,Cells,_), % find nodes which uses variable V as input
  extr_consts([ID|Cells],V,List),!.

extr_consts([ID|T],V,L):-
  c(ID,_,_,C),
  ((usat(ID) ; not visited(ID))        -> L=TL ;
   (C=(_,Cs)-_-t ; C=(_,_,_,Cs,_)-_-_) -> choose_touched_consts(Cs,V,TL,L)
                                        ; fail), % unknown node
  extr_consts(T,V,TL).
extr_consts([],_,[]).

choose_touched_consts([C|R],V,L,NL):-
  collect_vars(C,[],Vs),
  (mem(V,Vs) -> AL=[C-Vs|L] ; AL=L),
  choose_touched_consts(R,V,AL,NL).
choose_touched_consts([],_,L,L).

reexec_consts([C-CVs|T],Finished,Vs,NVs):-
  minus(CVs,Finished,RecompVs,_),
  comp_var_list(RecompVs,C,ChangedVs),
  add_list(ChangedVs,Vs,AVs),
  reexec_consts(T,Finished,AVs,NVs).
reexec_consts([],_,Vs,Vs).