program PlaMin(input, output);
{
expr = prod + prod + prod + ... + prod
prod = term . term . term . ... . term
term = tag | (expr) | tag' | (expr)'
}

label
   777, 666, 9999, 8888;

type
   variables  = (va,vb,vc,vd,ve,vf,vg,vh,vi,vj,
                 vk,vl,vm,vn,vo,vp,vq,vr,vs,vt,vu,vv,vw,vx,vy,vz);
   SP         = ^data;
   data       = record
                   vars       : set of variables;
                   notvars    : set of variables;
                   next       : SP;
                   end {record P};

var
   tracing    : boolean;
   saved      : char;
   hangfire   : boolean;
   vlast      : variables;
   Expr       : SP;
   S          : ARRAY [0..15] OF SP;
   where      : integer;
   AlwaysTrue, AlwaysFalse: SP;
      {--------------------------------------------------------------------------}

procedure PrintS(s: SP);

var
   final, v          : variables;

begin
   if s=NIL then
      WriteLn('<NIL???>')
   else if s=AlwaysTrue then
      WriteLn('True')
   else if s=AlwaysFalse then
      WriteLn('False')
   else if (s^.vars=[]) and (s^.notvars=[]) then begin
      Write('True');
      end
   else begin
      final := vlast;
      while not((final in s^.vars) or (final in s^.notvars)) do begin
         final := PRED(final);
         end {while};
      for v := va to final do begin
         if v in s^.vars then begin
            (*Write('v', ORD(v));*)
            Write(CHR(ORD('a')+ORD(v)));
            if v <> final then
               Write('.');
            end {if};
         if v in s^.notvars then begin
            (*Write('v', ORD(v), '''');*)
            Write(CHR(ORD('a')+ORD(v)), '''');
            if v <> final then
               Write('.');
            end {if};
         end {for};
      end {if};
   end {PrintS};

procedure PrintSP(s: SP);
begin
   if s=NIL then
      Write('<NIL???>')
   else if s=AlwaysTrue then
      Write('True')
   else if s=AlwaysFalse then
      Write('False')
   else
      while s <> NIL do begin
         PrintS(s);
         if s^.next <> NIL then
            Write (' + ');
         s := s^.next;
         end {while};
   end {PrintSP};
{--------------------------------------------------------------------------}

procedure Concat(var head: SP; tail: SP);

var
   s          : SP;

begin
   if head=NIL then
      head := tail
   else begin
      s := head;
      while s^.next <> NIL do
         s := s^.next;
      s^.next := tail;
      end {if};
   end {Concat};

function CopyOf(expr: SP): SP;

var
   prod, result     : SP;

begin
   if expr=AlwaysTrue then
      result := AlwaysTrue
   else if expr=Alwaysfalse then
      result := AlwaysFalse
   else begin
      result := NIL;
      while expr <> NIL do begin
         NEW(prod);
         prod^.vars := expr^.vars;
         prod^.notvars := expr^.notvars;
         prod^.next := result;
         result := prod;
         expr := expr^.next;
         end {while};
      end {if};
   CopyOf := result;
   end {CopyOf};
{--------------------------------------------------------------------------}

procedure RemoveDups(var s: SP);

var
   expr1, expr2, set1, set2       : SP;

begin
   {------------------------    Cast out duplicates    ------------------------}
   { does it by clearing them to blanks - really ought to tidy up as well... }
   { However, this reduces the complexity somewhat }
   expr1 := s;
   while expr1 <> NIL do begin
      expr2 := expr1;
      set1 := expr1;
      while expr2 <> NIL do begin
         set2 := expr2;
         if (set1<>set2) and (set1^.vars=set2^.vars) and (set1^.notvars=set2^.notvars) 
         then begin
            if (set1^.vars <> []) or (set1^.notvars <> []) then begin
               if tracing then begin
                  Write('Apply  A + A = A to ');
                  PrintS(set1);
                  Write(' + ');
                  PrintS(set2);
                  WriteLn;
                  end {tracing};
               end {if};
            set1^.vars := [];
            set1^.notvars := [];
            end {if};
         expr2 := expr2^.next;
         end {while};
      expr1 := expr1^.next;
      end {while};
   end {RemoveDups};

function RemoveComplements(var s: SP): boolean;

label
   99;

var
   expr1, expr2      : SP;
   v          : variables;
   tot        : integer;

begin
   {----------------     Apply rule A + A' = AlwaysTrue    -----------------}
   { If any found, entire expression is also always true (a + TRUE + b... }
   expr1 := s;
   while expr1 <> NIL do begin
      { First extract all likely sets }
      tot := 0;
      for v := va to vlast do begin
         if v in expr1^.vars then
            tot := tot+1;
         if v in expr1^.notvars then
            tot := tot+1;
         end;
      if tot=1 then begin
         expr2 := expr1;
         while expr2<>NIL do begin
            if (expr2^.vars=expr1^.notvars) and
             (expr1^.vars=expr2^.notvars) then begin
               if tracing then begin
                  Write('Apply  A + A'' = True to ');
                  PrintS(expr1);
                  Write(' + ');
                  PrintS(expr2);
                  WriteLn(' = True');
                  end {tracing};
               {DISPOSESP(s)}
               s := AlwaysTrue;
               RemoveComplements := True;
               goto 99
               end {if};
            expr2 := expr2^.next;
            end {while};
         end {if};
      expr1 := expr1^.next;
      end {while};
   RemoveComplements := False;
   99: 
   end {RemoveComplements};

procedure Optimise(var s: SP);

label
   99;

var
   last, dummy, expr, expr1, expr2, set1, set2       : SP;
   intersection: set of variables;
   v          : variables;

begin
   if (s=AlwaysTrue) or (s=AlwaysFalse) then
      goto 99;
   if tracing then begin
      Write('Problem: reduce ');
      PrintSP(s);
      WriteLn;
      end {tracing};
   NEW(dummy);
   dummy^.vars := [];
   dummy^.notvars := [];
   dummy^.next := s;
   last := dummy;
   expr := s;
   {--------------     Apply rule X'.X = 0      ---------------------------}
   while expr <> NIL do begin
      if expr^.vars * expr^.notvars <> [] then begin
         last^.next := expr^.next;
         if tracing then begin
            Write('Apply A.A'' = False to ');
            PrintS(expr);
            WriteLn;
            end {tracing};
         end
      else begin
         last := expr;
         end {if};
      expr := last^.next;
      end {while};
   s := dummy^.next;
   DISPOSE(dummy);
   {----------------      Apply rule P.Q + P.Q' = P     --------------------}
   expr1 := s;
   while expr1 <> NIL do begin
      expr2 := expr1;
      set1 := expr1;
      while expr2 <> NIL do begin
         set2 := expr2;
         if not((set1^.vars=set2^.vars) and
                (set1^.notvars=set2^.notvars)) then begin
            intersection := set2^.notvars*set1^.vars;
            if (set1^.vars-intersection = set2^.vars) and
               (set1^.notvars = set2^.notvars-intersection) and
               (* A + A' !!! ... *) (set1^.vars<>intersection) then begin
               if tracing then begin
                  Write('Apply A.B + A.B'' = A to ');
                  PrintS(Set1);
                  Write(' + ');
                  PrintS(Set2);
                  end {tracing};
               set1^.vars := set1^.vars-intersection;
               set2^.vars := [];
               set2^.notvars := [];
               if tracing then begin
                  Write(' = ');
                  PrintS(Set1);
                  WriteLn;
                  end {tracing};
               end
            else begin
               intersection := set1^.notvars*set2^.vars;
               if (set2^.vars-intersection = set1^.vars) and
                  (set2^.notvars = set1^.notvars-intersection) and
                  (set2^.vars <> intersection) then begin
                  if tracing then begin
                     Write('Apply A''.B + A.B = B to ');
                     PrintS(Set2);
                     Write(' + ');
                     PrintS(Set1);
                     end {tracing};
                  set2^.vars := set2^.vars-intersection;
                  set1^.vars := [];
                  set1^.notvars := [];
                  if tracing then begin
                     Write(' = ');
                     PrintS(Set2);
                     WriteLn;
                     end {tracing};
                  end {if};
               end {if}
            end {if};
         expr2 := expr2^.next;
         end {while};
      expr1 := expr1^.next;
      end {while};
   RemoveDups(s);
   {----------------      Apply rule A + AB = A    --------------------}
   expr1 := s;
   while expr1 <> NIL do begin
      expr2 := expr1;
      set1 := expr1;
      while expr2 <> NIL do begin
         set2 := expr2;
         if (set1^.vars=[]) and (set1^.notvars=[]) then begin
            end
         else if (set2^.vars=[]) and (set2^.notvars=[]) then begin
            end
         else begin
            if not((set1^.vars=set2^.vars) and
                   (set1^.notvars=set2^.notvars)) then begin
               (* was set1<>set2 - may change back... *)
               if (set1^.vars*set2^.vars = set1^.vars) and
               (set1^.notvars*set2^.notvars = set1^.notvars) then begin
                  if tracing then begin
                     Write('Applyi A + AB = A to ');
                     PrintS(set1);
                     Write(' + (redundant) ');
                     PrintS(set2);
                     WriteLn;
                     end {tracing};
                  set2^.vars := [];
                  set2^.notvars := [];
                  end
               else if (set1^.vars*set2^.vars = set2^.vars) and
 { Anti-symmetric }
           (   set1^.notvars*set2^.notvars = set2^.notvars) then begin
                  if tracing then begin
                     Write('Apply A + AB = A to ');
                     PrintS(set2);
                     Write(' + (redundant) ');
                     PrintS(set1);
                     WriteLn;
                     end {tracing};
                  set1^.vars := [];
                  set1^.notvars := [];
                  end {if};
               end {if};
            end {if};
         expr2 := expr2^.next;
         end {while};
      expr1 := expr1^.next;
      end {while};
   RemoveDups(s);
   if RemoveComplements(s) then
      goto 99;
   {----------------      Apply rule A + A'B = A + B    --------------------}
   expr1 := s;
   while expr1 <> NIL do begin
      expr2 := expr1;
      set1 := expr1;
      while expr2 <> NIL do begin
         set2 := expr2;
         if set1 = set2 then begin
            end
         else if (set1^.vars=[]) and (set1^.notvars=[]) then begin
            end
         else if (set2^.vars=[]) and (set2^.notvars=[]) then begin
            end
         else begin
            if (set1^.vars<>set2^.vars) or (set1^.notvars<>set2^.notvars) then begin
               (* Lines below should be identical to those above - unfortunately,
               we may be suffering from a compiler bug...
               if not((set1^.vars=set2^.vars) and
               (set1^.notvars=set2^.notvars)) then begin
               *)
               for v := va to vlast do begin
                  if (v in set1^.vars) and (v in set2^.notvars) then begin
                     if ((set1^.vars-[v])*set2^.vars = set1^.vars-[v]) and
                        (set1^.notvars*set2^.notvars-[v]=set1^.notvars) then begin
                        if tracing then begin
                           Write('Apply) A + A''B = A + B to ');
                           PrintS(set1);
                           Write(' + ');
                           PrintS(set2);
                           end {tracing};
                        set2^.notvars := set2^.notvars-[v];
                        if tracing then begin
                           Write(' = ');
                           PrintS(set1);
                           Write(' + ');
                           PrintS(set2);
                           WriteLn;
                           end {tracing};
                        end;
                     end
                  else if (v in set1^.notvars) and (v in set2^.vars) then begin
                     if ((set1^.notvars-[v])*set2^.notvars = set1^.notvars-[v]) and
                        (set1^.vars*set2^.vars-[v]=set1^.vars) then begin
                        if tracing then begin
                           Write('Apply A'' + AB = A'' + B to ');
                           PrintS(set2);
                           Write(' + ');
                           PrintS(set1);
                           end {tracing};
                        set2^.vars := set2^.vars-[v];
                        if tracing then begin
                           Write(' = ');
                           PrintS(set1);
                           Write(' + ');
                           PrintS(set2);
                           WriteLn;
                           end {tracing};
                        end;
                     end {if};
                  if RemoveComplements(s) then
                     goto 99;
                  { Anti-symmetric }
                  if (v in set2^.vars) and (v in set1^.notvars) then begin
                     if ((set2^.vars-[v])*set1^.vars = set2^.vars-[v]) and
                        (set2^.notvars*set1^.notvars-[v]=set2^.notvars) then begin
                        if tracing then begin
                           Write('Apply A + A''B = A + B to ');
                           PrintS(set2);
                           Write(' + ');
                           PrintS(set1);
                           end {tracing};
                        set1^.notvars := set1^.notvars-[v];
                        if tracing then begin
                           Write(' = ');
                           PrintS(set2);
                           Write(' + ');
                           PrintS(set1);
                           WriteLn;
                           end {tracing};
                        end;
                     end
                  else if (v in set2^.notvars) and (v in set1^.vars) then begin
                     if ((set2^.notvars-[v])*set1^.notvars = set2^.notvars-[v]) and
                        (set2^.vars*set1^.vars-[v]=set2^.vars) then begin
                        if tracing then begin
                           Write('Apply A'' + AB = A'' + B to ');
                           PrintS(set1);
                           Write(' + ');
                           PrintS(set1);
                           end {tracing};
                        set1^.vars := set1^.vars-[v];
                        if tracing then begin
                           Write(' = ');
                           PrintS(set2);
                           Write(' + ');
                           PrintS(set1);
                           WriteLn;
                           end {tracing};
                        end;
                     end {if};
                  if RemoveComplements(s) then
                     goto 99;
                  end {for};
               end {if};
            end {if};
         expr2 := expr2^.next;
         end {while};
      expr1 := expr1^.next;
      end {while};
   RemoveDups(s);
   {------------------------    Cast out blanks    ------------------------}
   NEW(dummy);
   dummy^.vars := [];
   dummy^.notvars := [];
   dummy^.next := s;
   last := dummy;
   expr := s;
   while expr <> NIL do begin
      if (expr^.vars = []) and (expr^.notvars = []) then begin
         (*      WriteLn('Removing ''+ false'' from expression');*)
         last^.next := expr^.next;
         end
      else begin
         last := expr;
         end {if};
      expr := last^.next;
      end {while};
   s := dummy^.next;
   DISPOSE(dummy);
   if tracing then begin
      Write('Ans: ');
      PrintSP(s);
      WriteLn;
      end {tracing};
   99: 
       if s=NIL then
          s := AlwaysFalse;
   end {Optimise};

procedure AndTerm(var prod: SP; term: SP);

var
   result, temp, temp2      : SP;

begin
   if tracing then begin
      Write('Apply distributive law to (');
      PrintSP(term);
      Write(') . (');
      PrintSP(prod);
      Write(') = ');
      end {tracing};
   (*      tricky!!! A few NEWs here. Also, do we dispose args? *)
   if term=AlwaysTrue then
      result := prod
   else if term=AlwaysFalse then
      result := AlwaysFalse
   else if prod=AlwaysTrue then
      result := term
   else if prod=AlwaysFalse then
      result := AlwaysFalse
   else begin
      result := NIL;
      if prod=NIL then
         WriteLn('Warning - you are anding the empty set!');
      while term <> NIL do begin
         temp := CopyOf(prod);
         {perform AND operation into temp}
         temp2 := temp;
         while temp2 <> NIL do begin
            temp2^.vars := temp2^.vars+term^.vars;
            temp2^.notvars := temp2^.notvars+term^.notvars;
            temp2 := temp2^.next;
            end {while};
         Concat(result, temp);
         term := term^.next;
         end {while};
      end {if};
   prod := result;
   if tracing then begin
      Write(' = ');
      PrintSP(result);
      WriteLn;
      end {tracing};
   end {AndTerm};

function DeMorgan(prod: SP): SP;

var
   v          : variables;
   single,result     : SP;

begin
   (*  Optimise(prod);*) { Assert no Q and Q' in same cell... }
   (* temp remove *)
   (****** ARGH!!!! This is hellishly expensive. Should be simple test! *BUG**)
   if tracing then begin
      Write('Apply De-Morgan to (');
      PrintS(prod);
      Write(')''');
      end {tracing};
   if prod=AlwaysTrue then
      result := AlwaysFalse
   else if prod=AlwaysFalse then
      result := AlwaysTrue
   else begin
      result := NIL;
      for v := va to vlast do begin
         if v in prod^.notvars then begin
            NEW(single);
            single^.vars := [v];
            single^.notvars := [];
            single^.next := result;
            result := single;
            end
         else if v in prod^.vars then begin
            NEW(single);
            single^.notvars := [v];
            single^.vars := [];
            single^.next := result;
            result := single;
            end {if};
         end {for};
      end {if};
   DeMorgan := result;
   if tracing then begin
      Write(' = ');
      PrintSP(result);
      WriteLn;
      end {tracing};
   end {DeMorgan};

procedure Complement(var s: SP);

var
   expr, sum, prod, result     : SP;

begin
   if tracing then begin
      Write('Complement ');
      PrintSP(s);
      WriteLn;
      end {tracing};
   if s=AlwaysTrue then
      s := AlwaysFalse
   else if s=AlwaysFalse then
      s := AlwaysTrue
   else begin
      NEW(result);
      result^.vars := [];
      result^.notvars := [];
      result^.next := NIL;
      { kludge - ought to drop off }
      expr := s;
      while expr <> NIL do begin
         prod := expr;
         sum := DeMorgan(prod);
         AndTerm(result, sum);
         Optimise(result);
         { Probably redundant ??? - Worried, Croydon. }
         (*** TRY PUTTING THIS LINE IN - SEE IF IT HELPS ***BUG***)
         expr := expr^.next;
         end {while};
      s := result;
      end {if};
   if tracing then begin
      Write('Result of complementing is ');
      PrintSP(s);
      WriteLn;
      end {tracing};
   end {Complement};
{--------------------------------------------------------------------------}

function GetCh: char;

var
   ch         : char;

begin
   if eof then
      goto 9999
   else if hangfire then begin
      hangfire := false;
      ch := saved;
      end
   else if eoln then begin
      ch := ' ';
      Readln;
      end
   else
      Read(ch);
   GetCh := ch;
   end {GetCh};

procedure BackSpace(ch: char);
begin
   hangfire := true;
   saved := ch;
   end {backSpace};

function Parse(ch: char): boolean;

var
   c          : char;

begin
   repeat
      c := GetCh
   until c <> ' ';
   if c=ch then
      Parse := true
   else begin
      Parse := false;
      BackSpace(c);
      end {if};
   end {Parse};

function ParseTag: variables;

var
   c          : char;
   ordinal    : integer;
   v          : variables;

begin
   (*  if ((Parse('V')) or (Parse('v'))) then begin
   if Parse('0') then ParseTag := va
   else if Parse('1') then ParseTag := v1
   else if Parse('2') then ParseTag := v2
   else if Parse('3') then ParseTag := v3
   else if Parse('4') then ParseTag := v4
   else if Parse('5') then ParseTag := v5
   else if Parse('6') then ParseTag := v6;
   end [if]******;
   *)
   repeat
      c := GetCh
   until c <> ' ';
   if c in ['a'..'z'] then begin
      ordinal := ORD(c)-ORD('a');
      for v := va to vlast do begin
         if ORD(v)=ordinal then
            ParseTag := v;
         end {for};
      end
   else begin
      BackSpace(c);
      goto 666;
      end {if};

   end {ParseTag};
{--------------------------------------------------------------------------}

function ParseExpr: SP;
   forward;

function ParseTerm: SP;

var
   expr       : SP;
   term       : variables;

begin
   if Parse('(') then begin
      expr := ParseExpr;
      if Parse(')') then begin
         end
      else
         goto 666;
      while Parse('''') do begin
         Complement(expr);
         end {while};
      end
   else begin
      term := ParseTag;
      NEW(expr);
      expr^.next := NIL;
      if Parse('''') then begin
         expr^.notvars := [term];
         expr^.vars := [];
         end
      else begin
         expr^.vars := [term];
         expr^.notvars := [];
         end {if};
      end {if};
   ParseTerm := expr;
   end {ParseTerm};

function ParseProd: SP;

label
   1;

var
   term, prod       : SP;

begin
   prod := ParseTerm;
   while parse('.') do begin
      term := ParseTerm;
      if term=AlwaysFalse then begin
         {DISPOSESP(prod)}
         prod := AlwaysFalse;
         goto 1
         end;
      AndTerm(prod, term);
      { And the term with each element in prod }
      end {while};
   1: ParseProd := prod;
   end {ParseProd};

function ParseExpr{: SP};

label
   1;

var
   prod, result     : SP;

begin
   result := NIL;
   repeat
      prod := ParseProd;
      if prod=AlwaysTrue then begin
         {DISPOSESP(result)}
         result := AlwaysTrue;
         goto 1
         end;
      if prod <> AlwaysFalse then
         Concat(result, prod);
   until not Parse('+');
   1: Optimise(result);
   ParseExpr := result;
   end {ParseExpr};
{--------------------------------------------------------------------------}
begin
   { WriteLn('Please enter a boolean expression using + and . and ''');
   Writeln('Variables are single lower-case letters, e.g.');
   WriteLn('Terminate the expression with a ''?''');
   WriteLn('Expr: (a+(b.c'').(b+c))''?');
   } NEW(AlwaysTrue);
   NEW(AlwaysFalse);
   { The contents of these are NEVER looked at; only the pointers to them }
   hangfire := false;
   vlast := vz;
   goto 777;
   666: WriteLn ('Error - line ignored');
   ReadLn;
   hangfire := false;
   777: 
        tracing := false;
   where := 0;
   repeat
      Expr := ParseExpr;
      Optimise(Expr);
      {ARGH!!!!}
      PrintSP(Expr);
      if Parse('?') then begin
         WriteLn(' +');
         BackSpace('?');
         end
      else begin
         WriteLn(' ;');
         end;
      S[where] := Expr;
      where := where+1;
      {   Complement(expr);
      Optimise(Expr);
      Write('which is equivalent to ('); PrintSP(Expr); WriteLn(')''');
      }
   until not Parse('?');
   if Parse(';') then
      goto 8888
   else
      goto 666;
   9999: 
         WriteLn('end of file');
   8888: 
   end {PlaMin}.