include "prolog.plz";

builtin(true).
builtin(false).
builtin(_ = _).
builtin(_ <= _).
builtin(_ > _).

sequence_tree(top, B, T) :-
   search_tree(B, T).

sequence_tree(bot, _T, bot).

sequence_tree(or(A0, B0), T, or(A1, B1)) :-
   sequence_tree(A0, T, A1),
   sequence_tree(B0, T, B1).

sequence_tree(constraint(C, T0), T, constraint(C, T1)) :-
   sequence_tree(T0, T, T1).


search_tree(A, T) :-
   print(A),nl,
   fail.
search_tree((A, B), T) :-
   search_tree(A, TA),
   sequence_tree(TA, B, T).

search_tree((A ; B), T) :-
   search_tree(A, TA),
   search_tree(B, TB),
   (
      TA == false,
      TB == false,
      T = bot
   ;
      TA == false,
      TB \= false,
      T = TB
   ;
      TA \= false,
      TB == false,
      T = TA
   ;
      TA \= false,
      TB \= false,
      T = or(TA, TB)
   ).
      
search_tree(B, T) :-
   builtin(B),
   (
      B == true,
      T = top
   ; 
      B == false,
      T = bot
   ;
      B \= true,
      B \= false,
      T = constraint(B, true)
   ).

search_tree(H, T) :-
   findall(B, clause(H, B), L),
   L \= [],
   disjunction(L, D),
   search_tree(D, T).


disjunction([], false).
disjunction([X], X).
disjunction([A, B | T], (A; C)) :-
   disjunction([B | T], C).

sbds(top, _).

sbds(or(A, B), Path) :-
   (
      A = constraint(C, A0),
      (
         C, sbds(A, [C | Path])
      ;
         cut_symmetry(C, Path), sbds(B, Path)
      )
   ;
      A \= constraint(_, _),
      (sbds(A, Path) ; sbds(B, Path))
   ).

sbds(constraint(C, T), Path) :-
   C, sbds(T, [C | Path]).