module cp.
import common_constr.

% X #!= Y
% X #/\ Y
% X #< Y
% X #<= Y
% X #<=> Y
% X #= Y
% X #=< Y
% X #=> Y
% X #> Y
% X #>= Y
% X #\/ Y
% X #^ Y
%  #~ X
% Vars::Exp
% Vars notin Exp
% acyclic(Vs,Es)
% acyclic_d(Vs,Es)
% all_different(FDVars)
% all_different_except_0(FDVars)
% all_distinct(FDVars)
% assignment(FDVars1,FDVars2)
% at_least(N,L,V)
% at_most(N,L,V)
% circuit(FDVars)
% count(V,FDVars,N)
% count(V,FDVars,Rel,N)
% cumulative(Ss,Ds,Rs,Limit)
% decreasing(L)
% decreasing_strict(L)
% diffn(RectangleList)
% disjunctive_tasks(Tasks)(cp only)
% element(I,List,V)
% element0(I,List,V)
% exactly(N,L,V):
% fd_degree(FDVar)=Degree(cp only)
% fd_disjoint(DVar1,DVar2)
% fd_dom(FDVar) = List
% fd_false(FDVar,Elm)
% fd_max(FDVar) = Max
% fd_min(FDVar) = Min
% fd_min_max(FDVar,Min,Max)
% fd_next(FDVar,Elm) = NextElm
% fd_prev(FDVar,Elm) = PrevElm
% fd_set_false(FDVar,Elm)(cp only)
% fd_size(FDVar) = Size
% fd_true(FDVar,Elm)
% fd_vector_min_max(Min,Max)
% global_cardinality(List,Pairs)
% hcp(Vs,Es)
% hcp(Vs,Es,K)
% hcp_grid(A)
% hcp_grid(A,Es)
% hcp_grid(A,Es,K)
% increasing(L)
% increasing_strict(L)
% indomain(Var)(nondet)(cp only)
% indomain_down(Var)(nondet)(cp only)
% lex_le(L_1,L_2)
% lex_lt(L_1,L_2)
% matrix_element(Matrix,I,J,V)
% matrix_element0(Matrix,I,J,V)
% neqs(NeqList)(cp only)
% new_dvar() = FDVar
% new_fd_var() = FDVar
% path(Vs,Es,Src,Dest)
% path_d(Vs,Es,Src,Dest)
% regular(X,Q,S,D,Q0,F)
% scalar_product(A,X,Product)
% scalar_product(A,X,Rel,Product)
% scc(Vs,Es)
% scc(Vs,Es,K)
% scc_d(Vs,Es)
% scc_d(Vs,Es,K)
% scc_grid(A)
% scc_grid(A,K)
% serialized(Starts,Durations)
% solve(Opts,Vars)(nondet)
% solve(Vars)(nondet)
% solve_all(Opts,Vars) = List
% solve_all(Vars) = List
% solve_suspended(Opt)(cp only)
% solve_suspended(cp only)
% subcircuit(FDVars)
% subcircuit_grid(A)
% subcircuit_grid(A,K)
% table_in(DVars,R)
% table_notin(DVars,R)
% tree(Vs,Es)
% tree(Vs,Es,K)

include "cp_sat_mip_smt.pi". % common built-ins for cp, sat, mip, and smt

'::'(Vars,Domain) =>
    bp.'_$_picat_in'(cp,Vars,Domain).

% '#='(X,Y) => '#='(X,Y) 
'#='(X,Y) => bp.'#='(X,Y).

% '#>='(X,Y) => '#>='(X,Y)
'#>='(X,Y) => bp.'#>='(X,Y).

% '#>'(X,Y) => '#>'(X,Y)
'#>'(X,Y) => bp.'#>'(X,Y).

% '#<'(X,Y) => '#<'(X,Y)
'#<'(X,Y) => bp.'#<'(X,Y).

% '#=<'(X,Y) => '#=<'(X,Y)
'#=<'(X,Y) => bp.'#=<'(X,Y).

% '#!='(X,Y) => '#!='(X,Y)
'#!='(X,Y) => bp.'#\\='(X,Y).

% '#\\='(X,Y) => '#\\='(X,Y)
'#\\='(X,Y) => bp.'#\\='(X,Y).

% '#<=>'(X,Y) => '#<=>'(X,Y)
'#<=>'(X,Y) => bp.'#<=>'(X,Y).

% '#=>'(X,Y) => '#=>'(X,Y)
'#=>'(X,Y) => bp.'#=>'(X,Y).

% '#/\\'(X,Y) => '#/\\'(X,Y)
'#/\\'(X,Y) => bp.'#/\\'(X,Y).

% '#\\/'(X,Y) => '#\\/'(X,Y)
'#\\/'(X,Y) => bp.'#\\/'(X,Y).

