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