:- use_module('ITERATIVE_COMPILATION', [construit_bl/3]).
:- use_module('RECURSIVE_COMPILATION', [recursive_compilation/3]).
:- use_module('TRACE_SEARCH_QCSP', [trace_search_qcsp/3]).
:- use_module('QCSP_BASE', [equivalente_qcsp_base/2]).

:- prolog_flag(toplevel_print_options,_,[quoted(true),numbervars(true),portrayed(true),max_depth(2000)]).
:- prolog_flag(debugger_print_options,_,[quoted(true),numbervars(true),portrayed(true),max_depth(2000)]).


%% EEEE
% | ?-  _Quant = [e(X, [0,1,2]), e(Y, [0,1,2]), e(Z, [0,1,2]), e(T, [0,1,2])], _Contraintes = (X #= (Y*Z)+T), trace_search_qcsp(_Quant, _Contraintes, _Trace), construit_bl(_Quant, _Trace, Base_Trace), recursive_compilation(_Quant, _Contraintes, _Base_Rec), equivalente_qcsp_base(Base_Trace, _Base_Rec).
% Base_Trace = bl([vlva(X,[0,1,2],[va(0),va(1),va(2)]),vlva(Y,[0,1,2],[va(0,ab(X,2,1,0)),va(1,ab(X,2,1,0)),va(2,ab(X,2,1,0))]),vlva(Z,[0,1,2],[va(0,ab(X,(2,ab(Y,2,1,0)),(1,ab(Y,2,1,0)),(0,ab(Y,2,1,0)))),va(1,ab(X,(2,ab(Y,2,1,0)),(1,ab(Y,1,0)),(0,ab(Y,0)))),va(2,ab(X,(2,ab(Y,1,0)),(1,ab(Y,0)),(0,ab(Y,0))))]),vlva(T,[0,1,2],[va(0,ab(X,(2,ab(Y,(2,ab(Z,1)),(1,ab(Z,2)))),(1,ab(Y,(1,ab(Z,1)))),(0,ab(Y,(2,ab(Z,0)),(1,ab(Z,0)),(0,ab(Z,2,1,0)))))),va(1,ab(X,(2,ab(Y,(1,ab(Z,1)))),(1,ab(Y,(2,ab(Z,0)),(1,ab(Z,0)),(0,ab(Z,2,1,0)))))),va(2,ab(X,(2,ab(Y,(2,ab(Z,0)),(1,ab(Z,0)),(0,ab(Z,2,1,0))))))])]) ? ;
% no



%% EEAE
% | ?-  _Quant = [e(X, [0,1,2]), e(Y, [0,1,2]), a(Z, [0,1,2]), e(T, [0,1,2])], _Contraintes = (X #= (Y*Z)+T), trace_search_qcsp(_Quant, _Contraintes, _Trace), construit_bl(_Quant, _Trace, Base_Trace), recursive_compilation(_Quant, _Contraintes, _Base_Rec), equivalente_qcsp_base(Base_Trace, _Base_Rec).
% Base_Trace = bl([vlva(X,[0,1,2],[va(0),va(1),va(2)]),vlva(Y,[0,1,2],[va(0,ab(X,2,1,0)),va(1,ab(X,2))]),vlva(T,[0,1,2],[va(0,ab(X,(2,ab(Y,(1,ab(Z,2)))),(0,ab(Y,(0,ab(Z,0,1,2)))))),va(1,ab(X,(2,ab(Y,(1,ab(Z,1)))),(1,ab(Y,(0,ab(Z,0,1,2)))))),va(2,ab(X,(2,ab(Y,(1,ab(Z,0)),(0,ab(Z,0,1,2))))))])]) ? ;
% no

%% EAEE
% | ?-  _Quant = [e(X, [0,1,2]), a(Y, [0,1,2]), e(Z, [0,1,2]), e(T, [0,1,2])], _Contraintes = (X #= (Y*Z)+T), trace_search_qcsp(_Quant, _Contraintes, _Trace), construit_bl(_Quant, _Trace, Base_Trace), recursive_compilation(_Quant, _Contraintes, _Base_Rec), equivalente_qcsp_base(Base_Trace, _Base_Rec).
% Base_Trace = bl([vlva(X,[0,1,2],[va(0),va(1),va(2)]),vlva(Z,[0,1,2],[va(0,ab(X,(2,ab(Y,0,1,2)),(1,ab(Y,0,1,2)),(0,ab(Y,0,1,2)))),va(2,ab(X,(2,ab(Y,0,1)),(1,ab(Y,0)),(0,ab(Y,0)))),va(1,ab(X,(2,ab(Y,0,1,2)),(1,ab(Y,0,1)),(0,ab(Y,0))))]),vlva(T,[0,1,2],[va(0,ab(X,(2,ab(Y,(1,ab(Z,2)),(2,ab(Z,1)))),(1,ab(Y,(1,ab(Z,1)))),(0,ab(Y,(0,ab(Z,0,1,2)),(1,ab(Z,0)),(2,ab(Z,0)))))),va(1,ab(X,(2,ab(Y,(1,ab(Z,1)))),(1,ab(Y,(0,ab(Z,0,1,2)),(1,ab(Z,0)),(2,ab(Z,0)))))),va(2,ab(X,(2,ab(Y,(0,ab(Z,0,1,2)),(1,ab(Z,0)),(2,ab(Z,0))))))])]) ? ;
% no

%% AEEE
% | ?-  _Quant = [a(X, [0,1,2]), e(Y, [0,1,2]), e(Z, [0,1,2]), e(T, [0,1,2])], _Contraintes = (X #= (Y*Z)+T), trace_search_qcsp(_Quant, _Contraintes, _Trace), construit_bl(_Quant, _Trace, Base_Trace), recursive_compilation(_Quant, _Contraintes, _Base_Rec), equivalente_qcsp_base(Base_Trace, _Base_Rec).
% Base_Trace = bl([vlva(Y,[0,1,2],[va(2,ab(X,0,1,2)),va(1,ab(X,0,1,2)),va(0,ab(X,0,1,2))]),vlva(Z,[0,1,2],[va(1,ab(X,(0,ab(Y,0)),(1,ab(Y,0,1)),(2,ab(Y,0,1,2)))),va(0,ab(X,(0,ab(Y,0,1,2)),(1,ab(Y,0,1,2)),(2,ab(Y,0,1,2)))),va(2,ab(X,(0,ab(Y,0)),(1,ab(Y,0)),(2,ab(Y,0,1))))]),vlva(T,[0,1,2],[va(0,ab(X,(0,ab(Y,(0,ab(Z,0,1,2)),(1,ab(Z,0)),(2,ab(Z,0)))),(1,ab(Y,(1,ab(Z,1)))),(2,ab(Y,(1,ab(Z,2)),(2,ab(Z,1)))))),va(2,ab(X,(2,ab(Y,(0,ab(Z,0,1,2)),(1,ab(Z,0)),(2,ab(Z,0)))))),va(1,ab(X,(1,ab(Y,(0,ab(Z,0,1,2)),(1,ab(Z,0)),(2,ab(Z,0)))),(2,ab(Y,(1,ab(Z,1))))))])]) ? ;
% no

%% AEAE
% | ?-  _Quant = [a(X, [0,1,2]), e(Y, [0,1,2]), a(Z, [0,1,2]), e(T, [0,1,2])], _Contraintes = (X #= (Y*Z)+T), trace_search_qcsp(_Quant, _Contraintes, _Trace), construit_bl(_Quant, _Trace, Base_Trace), recursive_compilation(_Quant, _Contraintes, _Base_Rec), equivalente_qcsp_base(Base_Trace, _Base_Rec).
% Base_Trace = bl([vlva(Y,[0,1,2],[va(1,ab(X,2)),va(0,ab(X,0,1,2))]),vlva(T,[0,1,2],[va(0,ab(X,(0,ab(Y,(0,ab(Z,0,1,2)))),(2,ab(Y,(1,ab(Z,2)))))),va(1,ab(X,(1,ab(Y,(0,ab(Z,0,1,2)))),(2,ab(Y,(1,ab(Z,1)))))),va(2,ab(X,(2,ab(Y,(0,ab(Z,0,1,2)),(1,ab(Z,0))))))])]) ? ;
% no

%% AAEE
% | ?-  _Quant = [a(X, [0,1,2]), a(Y, [0,1,2]), e(Z, [0,1,2]), e(T, [0,1,2])], _Contraintes = (X #= (Y*Z)+T), trace_search_qcsp(_Quant, _Contraintes, _Trace), construit_bl(_Quant, _Trace, Base_Trace), recursive_compilation(_Quant, _Contraintes, _Base_Rec), equivalente_qcsp_base(Base_Trace, _Base_Rec).
% Base_Trace = bl([vlva(Z,[0,1,2],[va(1,ab(X,(0,ab(Y,0)),(1,ab(Y,0,1)),(2,ab(Y,0,1,2)))),va(0,ab(X,(0,ab(Y,0,1,2)),(1,ab(Y,0,1,2)),(2,ab(Y,0,1,2)))),va(2,ab(X,(0,ab(Y,0)),(1,ab(Y,0)),(2,ab(Y,0,1))))]),vlva(T,[0,1,2],[va(0,ab(X,(0,ab(Y,(0,ab(Z,0,1,2)),(1,ab(Z,0)),(2,ab(Z,0)))),(1,ab(Y,(1,ab(Z,1)))),(2,ab(Y,(1,ab(Z,2)),(2,ab(Z,1)))))),va(2,ab(X,(2,ab(Y,(0,ab(Z,0,1,2)),(1,ab(Z,0)),(2,ab(Z,0)))))),va(1,ab(X,(1,ab(Y,(0,ab(Z,0,1,2)),(1,ab(Z,0)),(2,ab(Z,0)))),(2,ab(Y,(1,ab(Z,1))))))])]) ? ;
% no

%| ?- _Domaine = [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40], _Quant = [e(W1, Domaine), e(W2, Domaine), e(W3, Domaine), e(W4, Domaine), a(F, Domaine), e(C1, [-1,0,1]), e(C2, [-1,0,1]), e(C3, [-1,0,1]), e(C4, [-1,0,1])], _Contraintes = (C1*W1 + C2*W2 + C3*W3 + C4*W4 #= F), trace_search_qcsp(_Quant, _Contraintes, _Trace), construit_bl(_Quant, _Trace, Base_Trace), recursive_compilation(_Quant, _Contraintes, _Base_Rec), equivalente_qcsp_base(Base_Trace, _Base_Rec).
% ! Resource error: insufficient memory


% | ?- _Quant = [e(W1, [3]), e(W2, [9]), e(W3, [27]), e(W4, [1,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40]), a(F, [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40]), e(C1, [-1,0,1]), e(C2, [-1,0,1]), e(C3, [-1,0,1]), e(C4, [-1,0,1])], _Contraintes = (C1*W1 + C2*W2 + C3*W3 + C4*W4 #= F), trace_search_qcsp(_Quant, _Contraintes, _Trace), construit_bl(_Quant, _Trace, Base_Trace), recursive_compilation(_Quant, _Contraintes, _Base_Rec), equivalente_qcsp_base(Base_Trace, _Base_Rec).
% Base_Trace = bl([vlva(W1,[3],[va(3)]),vlva(W2,[9],[va(9,ab(W1,3))]),vlva(W3,[27],[va(27,ab(W1,(3,ab(W2,9))))]),vlva(W4,[1,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40],[va(1,ab(W1,(3,ab(W2,(9,ab(W3,27))))))]),vlva(C1,[-1,0,1],[va(1,ab(W1,(3,ab(W2,(9,ab(W3,(27,ab(W4,(1,ab(F,2,3,4,11,12,13,20,21,22,29,30,31,38,39,40)))))))))),va(0,ab(W1,(3,ab(W2,(9,ab(W3,(27,ab(W4,(1,ab(F,1,8,9,10,17,18,19,26,27,28,35,36,37)))))))))),va(-1,ab(W1,(3,ab(W2,(9,ab(W3,(27,ab(W4,(1,ab(F,5,6,7,14,15,16,23,24,25,32,33,34))))))))))]),vlva(C2,[-1,0,1],[va(1,ab(W1,(3,ab(W2,(9,ab(W3,(27,ab(W4,(1,ab(F,(5,ab(C1,-1)),(6,ab(C1,-1)),(7,ab(C1,-1)),(8,ab(C1,0)),(9,ab(C1,0)),(10,ab(C1,0)),(11,ab(C1,1)),(12,ab(C1,1)),(13,ab(C1,1)),(32,ab(C1,-1)),(33,ab(C1,-1)),(34,ab(C1,-1)),(35,ab(C1,0)),(36,ab(C1,0)),(37,ab(C1,0)),(38,ab(C1,1)),(39,ab(C1,1)),(40,ab(C1,1)))))))))))),va(0,ab(W1,(3,ab(W2,(9,ab(W3,(27,ab(W4,(1,ab(F,(1,ab(C1,0)),(2,ab(C1,1)),(3,ab(C1,1)),(4,ab(C1,1)),(23,ab(C1,-1)),(24,ab(C1,-1)),(25,ab(C1,-1)),(26,ab(C1,0)),(27,ab(C1,0)),(28,ab(C1,0)),(29,ab(C1,1)),(30,ab(C1,1)),(31,ab(C1,1)))))))))))),va(-1,ab(W1,(3,ab(W2,(9,ab(W3,(27,ab(W4,(1,ab(F,(14,ab(C1,-1)),(15,ab(C1,-1)),(16,ab(C1,-1)),(17,ab(C1,0)),(18,ab(C1,0)),(19,ab(C1,0)),(20,ab(C1,1)),(21,ab(C1,1)),(22,ab(C1,1))))))))))))]),vlva(C3,[-1,0,1],[va(1,ab(W1,(3,ab(W2,(9,ab(W3,(27,ab(W4,(1,ab(F,(14,ab(C1,(-1,ab(C2,-1)))),(15,ab(C1,(-1,ab(C2,-1)))),(16,ab(C1,(-1,ab(C2,-1)))),(17,ab(C1,(0,ab(C2,-1)))),(18,ab(C1,(0,ab(C2,-1)))),(19,ab(C1,(0,ab(C2,-1)))),(20,ab(C1,(1,ab(C2,-1)))),(21,ab(C1,(1,ab(C2,-1)))),(22,ab(C1,(1,ab(C2,-1)))),(23,ab(C1,(-1,ab(C2,0)))),(24,ab(C1,(-1,ab(C2,0)))),(25,ab(C1,(-1,ab(C2,0)))),(26,ab(C1,(0,ab(C2,0)))),(27,ab(C1,(0,ab(C2,0)))),(28,ab(C1,(0,ab(C2,0)))),(29,ab(C1,(1,ab(C2,0)))),(30,ab(C1,(1,ab(C2,0)))),(31,ab(C1,(1,ab(C2,0)))),(32,ab(C1,(-1,ab(C2,1)))),(33,ab(C1,(-1,ab(C2,1)))),(34,ab(C1,(-1,ab(C2,1)))),(35,ab(C1,(0,ab(C2,1)))),(36,ab(C1,(0,ab(C2,1)))),(37,ab(C1,(0,ab(C2,1)))),(38,ab(C1,(1,ab(C2,1)))),(39,ab(C1,(1,ab(C2,1)))),(40,ab(C1,(1,ab(C2,1)))))))))))))),va(0,ab(W1,(3,ab(W2,(9,ab(W3,(27,ab(W4,(1,ab(F,(1,ab(C1,(0,ab(C2,0)))),(2,ab(C1,(1,ab(C2,0)))),(3,ab(C1,(1,ab(C2,0)))),(4,ab(C1,(1,ab(C2,0)))),(5,ab(C1,(-1,ab(C2,1)))),(6,ab(C1,(-1,ab(C2,1)))),(7,ab(C1,(-1,ab(C2,1)))),(8,ab(C1,(0,ab(C2,1)))),(9,ab(C1,(0,ab(C2,1)))),(10,ab(C1,(0,ab(C2,1)))),(11,ab(C1,(1,ab(C2,1)))),(12,ab(C1,(1,ab(C2,1)))),(13,ab(C1,(1,ab(C2,1))))))))))))))]),vlva(C4,[-1,0,1],[va(1,ab(W1,(3,ab(W2,(9,ab(W3,(27,ab(W4,(1,ab(F,(1,ab(C1,(0,ab(C2,(0,ab(C3,0)))))),(4,ab(C1,(1,ab(C2,(0,ab(C3,0)))))),(7,ab(C1,(-1,ab(C2,(1,ab(C3,0)))))),(10,ab(C1,(0,ab(C2,(1,ab(C3,0)))))),(13,ab(C1,(1,ab(C2,(1,ab(C3,0)))))),(16,ab(C1,(-1,ab(C2,(-1,ab(C3,1)))))),(19,ab(C1,(0,ab(C2,(-1,ab(C3,1)))))),(22,ab(C1,(1,ab(C2,(-1,ab(C3,1)))))),(25,ab(C1,(-1,ab(C2,(0,ab(C3,1)))))),(28,ab(C1,(0,ab(C2,(0,ab(C3,1)))))),(31,ab(C1,(1,ab(C2,(0,ab(C3,1)))))),(34,ab(C1,(-1,ab(C2,(1,ab(C3,1)))))),(37,ab(C1,(0,ab(C2,(1,ab(C3,1)))))),(40,ab(C1,(1,ab(C2,(1,ab(C3,1)))))))))))))))),va(0,ab(W1,(3,ab(W2,(9,ab(W3,(27,ab(W4,(1,ab(F,(3,ab(C1,(1,ab(C2,(0,ab(C3,0)))))),(6,ab(C1,(-1,ab(C2,(1,ab(C3,0)))))),(9,ab(C1,(0,ab(C2,(1,ab(C3,0)))))),(12,ab(C1,(1,ab(C2,(1,ab(C3,0)))))),(15,ab(C1,(-1,ab(C2,(-1,ab(C3,1)))))),(18,ab(C1,(0,ab(C2,(-1,ab(C3,1)))))),(21,ab(C1,(1,ab(C2,(-1,ab(C3,1)))))),(24,ab(C1,(-1,ab(C2,(0,ab(C3,1)))))),(27,ab(C1,(0,ab(C2,(0,ab(C3,1)))))),(30,ab(C1,(1,ab(C2,(0,ab(C3,1)))))),(33,ab(C1,(-1,ab(C2,(1,ab(C3,1)))))),(36,ab(C1,(0,ab(C2,(1,ab(C3,1)))))),(39,ab(C1,(1,ab(C2,(1,ab(C3,1)))))))))))))))),va(-1,ab(W1,(3,ab(W2,(9,ab(W3,(27,ab(W4,(1,ab(F,(2,ab(C1,(1,ab(C2,(0,ab(C3,0)))))),(5,ab(C1,(-1,ab(C2,(1,ab(C3,0)))))),(8,ab(C1,(0,ab(C2,(1,ab(C3,0)))))),(11,ab(C1,(1,ab(C2,(1,ab(C3,0)))))),(14,ab(C1,(-1,ab(C2,(-1,ab(C3,1)))))),(17,ab(C1,(0,ab(C2,(-1,ab(C3,1)))))),(20,ab(C1,(1,ab(C2,(-1,ab(C3,1)))))),(23,ab(C1,(-1,ab(C2,(0,ab(C3,1)))))),(26,ab(C1,(0,ab(C2,(0,ab(C3,1)))))),(29,ab(C1,(1,ab(C2,(0,ab(C3,1)))))),(32,ab(C1,(-1,ab(C2,(1,ab(C3,1)))))),(35,ab(C1,(0,ab(C2,(1,ab(C3,1)))))),(38,ab(C1,(1,ab(C2,(1,ab(C3,1))))))))))))))))])]) ? ;
% no