\( (*\ 
      Package\ for\ minimization\ of\ Boolean\ expressions\ as\ functions\ of\ the\ built - 
        in\ Mathematica\ True\ and\ False\ symbols . \ 
            Version\ of\ 12\ July\ 2000. \ By\ Johannes\ Gahleitner, \ 
      Veldner\ Str . \ 14, \ A\ 4120\ Neufelden, \ 
      Austria, 
Email : \ 
        johannes . gahleitner@jk . uni - 
          linz . ac . at\ *) 

\  (*\ 
      This\ package\ may\ be\ freely\ distributed\ *) 

 (*\ 
      This\ package\ was\ developed\ during\ a\ diploma\ thesis\ on\ the\ department\ of\ algebra, \ 
      stochastics\ and\ Knowledge - 
        based\ mathematical\ systems\ of\ the\ Johannes\ Kepler\ Universität\ Linz\ *) 

 (*\ 
      The\ package\ boolean . 
          m\ from\ Charles\ Wells\ is\ needed\ *) 


BeginPackage["boolmin`"]
\)
\(nice::usage = "nice[p] gives the boolean polynom p in a nice form (+ instead of ||, * instead of &&, OverBar instead of Not)"
\)
\(unnice::usage = "unnice[p] gives the boolean polynom p in  an  unnice form (|| instead  of +, && instead  of *, Not instead  of OverBar)"
\)
\(dual::usage = "dual[p] gives the dual of the boolean polynom p"
\)
\(apiQuine::usage = "apiQuine[p] gets the sum of all prime implicants of the SOP-expression p with the Quine-McCluscey method"\ 
\)
apiReusch::usage = "apiReusch[p] gets the sum of all prime implicants \
of the SOP-expression p with the Reusch method" 

\(apiConsensus::usage = "apiConsensus[p] gets the sum of all prime implicants of the SOP-expression p with the consensus method"\ 
\)
\(apiNelson::usage = "apiNelson[p] gets the sum of all prime implicants of the boolean polynom p with the method of direct multiplication"\ 
\)
amsReusch::usage = "Let p be the set of all prime implikants of some \
boolean Polynom f and q a set of productterms such that the sum of these \
productterms is equivalent to f. Then amsReusch[p,q] gets the set of all \
irredundant SOP-expressions, which are equivalent to \
f"

minDisForm::usage = "minDisForm[p] gives a minimal SOP-expression, \
which is equivalent to p"
minConForm::usage = "minConForm[p] gives a minimal POS-expression, \
which is equivalent to p"

dontCareMin::usage = "Let p and q two SOP-expressions with p => q. \
Then dontCareMin[p,q] gives the set of all don\.b4t-care-iredundants \
SOP-expressions with respect to p and q"

\(OverBar::usage = "OverBar is a help function to make OverBar puplic"



\)
Begin["`private`"]

  
   
