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}.