:- use_module(library(clpfd)).
:- use_module('/afs/inria.fr/rocq/home/contraintes/jmartin/rules2cp/interpreter/prolog/r2cp.pl').
:- init_interpreter.

rcp_rule(q(var('I',0)), rcp_rec([row=free_var('_',0,1),column=var('I',0)])).
rcp_rule(board(var('N',0)), foldr(var('I',69),[1..var('N',0)],cons,[],q(var('I',69)))).
rcp_rule(safe(var('L',0)), all_different(variables(var('L',0)))and foldl(var('Q',80),var('L',0),and,1,foldl(var('R',84),var('L',0),and,1,let(var('I',87),rcp_att(column,[var('Q',80)]),let(var('J',89),rcp_att(column,[var('R',84)]),var('I',87)<var('J',89)implies rcp_att(row,[var('Q',80)])#var('J',89)-var('I',87)+rcp_att(row,[var('R',84)])and rcp_att(row,[var('Q',80)])#var('I',87)-var('J',89)+rcp_att(row,[var('R',84)])))))).
rcp_rule(queens_constraints(var('N',0)), let(var('B',91),board(var('N',0)),domain(variables(var('B',91)),1,var('N',0))and safe(var('B',91)))).

rcp_rule(queens_search(var('N',0)), let(var('B',93),board(var('N',0)),
					variable_ordering([least(var_order_criterion(2,[]))])and
				       labeling(variables(var('B',93))))).

rcp_rule(solve_query, let(var('N',94),4,queens_constraints(var('N',94))and(dynamic queens_search(var('N',94))))).


q(I, _A_) :- 
	rcp_var(from(q(I),0,1), Q_I),
	rcp_rec([row=Q_I,column=I], _A_).

q_search(I, _A_) :- 
	rcp_var(from(q(I),0,1), Q_I),
	rcp_rec([row=Q_I,column=I], _A_).

board_foldr_1([], _, []) :- 
	!.
board_foldr_1([I_68|Tail], [N], [_A_|_B_]) :- 
	board_foldr_1(Tail, [N], _B_),
	q(I_68, _A_).

board_foldr_1_search([], _, []) :- 
	!.
board_foldr_1_search([I_68|Tail], [N], [_A_|_B_]) :- 
	board_foldr_1_search(Tail, [N], _B_),
	q_search(I_68, _A_).

board(N, _B_) :- 
	rcp_range([1..N], _A_),
	board_foldr_1(_A_, [N], _B_).

board_search(N, _B_) :- 
	rcp_range([1..N], _A_),
	board_foldr_1_search(_A_, [N], _B_).

safe_foldl_2([], I_and, _, I_and) :- 
	!.
safe_foldl_2([R_74|Tail], I_and, [L,Q_70], _P_) :- 
	rcp_att(column, Q_70, _A_),
	I_77=_A_,
	rcp_att(column, R_74, _B_),
	J_79=_B_,
	fd_implies(_C_, _N_, _O_),
	fd_lt(I_77, J_79, _C_),
	fd_and(_H_, _M_, _N_),
	rcp_att(row, Q_70, _D_),
	fd_aeq(J_79-I_77, _E_),
	rcp_att(row, R_74, _F_),
	fd_aeq(_E_+_F_, _G_),
	fd_neq(_D_, _G_, _H_),
	rcp_att(row, Q_70, _I_),
	fd_aeq(I_77-J_79, _J_),
	rcp_att(row, R_74, _K_),
	fd_aeq(_J_+_K_, _L_),
	fd_neq(_I_, _L_, _M_),
	fd_and(I_and, _O_, _Q_),
	safe_foldl_2(Tail, _Q_, [L,Q_70], _P_).

safe_foldl_2_search([], I_and, _, I_and) :- 
	!.
safe_foldl_2_search([R_74|Tail], I_and, [L,Q_70], _L_) :- 
	rcp_att(column, Q_70, _A_),
	I_77=_A_,
	rcp_att(column, R_74, _B_),
	J_79=_B_,
	(
	fd_lt(I_77, J_79),
	rcp_att(row, Q_70, _C_),
	fd_aeq(J_79-I_77, _D_),
	rcp_att(row, R_74, _E_),
	fd_aeq(_D_+_E_, _F_),
	rcp_att(row, Q_70, _G_),
	fd_aeq(I_77-J_79, _H_),
	rcp_att(row, R_74, _I_),
	fd_aeq(_H_+_I_, _J_),
	fd_equiv((fd_neq(_C_,_F_),fd_neq(_G_,_J_)), _K_, 1)
	;
	fd_geq(I_77, J_79),
	fd_aeq(_K_, 1)
	),
	rcp_assert(I_and),
	rcp_assert(_K_),
	safe_foldl_2_search(Tail, _M_, [L,Q_70], _L_).

safe_foldl_1([], I_and, _, I_and) :- 
	!.
safe_foldl_1([Q_70|Tail], I_and, [L], _B_) :- 
	safe_foldl_2(L, 1, [L,Q_70], _A_),
	fd_and(I_and, _A_, _C_),
	safe_foldl_1(Tail, _C_, [L], _B_).

safe_foldl_1_search([], I_and, _, I_and) :- 
	!.
safe_foldl_1_search([Q_70|Tail], I_and, [L], _B_) :- 
	safe_foldl_2_search(L, 1, [L,Q_70], _A_),
	rcp_assert(I_and),
	rcp_assert(_A_),
	safe_foldl_1_search(Tail, _C_, [L], _B_).

safe(L, _B_) :- 
	variables(L, _A_),
	all_different(_A_),
	safe_foldl_1(L, 1, [L], _B_).

safe_search(L, _C_) :- 
	variables(L, _A_),
	all_different(_A_),
	safe_foldl_1_search(L, 1, [L], _B_),
	rcp_assert(_B_),
	fd_aeq(_C_, 1).

queens_constraints(N, _C_) :- 
	board(N, _A_),
	B_90=_A_,
	variables(B_90, _B_),
	domain(_B_, 1, N),
	safe(B_90, _C_).

queens_constraints_search(N, _D_) :- 
	board_search(N, _A_),
	B_90=_A_,
	variables(B_90, _B_),
	domain(_B_, 1, N),
	safe_search(B_90, _C_),
	rcp_assert(_C_),
	fd_aeq(_D_, 1).

var_order_criterion(1, Candidate, [], _C_) :- 
	rcp_call(Candidate, _A_),
	rcp_att(row, _A_, _B_),
	fd_size(_B_, _C_).

queens_search(N, _C_) :- 
	board(N, _A_),
	B_92=_A_,
	variables(B_92, _B_),
	variable_ordering([least(var_order_criterion(1,[]))]),
	rcp_labeling(_B_),
	fd_aeq(_C_, 1).

queens_search_search(N, _C_) :- 
	board_search(N, _A_),
	B_92=_A_,
	variables(B_92, _B_),
	variable_ordering([least(var_order_criterion(1,[]))]),
	rcp_labeling(_B_),
	fd_aeq(_C_, 1).

var_order_criterion(2, Candidate, [], _C_) :- 
	rcp_call(Candidate, _A_),
	rcp_att(row, _A_, _B_),
	fd_size(_B_, _C_),
	write(fd_size(_B_, _C_)),nl.

solve([Q_1,Q_2,Q_3,Q_4]) :- 
	rcp_var(from(q(1),0,1), Q_1),
	rcp_var(from(q(2),0,1), Q_2),
	rcp_var(from(q(3),0,1), Q_3),
	rcp_var(from(q(4),0,1), Q_4),
	domain([Q_1,Q_2,Q_3,Q_4], 1, 4),
	all_different([Q_1,Q_2,Q_3,Q_4]),
	Q_1#\=1+Q_2,
	Q_1#\= -1+Q_2,
	Q_1#\=2+Q_3,
	Q_1#\= -2+Q_3,
	Q_1#\=3+Q_4,
	Q_1#\= -3+Q_4,
	Q_2#\=1+Q_3,
	Q_2#\= -1+Q_3,
	Q_2#\=2+Q_4,
	Q_2#\= -2+Q_4,
	Q_3#\=1+Q_4,
	Q_3#\= -1+Q_4,
	rcp_assert(_A_),
	queens_search(4, _A_).