% '#^'(X,Y) => '#^'(X,Y)
'#^'(X,Y) => bp.'#\\'(X,Y).

% '#~'(X) => '#~'(X)
'#~'(X) => bp.'#\\'(X).

% solve(Vars) => solve(Vars).
solve(Vars) => 
    (bp.dvar_or_int_list(Vars) -> VList = Vars; vars(Vars) = VList),
    bp.labeling([],VList).

% solve(Options,Vars) => solve(Options,Vars)
solve(Options,Vars) =>
    (bp.dvar_or_int_list(Vars) -> VList = Vars; vars(Vars) = VList),
    (select($report(ReportCall), Options,Options1) ->
        MetaCalls = [$report('$dyna_eval_pred'(['$picat_top_level'],ReportCall))]
    ;
        Options1 = Options,
        MetaCalls = []
    ),
    (select($label(LabelPred), Options1,Options2) ->
        (atom(LabelPred) -> true; handle_exception($atom_expected(LabelPred), solve)),
        (bp.'$dyna_resolve_name'(['$picat_top_level'],LabelPred,1,pred,MLabelPred) ->
            true
        ;
            bp.c_module_qualified_pred_name(glb,LabelPred,MLabelPred)
        ),
        MetaCalls1 = [$label(MLabelPred)|MetaCalls]
    ;
        Options2 = Options1,
        MetaCalls1 = MetaCalls
    ),
    bp.labeling(MetaCalls1 ++ Options2,VList).

% solve_all(Vars) = solve_all(Vars).
solve_all(Vars) =
    solve_all([],Vars).

% solve_all(Options,Vars) = solve_all(Options,Vars).
solve_all(Options,Vars) =
    findall(Vars, solve(Options,Vars)).

% solve_suspended => solve_suspended.
solve_suspended =>
    bp.frozen(FL),
    FVars = [FVar : FVar in vars(FL), dvar(FVar)],
    bp.labeling([],FVars).

solve_suspended(Options) =>
    bp.frozen(FL),
    FVars = [FVar : FVar in vars(FL), dvar(FVar)],
    bp.labeling(Options,FVars).

% fd_degree(FDVar) = fd_degree(FDVar).
fd_degree(FDVar) = Degree, dvar(FDVar) => bp.fd_degree(FDVar,Degree).
fd_degree(FDVar) = Degree, integer(FDVar) => Degree = 0.
fd_degree(FDVar) = _Degree => handle_exception($dvar_expected(FDVar), fd_degree).
    
% fd_set_false(FDVar,Elm) => fd_set_false(FDVar,Elm).
fd_set_false(FDVar,Elm), dvar_or_int(FDVar), integer(Elm) => 
    bp.domain_set_false(FDVar,Elm).
fd_set_false(FDVar,Elm) =>
    Source = fd_set_false,
    (integer(Elm) ->
        handle_exception($dvar_expected(FDVar), Source)
    ;
        handle_exception($integer_expected(Elm), Source)
    ).

% all_different(FDVars) => all_different(FDVars).
all_different(FDVars) =>
    (array(FDVars) -> to_list(FDVars) = List; List = FDVars),
    bp.alldifferent(List).
    
% all_distinct(FDVars) => all_distinct(FDVars).
all_distinct(FDVars) =>
    (array(FDVars) -> to_list(FDVars) = List; List = FDVars),
    bp.all_distinct(List).

% assignment(FDVars1,FDVars2) => assignment(FDVars1,FDVars2).
assignment(FDVars1,FDVars2) =>
    (array(FDVars1) -> to_list(FDVars1) = List1; List1 = FDVars1),
    (array(FDVars2) -> to_list(FDVars2) = List2; List2 = FDVars2),
    bp.assignment(List1,List2).
    
% circuit(FDVars) => circuit(FDVars).
circuit(FDVars) =>
    (array(FDVars) -> to_list(FDVars) = List; List = FDVars),
    bp.circuit(List).

% cumulative(Starts,Durations,Resources,Limit) => cumulative(Starts,Durations,Resources,Limit).
cumulative(Starts,Durations,Resources,Limit) =>
    (array(Starts) -> to_list(Starts) = SList; SList = Starts),    
    (array(Durations) -> to_list(Durations) = DList; DList = Durations),    
    (array(Resources) -> to_list(Resources) = RList; RList = Resources),
    bp.bp_cumulative(SList,DList,RList,Limit,cp).
    
% diffn(RectangleList) => diffn(RectangleList).
diffn(RectangleList) =>
    (array(RectangleList) -> to_list(RectangleList) = RList; RList = RectangleList),
    bp.bp_diffn(RList,cp).

