/* A constraint solver implemented in B-Prolog for CPAI'08 Solver Competition */
/* by Neng-Fa Zhou, 2006, 2007, 2008, 2009                                         */
/* Version 7.2                                                         */

:-op(1050,xfy,':').  % needed for version B-Prolog 7.4 and up

main:-
    writeln('c bpsolver version 6.29.2009'),
    get_main_args(L),
    process_args(L,BaseName,TimeLimit),
    catch(convert_solve(BaseName,TimeLimit),Exception,writeln(Exception)).

process_args([BaseName,TimeLimit|_],BaseName1,TimeLimit1):-true :
    BaseName1=BaseName,
    atom_codes(TimeLimit,Codes),
    number_codes(Limit,Codes),
    (integer(Limit)->TimeLimit1 is Limit*1000; 
     format("Wrong time limit",[]),
     halt).
process_args([BaseName],BaseName1,TimeLimit1):-true :
    BaseName1=BaseName,
    TimeLimit1 is 1800000.
process_args(_Args,_InFile,_TimeLimit):-format("usage: solver FileName ~n",[]),halt.

/****************************************************************/
ec(support1(Tuple),CompVars,_Neqs):- true :
    CompVars=Tuple.
ec(support(Arity,Mins,Maxs,BigTrie,Tries),CompVars,_Neqs):- true :
    constr_scope_tuple(Arity,CompVars),
    $cfd_var_in(Arity,CompVars,Mins,Maxs,BigTrie,Tries).