<<  
      boolean`


nice[p_] := 
        p /. {And -> Times, Or -> Plus, 
            Not -> OverBar};
unnice[p_] := 
        p /. {Times -> And, Plus -> Or, 
            OverBar -> 
              Not};


 (* vars[
          p] gives a list of all letters of the boolean expression p *)  
vars[
          p_] := Union[
                  Flatten[
                    p  /.  {Times -> List, Plus -> List, 
                        OverBar -> List, And -> List, 
                        Or -> List, Not -> List}]]  //  
                DeleteCases[#, "-"] &  //  
              DeleteCases[#, _Integer] & //  
            DeleteCases[#, True] &  //  
          DeleteCases[#, False] &;
vars[p_Symbol] := {p};
\(vars[True] := {}; \ 
    vars[False] := {};


 (*\ 
      literals[p]\ gives\ a\ list\ of\ all\ literals\ of\ the\ boolean\ expression\ p\ *) \)
literals[
          p_] := Union[
                Flatten[
                  p  /.  {Times -> List, Plus -> List, 
                      And -> List, Or -> List}]]  //  
              DeleteCases[#, "-"] &  //  
            DeleteCases[#, True] &  //  
          DeleteCases[#, False] &;
literals[p_Symbol] := {p};
literals[! p_Symbol] := {! p};
literals[True] := {};  
    literals[False] := {};


dual[p_] := 
        p  /. {And -> Or, Or -> And, 
            v_  /;  MemberQ[vars[p], 
                  v] -> ! v};
dual[True] = False;
dual[False] = 
        True;


  
     
add[t1_And, t2_And] := 
        Module[{c1 = Complement[t1, t2], c2 = Complement[t2, t1]}, 
          If[SameQ[c1, ! c2], 
            DeleteCases[t1, c1], -1]];
add[! x_, x_] := True;
add[x_, ! x_] := True;
\(\(add[_, _] := \(-1\);\)


 (*\ 
      Then\ quineHelp[
          d]\ gives\ the\ list\ of\ all\ prime\ Implicants\ of\ the\ polynom\ you\ get\ when\ you\ sum\ all\ product\ expressions\ contained\ in\ d\ *) \ \)
quineHelp[d_] := 
        Module[{ help = Map[{#, False} &, d, {2}], 
            newImpl = Table[{}, {i, 1, Length[d]}], a, newPrims, k, i, 
            j}, 
For[k = 1, 
            k < Length[help], k++, 
For[i = 1, 
                i ≤ 
                  Length[help[[k]]], i++, 
For[
                    j = 1, j ≤ Length[help[[k + 1]]], j++, 
                    a = add[help[[k, i, 1]], 
                        help[[k + 1, j, 
                            1]]];   
If[! IntegerQ[
                          a], newImpl[[k]] = 
                        Append[newImpl[[k]], a]; 
                      help[[k, i, 2]] = True; 
                      help[[k + 1, j, 2]] = 
                        True;];
];
];
]; 
newPrims = Cases[help, {_, False}, 
                  2] // Flatten  // 
              DeleteCases[#, False] &; 
If[
            newImpl == {}, 
            newPrims, 
Union[newPrims, 
              quineHelp[
                Map[Union, 
                  newImpl]]]]
];
quineHelp[{f_}] := f;
\(\(quineHelp[{{} ... }] := {};\)


 (*\ Length[
          t]\ gives\ the\ number\ of\ uncomplemented\ literals\ of\ the\ product\ expression\ t\ *) \)
ones[t_] := 
        Length[t] - 
          Count[t, ! _];


 (* 
      Let d be a list of minterms with n letters *) 
\(\(struct[d_] := 
        Table[Cases[d, t_ /; ones[t] == i], {i, 0, 
            Length[d[\([1]\)]]}];\)

\)
apiQuine[p_Or] := 
        Module[{d = struct[ ToExpression[ DNF[p]]] /. Or -> List}, 
          quineHelp[d]  /.  List -> Or];
apiQuine[p_And] = p;
apiQuine[p_Not] = p;
apiQuine[p_Symbol] = 
        p;


apiReusch[p_Or] := apiReusch[p] = 
          Module[{x = vars[p]  // First, p0, p1}, 
p0 = 
              p /. x -> False;  
p1 = 
              p /. x -> 
                  True; 
LogicalExpand[¬ x ∧ 
                  apiReusch[p0] ∨ x ∧ apiReusch[p1] ∨ 
                apiReusch[p0] ∧ apiReusch[p1]]];
apiReusch[p_And] = p;
apiReusch[p_Not] = p;
apiReusch[p_Symbol] = 
        p;


  
  
consens[t1_And, t2_And, v_] := 
        If[MemberQ[t1, v] && MemberQ[t2, ! v] || 
            MemberQ[t1, ! v] && MemberQ[t2, v], 
          LogicalExpand[
            DeleteCases[t1, v | ! v] && 
              DeleteCases[t2, v | ! v]]];
consens[v_, t2_And, v_] := 
        If[MemberQ[t2, ! v], DeleteCases[t2, ! v]];
consens[t1_And, v_, v_] := 
        If[MemberQ[t1, ! v], 
          DeleteCases[t1, ! v]];
consens[! v_, t2_And, v_] := 
        If[MemberQ[t2, v], DeleteCases[t2, v]];
consens[t1_And, ! v_, v_] := 
        If[MemberQ[t1, v], DeleteCases[t1, v]];
consens[! v_, v_, v_] := True;
\(\(consens[v_, \(! v_\), v_] := 
        True;\)


 (*\ 
      shorten[p]\ shortens\ p\ with\ the\ absorption\ law\ *) \)
shorten[p_] := 
        LogicalExpand[
          p];


apiConsensus[p_] := apiConsensus[p] = 
          Module[{vs, p1, i, consensi, help}, 
p1 = 
              shorten[p]; 
            vs = vars[p1]; 
For[i = 1, 
              i ≤ 
                Length[vs], i++, 
consensi = ReplaceList[p1 /. {Or -> List}, {___, t1_, ___, t2_, ___} -> 
                          consens[t1, t2, vs[[i]]]] // 
                      DeleteCases[#, Null] & // 
                    DeleteCases[#, consens[__]] &  // 
                  DeleteCases[#, False] & ; 
p1 = 
                p1 || (consensi /. {List -> Or})  //  
                  shorten;
]; 
p1  /.  
              List -> 
                Or
];


 (* 
      f is a list of SOP - expressions *) 
 (* 
      logicalMult[
          f] gives the product of all elements of f *) 
logicalMult[f_] := logicalMult[f] = 
          Module[{half = 
                Quotient[Length[f], 2]}, 
logicalMult[
                  Take[f, half]] && 
                logicalMult[Take[f, {half + 1, Length[f]}]] // 
              LogicalExpand];
logicalMult[{e_}] := logicalMult[{e}] = 
          e;
logicalMult[e_Not] := e;
logicalMult[e_Or] := e;
logicalMult[e_Symbol] := 
        e;


apiNelson[p_] := 
        Module[{conForm = (LogicalExpand[Not[p]] //  dual)} , 
          logicalMult[
            conForm  /.  {And -> 
                  List}]]; 


 (* 
      c is a list of SOP - 
        expressions where all literals are uncomplemented *) 
 (* 
      cnfShort gives the product of the elements of c *) 
\(\(cnfShort[c_] := 
        Module[{vars = DeleteCases[c\ , _Or]\  // Union, 
            terms = Cases[c, _Or] // Union, rule}, 
rule = 
            Map[Replace[#, int_Integer -> \((int -> True)\)] &, 
              vars]; If[terms == {}, 
            vars\  /. \ List -> 
                And, 
\(Append[
                  vars, \((terms /. rule\ \  // logicalMult)\)] // Flatten\) // 
              logicalMult]];\)


 (*\ 
      p\ and\ q\ are\ product\ expressions\ *) 
 (*\ 
      otherwise\ ratio[p, 
          q]\ gives\ the\ product\ of\ all\ literals\ that\ appear\ in\ p\ but\ not\ in\ p\ but\ not\ in\ q\ *) \)
ratio[p_, q_] := 
        Complement[literals[p] , literals[q]]  /.  {List -> And, 
            OverBar -> Not};
ratio[ ___  && 
            v_ && ___, ___ && ! v_ && ___] := "-"; 
\(\(ratio[\ ___ && \(! v_\) && ___, ___ && 
            v_ && ___] := "-";\)


 (*\ c\ is\ a\ list\ of\ product\ expressions\ *) 
 (*\ 
      isMonoform[v, 
          c]\ returns\ True\ iff\ the\ letter\ v\ appers\ is\ c\ either\ complemented\ or\ uncomplemented\ *) \)
\(\(isMonoform[v_, c_] := 
        Xor[MemberQ[literals[c], v], 
          MemberQ[literals[
              c], \(! v\)]];\)


 (*\ 
      drop[v, a]\ gives\ a\ dash\ iff\ the\ letter\ v\ is\ contained\ in\ the\ product\ expression\ a\ *) \)
drop[v_, a_] := a; 
drop[v_, ___  && v_ &&  ___] := "-";
drop[v_, ___  && ! v_  && ___] := "-";
drop[v_, v_] := "-";
\(\(drop[
          v_, \(! v_\)] := "-";\)


 (*\ c\ is\ a\ list\ of\ product\ expressions\ *) 
 (*\ 
      dropMonoformVariables[
          c]\ replaces\ repeated\ all\ product\ terms\ with\ monoform\ variables\ with\ dash\ *) \ \)
\(\(dropMonoformVariables[c_] := 
        Module[{vs, help}, 
vs = 
            vars[c]; \ 
For[i = 1, 
            i ≤ 
              Length[vs], \(i++\), 
\(If[
                isMonoform[vs[\([i]\)], c], 
                help = Map[drop[vs[\([i]\)], #] &, c]; \ 
                Return[dropMonoformVariables[
                    help]]];\)
]; 
Return[
            c];
];\)


 (*\ 
      c\ is\ a\ list\ *) 
 (*\ 
      index[c]\ replaces\ all\ elements\ e\ of\ c\ by\ a\ list\ with\ the\ elements\ e\ and\ the\ position\ *) \ \)
\(\(index[c_] := 
        Inner[List, c, Table[i, {i, 1, Length[c]}], 
          List];\)

 (*\ 
      c\ is\ a\ boolean\ expression\ or\ a\ list\ of\ boolean\ expressions\ *) 
 (*\ 
      pivotalVar[
          c]\ gives\ all\ letters\ which\ appear\ in\ c\ complemented\ and\ uncomplemented\ *) \)
\(\(pivotalVar[c_] := 
        literals[c]\  // \ 
          Union[ReplaceList[#, {___, v_, ___, \(! v_\), ___} -> v], 
              ReplaceList[#, {___, \(! v_\), ___, v_, ___} -> 
                  v]] &;\)

 (*\ 
      c\ is\ of\ the\ form\ {{p1, pos1},  ... , {pn, 
            posn}}\ where\ the\ pi\ are\ produktexpressions\ and\ the\ posi\ are\ natural\ numbers\ which\ represent\ the\ indezes\ in\ the\ column\ *) 
 (*\ 
      Then\ columnFactor[
          c]\ gives\ the\ columnFactor\ of\ the\ column\ with\ the\ entries\ p1, p2,  ... , pn\ *) \)
columnFactor[
          c_  /;  pivotalVar[
                c] == {}] := (Cases[c, {True, _}]   //  
                Flatten  //  DeleteCases[#, True] &)  /.  
          List -> Or;
\(\(columnFactor[c_ /; pivotalVar[c] ≠ {}] := 
        Module[{v, f0, f1}, 
v = 
            First[pivotalVar[c]]; 
f0 = 
            c /. v -> True\  // \ 
              DeleteCases[#, {False, _Integer}] &; 
f1 = 
            c /. v -> False\  // \ 
              DeleteCases[#, {False, _Integer}] &; 
LogicalExpand[
            columnFactor[f0] && 
              columnFactor[
                f1]]
];\)

\)
amsReusch[p1_, q1_] := 
        Module[{p = ({p1}  //  unnice)  /.  {Or -> List}  //  
                Flatten, 
            q = ({q1}  //  unnice)  /.  {Or -> List}  //  
                Flatten, tab1, tab2, pettrick, i}, 
tab1 = 
            Outer[ratio, p, q , 1]; 
tab2 = 
            Map[dropMonoformVariables[#] &, 
              Transpose[tab1]]; 
tab1 = 
            Map[DeleteCases[index[#], {"-", _Integer}] &, 
              tab2]; 
pettrick = 
            cnfShort[
              Map[columnFactor[#] &, tab1]]; 
ClearAll[
            i]; 
{pettrick  /.  {Or -> 
                        List}   /.  {And -> 
                      Or}  /.  {i_Integer :> p[[i]]}}  //  
            Flatten 
];
amsReusch[{}, _] := {False};
\(\(amsReusch[{False}, _] := {False};\)

\)
minDisForm[p_] := 
        Module[{prims = ({apiReusch[LogicalExpand[p]]}  /.  
                    Or -> List)  // Flatten}, 
          amsReusch[prims, prims]  //  
            First];


minConForm[p_] := 
        minDisForm[LogicalExpand[! p]]  //  
          dual;


dontCareMin[pl_, pu_] := 
        Module[{prims = {apiReusch[pu] /. Or -> List}  //  Flatten}, 
          amsReusch[
            prims, {pl /. Or -> List}  //  
              Flatten]];


OverBar[];


End[]
EndPackage[]