% RA: Relación 02
% OTTER: sumador.in
% Departamento de Ciencias de la Computación e Inteligencia Artificial
%==============================================================================


%==============================================================================
% Enunciado
%==============================================================================

% Diseñar un circuito lógico que implemente un sumador lógico de tres bits con
% componentes AND, OR y, como mucho, una única componente NOT.
%
%  Sumador de tres bits     Componente AND   Componente OR    Componente NOT
%
%     i1 i2 i3 | o1 o2        i1 i2 | o1       i1 i2 | o1        i1 | o1
%    ------------------      ------------     ------------      ---------
%     0  0  0  |  0  0        0  0  |  0       0  0  |  0        0  |  1
%     0  0  1  |  0  1        0  1  |  0       0  1  |  0        1  |  0
%     0  1  0  |  0  1        1  0  |  0       1  0  |  0
%     0  1  1  |  1  0        1  1  |  1       1  1  |  1
%     1  0  0  |  0  1
%     1  0  1  |  1  0
%     1  1  0  |  1  0
%     1  1  1  |  1  1

% Utilizar OTTER para encontrar una solución al problema.

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

set(auto2).

make_evaluable(_+_, $SUM(_,_)).
make_evaluable(_-_, $DIFF(_,_)).
make_evaluable(_<=_, $LE(_,_)).
make_evaluable(_>_, $GT(_,_)).

formula_list(sos).
 all x1 x2 x3 x4 x5 x6 x7 x8 yn y1 y2 y3 y4 y5 y6 y7 y8
  (salida([],x1,x2,x3,x4,x5,x6,x7,x8) &
   salida(yn,y1,y2,y3,y4,y5,y6,y7,y8) ->
   salida(yn,and(x1,y1),and(x2,y2),and(x3,y3),and(x4,y4),
             and(x5,y5),and(x6,y6),and(x7,y7),and(x8,y8))).

 all xn x1 x2 x3 x4 x5 x6 x7 x8 y1 y2 y3 y4 y5 y6 y7 y8
  (salida(xn,x1,x2,x3,x4,x5,x6,x7,x8) &
   salida(xn,y1,y2,y3,y4,y5,y6,y7,y8) ->
   salida(xn,and(x1,y1),and(x2,y2),and(x3,y3),and(x4,y4),
             and(x5,y5),and(x6,y6),and(x7,y7),and(x8,y8))).

 all x1 x2 x3 x4 x5 x6 x7 x8 yn y1 y2 y3 y4 y5 y6 y7 y8
  (salida([],x1,x2,x3,x4,x5,x6,x7,x8) &
   salida(yn,y1,y2,y3,y4,y5,y6,y7,y8) ->
   salida(yn,or(x1,y1),or(x2,y2),or(x3,y3),or(x4,y4),
             or(x5,y5),or(x6,y6),or(x7,y7),or(x8,y8))).

 all xn x1 x2 x3 x4 x5 x6 x7 x8 y1 y2 y3 y4 y5 y6 y7 y8
  (salida(xn,x1,x2,x3,x4,x5,x6,x7,x8) &
   salida(xn,y1,y2,y3,y4,y5,y6,y7,y8) ->
   salida(xn,or(x1,y1),or(x2,y2),or(x3,y3),or(x4,y4),
             or(x5,y5),or(x6,y6),or(x7,y7),or(x8,y8))).

 all x1 x2 x3 x4 x5 x6 x7 x8
  (salida([],x1,x2,x3,x4,x5,x6,x7,x8) ->
   salida([x1,x2,x3,x4,x5,x6,x7,x8],not(x1),not(x2),not(x3),not(x4),
                                    not(x5),not(x6),not(x7),not(x8))).

 salida([],0,0,0,0,1,1,1,1).
 salida([],0,0,1,1,0,0,1,1).
 salida([],0,1,0,1,0,1,0,1).

%  all b
%    (salida([],0,0,0,1,0,1,1,1) & salida(b,0,1,1,0,1,0,0,1) -> $ANS(b)).
% 
%  all a
%    (salida(a,0,0,0,1,0,1,1,1) & salida([],0,1,1,0,1,0,0,1) -> $ANS(a)).

 all a
   (salida(a,0,0,0,1,0,1,1,1) & salida(a,0,1,1,0,1,0,0,1) -> $ANS(a)).

 all x (and(x,0) = 0).
 all x (and(x,1) = x).
 all x (or(x,1) = 1).
 all x (or(x,0) = x).
 not(0) = 1.
 not(1) = 0.
end_of_list.

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