(***********************************************************************
This file was generated automatically by the Mathematica front end.
It contains Initialization cells from a Notebook file, which typically
will have the same name as this file except ending in ".nb" instead of
".m".

This file is intended to be loaded into the Mathematica kernel using
the package loading commands Get or Needs.  Doing so is equivalent to
using the Evaluate Initialization Cells menu command in the front end.

DO NOT EDIT THIS FILE.  This entire file is regenerated automatically 
each time the parent Notebook file is saved in the Mathematica front end.
Any changes you make to this file will be overwritten.
***********************************************************************)

(* 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\[ADoubleDot]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`"]

(* loading the package "boolean.m" *)
(* probably you have to change the path here *) 
<< boolean`


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


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


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


(* Let t1 and t2 be product expressions. 
        If there ist exactly one literal which appears in t1 complemented and \
in t2 uncomplemented (or visa-
          verse) and all other literals of t1 and t2 are equal then add[t1,
        t2] gives the (ordered) product expression which is equivalent to t1||
    t2 *)
(* otherwise add[t1,t2] gives -1 *)   
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\[LessEqual]Length[help[[k]]],i++,
            
            For[j=1,j\[LessEqual]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\[Equal]{},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]\[Equal]i],{i,0,Length[d[[1]]]}];


apiQuine[p_Or]:=
    Module[{d=struct[ ToExpression[ DNF[p]]]/.Or\[Rule]List},
      quineHelp[d] /. List\[Rule]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\[Rule]False; 
        p1=p/.x\[Rule]True;
        LogicalExpand[\[Not]x\[And]apiReusch[p0]\[Or]x\[And]apiReusch[p1]\[Or]
            apiReusch[p0]\[And]apiReusch[p1]]];
apiReusch[p_And]=p;
apiReusch[p_Not]=p;
apiReusch[p_Symbol]=p;


(* consens[t1,t2,
      v] gives the consensusterm of the product expressions t1 and t2 with \
respect to the letter v *)
(* If this consensusterm does not exist this function is not evaluated *)
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\[LessEqual]Length[vs],i++,
          
          consensi=
            ReplaceList[
                    p1/.{Or\[Rule]List},{___,t1_,___,t2_,___}\[Rule]
                      consens[t1,t2,vs[[i]]]]//DeleteCases[#,Null]&//
                DeleteCases[#,consens[__]]& //DeleteCases[#,False]& ;
          p1=p1||(consensi/.{List\[Rule]Or}) // shorten;
          ];
        p1 /. List\[Rule]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\[Rule]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\[Rule](int\[Rule]True)]&,vars];
      If[terms\[Equal]{},vars /. List\[Rule]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\[Rule]And,
        OverBar\[Rule]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\[LessEqual]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_,___}\[Rule]v],
          ReplaceList[#,{___,!v_,___,v_,___}\[Rule]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]\[Equal]{}]:=(Cases[c,{True,_}]  // Flatten // 
          DeleteCases[#,True]&) /. List\[Rule]Or;
columnFactor[c_/;pivotalVar[c]\[NotEqual]{}]:=Module[{v,f0,f1},
      v=First[pivotalVar[c]];
      f0=c/.v\[Rule]True // DeleteCases[#,{False,_Integer}]&;
      f1=c/.v\[Rule]False // DeleteCases[#,{False,_Integer}]&;
      LogicalExpand[columnFactor[f0]&&columnFactor[f1]]
      ];


amsReusch[p1_,q1_]:=
    Module[{p=({p1} // unnice) /. {Or\[Rule]List} // Flatten,
        q=({q1} // unnice) /. {Or\[Rule]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\[Rule]List}  /. {And\[Rule]Or} /. {i_Integer:>
                p[[i]]}} // Flatten 
      ];
amsReusch[{},_]:={False};
amsReusch[{False},_]:={False};


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


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


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


OverBar[];


End[]
EndPackage[]