% RA: jarras.in
% Problema de las jarras de agua
% Departamento de Ciencias de la Computación e Inteligencia Artificial
% Universidad de Sevilla
%==============================================================================


%==============================================================================
% Formalización
%==============================================================================

set(binary_res).

formula_list(sos).
 % Operadores
 % Vaciar jarras
 % vaciar A
 all x y (jarras(x,y) -> jarras(0,y)).
 % vaciar B
 all x y (jarras(x,y) -> jarras(x,0)).
 % Llenar jarras
 % llenar A
 all x y (jarras(x,y) -> jarras(4,y)).
 % llenar B
 all x y (jarras(x,y) -> jarras(x,3)).

 % Vaciar una jarra en otra
 % vaciar A en B
 all x y (x+y > 3 & jarras(x,y) -> jarras(x+y-3,3)).
 % llenar B con A
 all x y (x+y <= 3 & jarras(x,y) -> jarras(0,x+y)).
 % vaciar B en A
 all x y (x+y > 4 & jarras(x,y) -> jarras(4,x+y-4)).
 % llenar A con B
 all x y (x+y <= 4 & jarras(x,y) -> jarras(x+y,0)).

 jarras(0,0).
 all x -jarras(2,x).
end_of_list.

%==============================================================================
