:- use_module('SEARCH_BL_QBF',[search_bl_qbf/3]).
:- use_module(library(clpb)).

% MON EXEMPLE : ( (C + B) * (B =< ((C =< D) * (C + (A =:= ~D))) ) )

% | ?- search_bl_qbf([e(A),e(B),e(C),e(D)], ( (C + B) * (B =< ((C =< D) * (C + (A =:= ~D))) ) ), Base).
% Base = bl([e(A),e(B),e(C),e(D)],[(1,1),(~A*1+(A*1+0),~A*1+(A*1+0)),(~B*(~A*1)+(~B*(A*1)+(B*(~A*1)+(B*(A*1)+0))),B*(~A*1)+(B*(A*1)+0)),(C*(~B*(~A*1))+(C*(~B*(A*1))+(~C*(B*(~A*1))+(C*(B*(~A*1))+(C*(B*(A*1))+0)))),C*(~B*(~A*1))+(~C*(B*(A*1))+(C*(~B*(A*1))+0)))]) ? ;
% no

% | ?- search_bl_sat([A,B,C,D], ( (C + B) * (B =< ((C =< D) * (C + (A =:= ~D))) ) ), Base).
% Base = bl([A,B,C,D],[(1,1),(~A*1+(A*1+0),~A*1+(A*1+0)),(~B*(~A*1)+(~B*(A*1)+(B*(~A*1)+(B*(A*1)+0))),B*(~A*1)+(B*(A*1)+0)),(C*(~B*(~A*1))+(C*(~B*(A*1))+(~C*(B*(~A*1))+(C*(B*(~A*1))+(C*(B*(A*1))+0)))),C*(~B*(~A*1))+(~C*(B*(A*1))+(C*(~B*(A*1))+0)))]) ? ;
% no

% | ?- search_bl_qbf([a(A),e(B),a(C),e(D)], ( (C + B) * (B =< ((C =< D) * (C + (A =:= ~D))) ) ), Base).
% Base = bl([a(A),e(B),a(C),e(D)],[(1,1),(~A*1+(A*1+0),0),(B*(~A*1)+(B*(A*1)+0),B*(~A*1)+(B*(A*1)+0)),(~C*(B*(~A*1))+(C*(B*(~A*1))+(C*(B*(A*1))+0)),~C*(B*(A*1))+0)]) ? ;
% no

% EXEMPLE BENEDETTI : AaAbEcAdEeEf (~b + e + f) * (a + c + f) * (a + d + e) * (~a + ~b + ~d + e) * (~a + b  + ~c) * (~a + ~c + ~f) * (a + ~d + ~e) * (~a + d + ~e) * (a + ~e + ~f)

% | ?- search_bl_qbf([a(A),a(B),e(C),a(D),e(E),e(F)], ((~B + E + F) * (A + C + F) * (A + D + E) * (~A + ~B + ~D + E) * (~A + B  + ~C) * (~A + ~C + ~F) * (A + ~D + ~E) * (~A + D + ~E) * (A + ~E + ~F)), Base).
% Base = bl([a(A),a(B),e(C),a(D),e(E),e(F)],[(1,1),(~A*1+(A*1+0),~A*1+(A*1+0)),(~B*(~A*1)+(B*(~A*1)+0),~B*(A*1)+(B*(A*1)+0)),(C*(~B*(~A*1))+(~C*(~B*(A*1))+(C*(B*(~A*1))+(~C*(B*(A*1))+0))),C*(~B*(~A*1))+(~C*(~B*(A*1))+(C*(B*(~A*1))+(~C*(B*(A*1))+0)))),(~D*(C*(~B*(~A*1)))+(~D*(C*(B*(~A*1)))+(D*(~C*(~B*(A*1)))+(D*(~C*(B*(A*1)))+0))),D*(C*(~B*(~A*1)))+(~D*(~C*(~B*(A*1)))+(D*(~C*(~B*(A*1)))+(D*(C*(B*(~A*1)))+(~D*(~C*(B*(A*1)))+0))))),(~E*(D*(C*(~B*(~A*1))))+(~E*(~D*(~C*(~B*(A*1))))+(~E*(D*(~C*(~B*(A*1))))+(E*(D*(~C*(~B*(A*1))))+(~E*(D*(C*(B*(~A*1))))+(~E*(~D*(~C*(B*(A*1))))+(E*(D*(~C*(B*(A*1))))+0)))))),~E*(D*(C*(~B*(~A*1))))+(E*(~D*(C*(~B*(~A*1))))+(~E*(~D*(~C*(~B*(A*1))))+(~E*(D*(~C*(~B*(A*1))))+(E*(D*(~C*(~B*(A*1))))+(E*(~D*(C*(B*(~A*1))))+(E*(D*(~C*(B*(A*1))))+0)))))))]) ? ;
% no

% | ?- _E = (~A * B), _F = (~A * ~B), _G = (B * A), _H = (~B * A), _I = (C * ~D), _J = (C * D), _K = (~D * ~C), _L = (D * ~C), search_bl_qbf([e(A),e(B),e(C),e(D)], (((_E+_H)*(_J+_K))+((_F+_G)*(_I+_L))), Base).
% Base = bl([e(A),e(B),e(C),e(D)],[(1,1),(~A*1+(A*1+0),~A*1+(A*1+0)),(~B*(~A*1)+(~B*(A*1)+(B*(~A*1)+(B*(A*1)+0))),~B*(~A*1)+(~B*(A*1)+(B*(~A*1)+(B*(A*1)+0)))),(~C*(~B*(~A*1))+(C*(~B*(A*1))+(C*(B*(~A*1))+(~C*(B*(A*1))+0))),C*(~B*(~A*1))+(~C*(~B*(A*1))+(~C*(B*(~A*1))+(C*(B*(A*1))+0))))]) ? ;
% no