ec(conflict(_Arity,[],_),_CompVars,_Neqs):- true : true.
ec(conflict(Arity,Tuples),CompVars,Neqs):- Arity=2 ?
    $eq_rel(Tuples,Min,Max),
    CompVars=t(V1,V2),
    domain_min_max(V1,Min1,Max1),
    domain_min_max(V2,Min2,Max2),
    Min1>=Min,Min2>=Min,Max1=<Max,Max2=<Max,!,
    constr_scope_tuple(Arity,CompVars),
    attach(V1 #\= V2,Neqs).
ec(conflict(Arity,Tuples),CompVars,_Neqs):- true :
    constr_scope_tuple(Arity,CompVars),
    $cfd_var_notin(Arity,CompVars,Tuples).

$eq_rel([t(E,E)|Tuples],Min,Max):-true : 
    Min=E,
    Next is E+1,
    $eq_rel_aux(Tuples,Next,Max).

$eq_rel_aux([t(E,E)],E,Max):-true : Max=E.
$eq_rel_aux([t(E,E)|Tuples],E,Max):-true : 
    Next is E+1,
    $eq_rel_aux(Tuples,Next,Max).

/****************************************************************/
:-include('c:/solvers/09/convert.pl').
convert_solve(BaseName,TimeLimit):-
    xcsp2pl(BaseName),
    solve(BaseName,TimeLimit).

solve(BaseName):-
%    solve(BaseName,1800000).
    solve(BaseName,600000).

t(BaseName):-
    atom_codes(BaseName,String),
    append(String,".pl",String2),
    atom_codes(InFile,String2),
    (exists(InFile)->true;format("File not found:~w~n",[InFile]),halt),
    see(InFile),
    read((csp(Vars):-Body)),
    seen,
    cputime(Start),
    statistics(backtracks,B0), 
    execute_body(Body),
    (labeling(Vars)->Res=suc(Vars);Res=fail),
    statistics(backtracks,B1),
    cputime(End),
    Time is End-Start,
    writeln(Res),
    B is B1-B0,
    format("~nc Time: ~w ~nBacktracks:~w~n~n",[Time,B]),!.

tall(BaseName):-
    atom_codes(BaseName,String),
    append(String,".pl",String2),
    atom_codes(InFile,String2),
    (exists(InFile)->true;format("File not found:~w~n",[InFile]),halt),
    see(InFile),
    read((csp(Vars):-Body)),
    seen,
    execute_body(Body),
    labeling(Vars),
    writeln(Vars),fail.
   
solve(BaseName,TimeLimit):-
    statistics(backtracks,Backs0),
    atom_codes(BaseName,String),
    append(String,".pl",String2),
    atom_codes(InFile,String2),
    (exists(InFile)->true;format("c File not found:~w~n",[InFile]),halt),
    see(InFile),
    cputime(Start),
    read((csp(Vars):-Body)),
    seen,
%    append(String,".sol",String3),
%    atom_codes(SolFile,String3),
%    SolFile=solution,
    SolFile=user,
    tell(SolFile),
    writeln(user,'c solving'(BaseName,TimeLimit)),
    writeln('c solving'(BaseName,TimeLimit)),
    solve_prob(Body,Vars,TimeLimit),
    cputime(End),
    statistics(backtracks,Backs1),
    NBacks is Backs1-Backs0,
    Time is End-Start,
    format("~nc Time=~w ms Backtracks=~w~n~n",[Time,NBacks]),!,
    told.

solve_prob(Body,Vars,TimeLimit):-
    execute_body(Body),!,
    (global_get('_$disjunctive_tasks',1)->
     Strategies=[ff_inout,ff_min,ff_backward];
     Strategies=[ffc_inout,ff_inout,forward,ff_backward,ffc]),
     global_set('_$disjunctive_tasks',0),
    solve_vars(Vars,TimeLimit,Strategies).
solve_prob(_Body,_Vars,_TimeLimit):-
    writeln('c before_labeling'),
    writeln('s UNSATISFIABLE'),nl.

execute_body(Body):-
    post_constr(Body,Disjunctions,[],Neqs),
    closetail(Neqs),
%    writeln(user,Neqs),
    post_neqs(Neqs),
    post_disjunctive_tasks(Disjunctions).

post_constr(G,Disjunctions,DisjunctionsR,Neqs):-
    G=((X*Y#<0#\/abs(X-Y)#>=N1),
       constr_scope([X,Y]),
       (X*Y#>0 #\/ abs(abs(X)-abs(Y))#>=N2),
       G1),
    dvar_excludable(X),dvar_excludable(Y),
    integer(N1),integer(N2),N1>=N2,
    b_DM_FALSE_cc(X,0),b_DM_FALSE_cc(Y,0) :
    constr_scope([X,Y]),
    (N1==N2->
     (N1==0->true;abs(abs(X)-abs(Y)) #>= N1)
    ;
     (N2==0->true; abs(X-Y)#>=N2, $comp_prop_fapp2(X,Y,N2,_)), %    X*Y#>0 #\/ abs(AbsY(X)-AbsY)#>=N2,
     $comp_prop_fapp1(X,Y,N1,_)),  %    X*Y#<0 #\/ abs(X-Y)#>=N1,
    post_constr(G1,Disjunctions,DisjunctionsR,Neqs).
post_constr(((Exp1 #\/ Exp2),G2),Disjunctions,DisjunctionsR,Neqs) :-
    Exp1=(abs(P1//N-P2//N)#=1#/\abs(P1 mod N-P2 mod N)#=2),
    Exp2=(abs(P1//N-P2//N)#=2#/\abs(P1 mod N-P2 mod N)#=1),
    integer(N),N>0, dvar(P1),dvar(P2),dvar_excludable(P1), dvar_excludable(P2),
    domain_min_max(P1,Min1,_),
    domain_min_max(P2,Min2,_),
    Min1>=0,Min2>=0 : 
    $knightMove(P1,P2,N),
    post_constr(G2,Disjunctions,DisjunctionsR,Neqs).
post_constr(((Exp1 #\/ (Exp2 #\/ Exp3)),G2),Disjunctions,DisjunctionsR,Neqs) :-
    Exp1=(P1 mod N#=P2 mod N),
    Exp2=(P1//N#=P2//N),
    Exp3=(abs(P1//N-P2//N)#=abs(P1 mod N-P2 mod N)),
    integer(N),N>0, dvar(P1),dvar(P2),dvar_excludable(P1), dvar_excludable(P2),
    domain_min_max(P1,Min1,_),
    domain_min_max(P2,Min2,_),
    Min1>=0,Min2>=0 : 
    $queenMove(P1,P2,N),
    post_constr(G2,Disjunctions,DisjunctionsR,Neqs).
post_constr((G1,G2),Disjunctions,DisjunctionsR,Neqs):-true :
    post_constr(G1,Disjunctions,Disjunctions1,Neqs),
    post_constr(G2,Disjunctions1,DisjunctionsR,Neqs).
post_constr(G,Disjunctions,DisjunctionsR,_Neqs):-G=((S1+D1 #=< S2) #\/ (S2 + D2 #=< S1)),
    dvar_excludable(S1),dvar_excludable(S2),integer(D1),integer(D2),D1>0,D2>0,S1\==S2 :
    Disjunctions=[disj_tasks(S1,D1,S2,D2)|DisjunctionsR].
post_constr(G,Disjunctions,DisjunctionsR,_Neqs):-G=((S2 #>= S1+D1) #\/ (S1 #>= S2 + D2)),
    dvar_excludable(S1),dvar_excludable(S2),integer(D1),integer(D2),D1>0,D2>0,S1\==S2 :
    Disjunctions=[disj_tasks(S1,D1,S2,D2)|DisjunctionsR].
post_constr(G,Disjunctions,DisjunctionsR,Neqs):-
    G=(V1#\=V2),
    dvar_excludable(V1),
    dvar_excludable(V2),
    dvar(V1),dvar(V2) :
    Disjunctions=DisjunctionsR,
    attach(G,Neqs).
post_constr(G,Disjunctions,DisjunctionsR,Neqs):-G=ec(Rel,CompVars) :
    Disjunctions=DisjunctionsR,
    ec(Rel,CompVars,Neqs).
post_constr(G,Disjunctions,DisjunctionsR,_Neqs):-true :
    Disjunctions=DisjunctionsR,
    call(G).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
/*  (X*Y#<0) #\/ (abs(X-Y)#>=N), X to Y */
:-determinate $opposite_sign_or_zero/2,$constructive_or_prop1/3.
$comp_prop_fapp1(X,Y,_N,Flag),var(Flag),{generated,ins(X),bound(X),ins(Y),bound(Y),ins(Flag)} => 
     b_COMP_PROP_FAPP1.
$comp_prop_fapp1(_X,_Y,_N,0) => true.
$comp_prop_fapp1(X,Y,N,1) => % X*Y<0 fails
     $constructive_or_prop1(X,Y,N),$constructive_or_prop1(Y,X,N).
$comp_prop_fapp1(X,Y,_N,_) => % (abs(X-Y)#>=N) fails
     $opposite_sign_or_zero(X,Y).

/* (X*Y#>0) #\/ (abs(abs(X)-abs(Y))#>=N), X to Y */
/* Bind Flag to: 0 if either (X*Y#>0) or (abs(abs(X)-abs(Y))#>=N)
		  01 if (X*Y#>0) fails because X<=0 Y>= 0
                10 if (X*Y#>0) fails because X>=0 Y<= 0
                 2 if (abs(abs(X)-abs(Y))#>=N) fails
*/
:-determinate fd_new_var/1,$same_sign_or_zero/2,$linear_constr_eq_2_ARC/5.
$comp_prop_fapp2(X,Y,_N,Flag),var(Flag),{ins(X),bound(X),ins(Y),bound(Y),ins(Flag)} => 
     b_COMP_PROP_FAPP2.
$comp_prop_fapp2(_X,_Y,_N,0) => true.
$comp_prop_fapp2(X,Y,N,01) => % X=<0 Y>=0
     (integer(X)->MX is -X;
      fd_new_var(MX),
      $linear_constr_eq_2_ARC(0,1,1,X,MX)),
     $constructive_or_prop1(MX,Y,N),
     $constructive_or_prop1(Y,MX,N).
$comp_prop_fapp2(X,Y,N,10) => % X>=0 Y=<0
     (integer(Y)->MY is -Y;
      fd_new_var(MY),
      $linear_constr_eq_2_ARC(0,1,1,Y,MY)),
     $constructive_or_prop1(X,MY,N),
     $constructive_or_prop1(MY,X,N).
$comp_prop_fapp2(X,Y,_N,_Flag) =>  /* Flag=2, abs(abs(X)-abs(Y))#>=N fails */
     $same_sign_or_zero(X,Y).

%%%%%%%%%
solve_vars(Vars,TimeLimit,[Strategy]):-true :
%    writeln(user,try(Strategy,TimeLimit)),
%    solve_vars_aux_nolimit(Vars,Strategy).
    solve_vars_aux(Vars,Strategy,TimeLimit,_Result).
solve_vars(Vars,TimeLimit,[Strategy|_Strategies]):-true ?
    TimeLimitForThisTry is TimeLimit//2,
%    writeln(user,try(Strategy,TimeLimitForThisTry)),
    solve_vars_aux(Vars,Strategy,TimeLimitForThisTry,Result),
    (Result\=time_out->true;
     fail).
solve_vars(Vars,TimeLimit,[_Strategy|Strategies]):-true :
    TimeLimitRest is TimeLimit-TimeLimit//2,
    solve_vars(Vars,TimeLimitRest,Strategies).
    
solve_vars_aux(Vars,Strategy,TimeLimit,Result):-
    time_out(solver_labeling(Vars,Strategy),TimeLimit,Result),!,
    (Result==success->
      writeln('c '(Strategy)),
      write('s SATISFIABLE'),nl,
      write('v'),write(' '),
      write_list(Vars),nl;
     true).
solve_vars_aux(_Vars,Strategy,_TimeLimit,Result):-
     Result=fail,
     writeln('c '(Strategy)),
     write('s UNSATISFIABLE'),nl.

solve_vars_aux_nolimit(Vars,Strategy):-
    solver_labeling(Vars,Strategy),!,
    writeln('c '(Strategy)),
    write('s SATISFIABLE'),nl,
    write('v'),write(' '),write_list(Vars),nl.
solve_vars_aux_nolimit(_Vars,Strategy):-
    writeln('c '(Strategy)),
    write('s UNSATISFIABLE'),nl.
    
solver_labeling([],_Strategy):-true : true.
solver_labeling([V|Vs],Strategy):-nonvar(V) : solver_labeling(Vs,Strategy).
solver_labeling([V|Vs],Strategy):-get_attr(V,scc_num,SccNo) :
     collect_vars_in_scc(Vs,SccNo,Scc,Rest),
     labeling([Strategy],[V|Scc]),!,
     solver_labeling(Rest,Strategy).
solver_labeling([V|Vs],Strategy):-true :
     indomain(V),
     solver_labeling(Vs,Strategy).

collect_vars_in_scc([],_SccNo,Scc,Rest):-true : Scc=[],Rest=[].
collect_vars_in_scc([V|Vs],SccNo,Scc,Rest):-nonvar(V) : 
     collect_vars_in_scc(Vs,SccNo,Scc,Rest).
collect_vars_in_scc([V|Vs],SccNo,Scc,Rest):-get_attr(V,scc_num,SccNo) :
     Scc=[V|SccR],
     collect_vars_in_scc(Vs,SccNo,SccR,Rest).
collect_vars_in_scc([V|Vs],SccNo,Scc,Rest):-true :
     Rest=[V|RestR],
     collect_vars_in_scc(Vs,SccNo,Scc,RestR).

% All variables in a strongly-collected-component share the same identity variable SCC
constr_scope_tuple(Arity,Vars):-
    constr_scope_tuple(Arity,Vars,_SCC).

constr_scope_tuple(0,_Vect,_SCC):-true : true.
constr_scope_tuple(I,Vect,SCC):-true : 
    arg(I,Vect,V),
    (var(V)->put_attr_no_hook(V,scc_num,SCC);true),
    I1 is I-1,
    constr_scope_tuple(I1,Vect,SCC).

constr_scope(Vars):-
    constr_scope(Vars,_SCC).

constr_scope([],_SCC):-true : true.
constr_scope([V|Vs],SCC):-true : 
    (var(V)->put_attr_no_hook(V,scc_num,SCC);true),
    constr_scope(Vs,SCC).

%%
call_all_distinct(Vs):-
     constr_scope(Vs,_SCC),
     all_distinct(Vs).

%%
call_cumulative(Os,Ds,Es,Hs,Limit):-
     cumulative_no_dvar(Es),!,
     constr_scope(Os,SCC),
     constr_scope(Ds,SCC),
     constr_scope(Hs,SCC),
     cumulative(Os,Ds,Hs,Limit).
call_cumulative(Os,Ds,Es,Hs,Limit):-
     constr_scope(Os,SCC),
     constr_scope(Ds,SCC),
     constr_scope(Es,SCC),
     constr_scope(Hs,SCC),
     relate_os_es(Os,Ds,Es),
     cumulative(Os,Ds,Hs,Limit).

cumulative_no_dvar([]):-true : true.
cumulative_no_dvar([X|_]):-dvar_or_int(X) : fail.
cumulative_no_dvar([_|Xs]):-true : 
     cumulative_no_dvar(Xs).

relate_os_es([],_Ds,_Es):-true : true.
relate_os_es([O|Os],[D|Ds],[E|Es]):-true : 
     O+D #= E,
     relate_os_es(Os,Ds,Es).
%%
call_element(I,As,V):-
     constr_scope([I,V|As],_SCC),
     element(I,As,V).
     
%%
call_weightedSum(Coes,Vs,Rel,Rhs):-
     constr_scope([Rhs|Vs],_SCC),
     rel_to_constr(Rel,ConstrRel),
     scalar_product(Coes,Vs,ConstrRel,Rhs).

rel_to_constr(eq,'#=').
rel_to_constr(ne,'#\=').
rel_to_constr(ge,'#>=').
rel_to_constr(gt,'#>').
rel_to_constr(le,'#=<').
rel_to_constr(lt,'#<').

write_list([]):-true : true.
write_list([X|Xs]):-true :
    write(X),write(' '),
    write_list(Xs).

/****************************************************************/
%%    Let X1 = P1//N, Y1 = P1 mod N, X2 = P2//N, Y2 = P2 mod N
%%    abs(X1-X2)=1 /\ abs(Y1-Y2)=2  \/  abs(X1-X2)=2 /\ abs(Y1-Y2)=1
$knightMove(P1,P2,N):-
    CompVars=(P1,P2),
    domain_min_max(P1,Min1,Max1),
    $create_knight_moves(P1,Min1,Max1,N,P2,Tuples),
    CompVars in Tuples.

$create_knight_moves(_P1,Max,Max,N,P2,Tuples):-true : 
    $create_knight_moves_aux(Max,N,P2,Tuples,[]).
$create_knight_moves(P1,Cur,Max,N,P2,Tuples):-true :
    $create_knight_moves_aux(Cur,N,P2,Tuples,Tuples1),
    b_DM_NEXT_ccf(P1,Cur,Next),
    $create_knight_moves(P1,Next,Max,N,P2,Tuples1).

$create_knight_moves_aux(Code1,N,P2,Tuples,TuplesR):-
    X is Code1//N,
    Y is Code1 mod N,
    X1 is X+1,  Y1 is Y+2,
    $add_knight_move(Code1,X1,Y1,N,P2,Tuples,Tuples1),
    X2 is X+1,  Y2 is Y-2,
    $add_knight_move(Code1,X2,Y2,N,P2,Tuples1,Tuples2),
    X3 is X-1,  Y3 is Y+2,
    $add_knight_move(Code1,X3,Y3,N,P2,Tuples2,Tuples3),
    X4 is X-1,  Y4 is Y-2,
    $add_knight_move(Code1,X4,Y4,N,P2,Tuples3,Tuples4),
    X5 is X+2,  Y5 is Y+1,
    $add_knight_move(Code1,X5,Y5,N,P2,Tuples4,Tuples5),
    X6 is X+2,  Y6 is Y-1,
    $add_knight_move(Code1,X6,Y6,N,P2,Tuples5,Tuples6),
    X7 is X-2,  Y7 is Y+1,
    $add_knight_move(Code1,X7,Y7,N,P2,Tuples6,Tuples7),
    X8 is X-2,  Y8 is Y-1,
    $add_knight_move(Code1,X8,Y8,N,P2,Tuples7,TuplesR).

$add_knight_move(Code1,X,Y,N,P2,Tuples,TuplesR):-
    X>=0,Y>=0,Y<N :
    Code2 is X*N+Y,
    (b_DM_TRUE_cc(P2,Code2)->Tuples=[(Code1,Code2)|TuplesR];Tuples=TuplesR).
$add_knight_move(_Code1,_X,_Y,_N,_P2,Tuples,TuplesR):-true :
    Tuples=TuplesR.

% (P1 mod N#=P2 mod N) or 
% (P1//N#=P2//N) or 
% (abs(P1//N-P2//N)#=abs(P1 mod N-P2 mod N)),
$queenMove(P1,P2,N):-
    CompVars=(P1,P2),
    domain_min_max(P1,Min1,Max1),
    $create_queen_moves(P1,Min1,Max1,N,P2,Tuples),
    CompVars in Tuples.

$create_queen_moves(_P1,Max,Max,N,P2,Tuples):-true : 
    $create_queen_moves2(Max,N,P2,Tuples,[]).
$create_queen_moves(P1,Cur,Max,N,P2,Tuples):-true :
    $create_queen_moves2(Cur,N,P2,Tuples,Tuples1),
    b_DM_NEXT_ccf(P1,Cur,Next),
    $create_queen_moves(P1,Next,Max,N,P2,Tuples1).

$create_queen_moves2(I1,N,P2,Tuples,TuplesR):-
    domain_min_max(P2,Min2,Max2),
    $create_queen_moves2(I1,N,P2,Min2,Max2,Tuples,TuplesR).

$create_queen_moves2(I1,N,_P2,I2,Max,Tuples,TuplesR):-I2==Max :
   ($isQueenMove(I1,I2,N)->
    Tuples=[(I1,I2)|TuplesR];Tuples=TuplesR).
$create_queen_moves2(I1,N,P2,I2,Max,Tuples,TuplesR):-true :
   ($isQueenMove(I1,I2,N)->
    Tuples=[(I1,I2)|Tuples1];Tuples=Tuples1),
    b_DM_NEXT_ccf(P2,I2,NextI2),
   $create_queen_moves2(I1,N,P2,NextI2,Max,Tuples1,TuplesR).
   
$isQueenMove(I1,I2,N):-
   I1 mod N =:= I2 mod N : true.
$isQueenMove(I1,I2,N):-
   I1//N =:= I2//N : true.
$isQueenMove(I1,I2,N):-
   abs(I1//N-I2//N)=:=abs(I1 mod N-I2 mod N) : true.

dump_props:-
   tell(trace),
   csp(_),
   frozen(L),
   writeln(L),
   told.

    