% disjunctive_tasks(Tasks) => disjunctive_tasks(Tasks).
disjunctive_tasks(Tasks) =>
    (array(Tasks) -> to_list(Tasks) = TList; TList = Tasks),    
    bp.post_disjunctive_tasks(TList).

% element(I,Terms,V) => element(I,Terms,V).
element(I,Terms,V) =>
    (array(Terms) -> to_list(Terms) = List; List = Terms),    
    (bp.dvar_or_int_list(List) -> true; handle_exception($dvar_or_int_list_expected(List), element)),
    bp.element(I,List,V).

% 0-based indexing
% element0(I,FDVars,V) => element0(I,FDVars,V).
element0(I,FDVars,V) =>
    (array(FDVars) -> to_list(FDVars) = List; List = FDVars),
    (bp.dvar_or_int_list(List) -> true; handle_exception($dvar_or_int_list_expected(List), element)),
    bp.element0(I,List,V).

% fd_set_false(FDVar,Elm) => fd_set_false(FDVar,Elm).
% global_cardinality(FDVars,Pairs) => global_cardinality(FDVars,Pairs).
global_cardinality(List,Pairs) =>
    (bp.check_pairs(Pairs) -> true; handle_exception($pairs_expected(Pairs), global_cardinality)),
    bp.global_cardinality(List,Pairs).

% indomain(Var) => indomain(Var).
indomain(Var), dvar(Var) =>
    bp.indomain_dvar(Var).
indomain(Var), integer(Var) =>  true.
indomain(Var) =>
    handle_exception($dvar_expected(Var), indomain).

% indomain_down(Var) => indomain_down(Var).
indomain_down(Var), dvar(Var) =>
    bp.domain_min_max(Var,_,Max),
    bp.indomain_dvar_backward(Var,Max).
indomain_down(Val), integer(Val) => true.
indomain_down(Var) =>
    handle_exception($dvar_expected(Var), indomain_down).

% neqs(Neqs) => neqs(Neqs).
neqs(Neqs) =>
    (array(Neqs) -> to_list(Neqs) = List; List = Neqs),    
    check_neqs_args(List,List1),
    bp.post_neqs(List1).

% serialized(Starts,Durations) => serialized(Starts,Durations).
serialized(Starts,Durations) =>
    (array(Starts) -> to_list(Starts) = SList; SList = Starts),    
    (array(Durations) -> to_list(Durations) = DList; DList = Durations),    
    bp.disjunctive_tasks(SList,DList).

% subcircuit(FDVars) => subcircuit(FDVars).
subcircuit(FDVars) =>
    (array(FDVars) -> to_list(FDVars) = List; List = FDVars),
    bp.subcircuit(List).   

%%%%%%%%%%%%%%%%%%%%%%%% common to cp and sat modules %%%%%%%%%%%%%%%%%%%%%%
%%
table_in(Vars,Tuples) =>
    bp.table_in(Vars,Tuples).

%%
notin(Vars,Domain) =>
    bp.'_$_picat_notin'(cp,Vars,Domain).

%%
table_notin(Vars,Tuples) =>
    bp.table_notin(Vars,Tuples).

/************************************************************************* 
    regular(L,Q,S,M,Q0,Fs)

  L : A sentence (an IntVar array or list)
  Q : number of states
  S : input_max, inputs are from 1 to S
  M : transition matrix:  M[I,J] (I in 1..S, J in 1..Q) is a list of outgoing states for NFA (0 means an error).
  Q0: initial state
  Fs : accepting states
***************************************************************************/
regular(L, Q, S, M, Q0, Fs) =>
    regular_constr(L, Q, S, M, Q0, Fs, cp).

%%
%% lex_le(L1,L2): collection L1 is lexicographically less than or equal to L2
%%
lex_le(L1,L2), list(L1), list(L2) =>
    check_args_lex(L1,L2,L11,L22),
    lex_le_aux(L11,L22).
lex_le(L1,L2), array(L1), array(L2) =>
    check_args_lex(to_list(L1), to_list(L2), L11,L22),
    lex_le_aux(L11,L22).
lex_le(L1,L2) =>
    throw($invalid(lex_le(L1,L2))).

%%
%% lex_lt(L1,L2): collection L1 is lexicographically less than L2
%%
lex_lt(L1,L2), list(L1), list(L2) =>
    check_args_lex(L1,L2,L11,L22),
    lex_lt_aux(L11,L22).
lex_lt(L1,L2), array(L1), array(L2) =>
    check_args_lex(to_list(L1), to_list(L2), L11,L22),
    lex_lt_aux(L11,L22).
lex_lt(L1,L2) =>
    throw($invalid(lex_lt(L1,L2))).

