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.