check_args_lex(L1,L2,L11,L22) =>
    (bp.dvar_or_int_list(L1) -> true; handle_exception($dvar_list_expected(L1), lex)),
    (bp.dvar_or_int_list(L2) -> true; handle_exception($dvar_list_expected(L2), lex)),
    N1 = length(L1),
    N2 = length(L2),
    (N1 == N2 ->
        L11 = L1, L22 = L2
    ; N1 < N2 ->
        Min = min([fd_min(V) : V in L2]),
        Min1 = Min-1,
        L1Pad = [Min1 : _ in 1..N2-N1],
        L11 = L1++L1Pad, L22 = L2
    ;
        Min = min([fd_min(V) : V in L1]),
        Min1 = Min-1,
        L2Pad = [Min1 : _ in 1..N1-N2],
        L11 = L1, L22 = L2++L2Pad
    ).

%%%
lex_le_aux([],_) => true.
lex_le_aux([X],[Y]) => 
    (var(X) ->
        (var(Y) ->
            bp.v_ge_v(Y,X)
        ;
            bp.domain_region_max(X,Y)
        )
    ;
        (var(Y) ->
            bp.domain_region_min(Y,X)
        ;
            X =< Y
        )
    ).
lex_le_aux([X|Xs],[Y|Ys]), integer(X), integer(Y) =>
    (X < Y -> 
        true
    ; X == Y ->
        lex_le_aux(Xs,Ys)
    ;
        fail
    ).
lex_le_aux([X|Xs],[Y|Ys]) =>
    watch_lex_le(X,Y,Xs,Ys).

watch_lex_le(X,Y,_Xs,_Ys), var(X),
    {generated, ins(X), ins(Y), bound(X), bound(Y)} 
 =>
    fd_min_max(X,MinX,_),
    fd_min_max(Y,_,MaxY),
    (MinX > MaxY -> fail; true).
watch_lex_le(X,Y,_Xs,_Ys), var(Y),
    {generated, ins(Y), bound(Y)} 
 =>
    fd_min_max(X,MinX,_),
    fd_min_max(Y,_,MaxY),
    (MinX > MaxY -> fail; true).
watch_lex_le(X,Y,Xs,Ys) =>   % come here when both X, Y become integers
    (X < Y ->
        true
    ; X == Y ->
        lex_le(Xs,Ys)
    ; 
        fail
    ).

%%%
lex_lt_aux([],_) => true.
lex_lt_aux([X],[Y]) => 
    (var(X) ->
        (var(Y) ->
            bp.v_gt_v(Y,X)
        ;
            bp.domain_region_max(X,Y-1)
        )
    ;
        (var(Y) ->
            bp.domain_region_min(Y,X+1)
        ;
            X < Y
        )
    ).
lex_lt_aux([X|Xs],[Y|Ys]), integer(X), integer(Y) =>
    (X < Y -> 
        true
    ; X == Y ->
        lex_lt_aux(Xs,Ys)
    ;
        fail
    ).
lex_lt_aux([X|Xs],[Y|Ys]) =>
    watch_lex_lt(X,Y,Xs,Ys).

watch_lex_lt(X,Y,_Xs,_Ys), var(X),
    {generated, ins(X), ins(Y), bound(X), bound(Y)} 
 =>
    fd_min_max(X,MinX,_),
    fd_min_max(Y,_,MaxY),
    (MinX > MaxY -> fail; true).
watch_lex_lt(X,Y,_Xs,_Ys), var(Y),
    {generated, ins(Y), bound(Y)} 
 =>
    fd_min_max(X,MinX,_),
    fd_min_max(Y,_,MaxY),
    (MinX > MaxY -> fail; true).
watch_lex_lt(X,Y,Xs,Ys) =>   % come here when both X, Y become integers
    (X < Y ->
        true
    ; X == Y ->
        lex_lt(Xs,Ys)
    ; 
        fail
    ).

%%
nvalue(N, L) => bp.nvalue(N,L).

%% The following constraints are proposed and implemented by Hakan Kjellerstrand
matrix_element(M,I,J,MIJ) =>
    check_matrix(M,NRows,NCols),
    matrix_element(M,NRows,NCols,I,J,MIJ,cp).

%
% Requires that all non-zero values in Xs are distinct.
%
alldifferent_except_0(Xs) =>
    all_different_except_0(Xs).

all_different_except_0(Xs) =>
    (list(Xs) ->
        Arr = to_array(Xs)
    ;array(Xs) ->
        Arr = Xs
    ;
        handle_exception($dvar_or_int_collection_expected(Xs), all_different_except_0)
    ),
    all_different_except_0_aux(Arr).

all_different_except_0_aux(Xs) =>
    N = len(Xs),
    foreach(I in 1..N-1, J in I+1..N)
        Xs[I] #= 0 #\/ Xs[J] #= 0 #\/ Xs[I] #!= Xs[J]
    end.