(* Package for manipulation of Boolean expressions as functions
of the built-in Mathematica True and False symbols. Version of 
12 October 1992. By Charles Wells, Department of Mathematics,
Case Western Reserve University, Cleveland OH 44106-7058, USA. 
Email: cfw2@po.cwru.edu. *)

(* Copyright 1992 by Charles F. Wells.  This package may be freely
distributed for noncommercial purposes provided that no changes
are made. *)

(* This package was developed with the support of the
Consolidated Natural Gas Company. *)

Off[General::spelll]

BeginPackage["Bool`"] 

TruthTable::usage = "TruthTable[e] produces the truth table of
the Boolean expression e.  Known bug:  The table header cuts off
right brackets from a nested expression.  The table itself is
correct."

Equivalent::usage = "p ~Equivalent~ q returns True if p and q have
the same truth value.  Otherwise it returns false.  This fills in
a gap in the functions supplied by Mathematica."

TautologyQ::usage = "TautologyQ[e] returns True if e is a Boolean
expression that is a tautology.  It returns False if it is a 
Boolean expression but not a tautology."

DNF::usage = "DNF[e] returns the Disjunctive Normal Form of the
Boolean expression e.  The form returned is a string, not an
expression, but ToExpression can be applied to it to make it an
expression."

CNF::usage = "CNF[e] returns the Conjunctive Normal Form of the
Boolean expression e.  The form returned is a string, not an
expression, but ToExpression can be applied to it to make it an
expression."

Begin["`private`"]

(* TT produces a list of all possible truth value combinations.
*)
TT[1] := {{True},{False}}

TT[n_ /; n>1] := T[n] =
  Join[Map[Prepend[#,True]&,TT[n-1]],
    Map[Prepend[#,False]&,TT[n-1]]]

SymbolQ[x_] := If[Head[x]==Symbol,True,False,False]

(* VariableSet extracts the set of variables in an expression. *)
VariableSet[e_] := 
   Select[Union[Level[e, {-1}]],SymbolQ]

MakeArgs[l_List] := StringReplace[ToString[l],
   {"," -> "_,","{" -> "[", "}" -> "_]"}]

(* MakeFunction defines the function f to have the value of the
expression e. *)
MakeFunction[e_,f_] := 
  ToExpression[StringJoin[f // ToString, 
     MakeArgs[VariableSet[e]],
     " := ", e // InputForm // HoldForm //ToString]]

Abb[True] := "T"
Abb[False] := "F"
SetAttributes[Abb,Listable]

TruthTable[e_] :=
  Module[{args = VariableSet[e],
    expr=InString[$Line],list,lbracket,rbracket,n,ff},
   (MakeFunction[e,ff];
    n = Length[args];
    lbracket=StringPosition[expr,"[",1][[1]][[1]];
    rbracket=StringPosition[expr,"]",1][[1]][[1]];
    list = MapThread[Join,
         {TT[n],Map[List[Apply[ff,#]]&,TT[n]]}] // Abb;
    list = Prepend[list,    
      Join[args,{StringTake[expr,{lbracket+1,rbracket-1}]}]];
    TableForm[list,
        TableAlignments-> Center,
        TableSpacing -> {0,2}])]

TruthList[f_, n_Integer /; n>0] :=
   Map[List[Apply[f,#]]&,TT[n]]

TautologyQ[e_] :=
 Module[{args = VariableSet[e],n,ff},
   (MakeFunction[e,ff];
    n = Length[args];
     Union[TruthList[ff,n]]=={{True}})]

Equivalent[p_,q_] := If[p,q,!q]

(* MakeAtom[b,c] takes a Boolean expression b and a string c
and returns the string c if b is true and the string !c if b
is false. *)
MakeAtom[{b_,c_String}] := If[b,c,"!"<>c]

(* SymbolicApply produces a string consisting of the entries of the
   list l with x between each pair of them. *)
SymbolicApply[l_List,x_String] := 
   Module[{n=Length[l]},
   Join[Map[StringJoin[#,x]&,
    Take[l,n-1]],{l[[n]]}] // StringJoin]

DNF[e_] :=
  Module[{args = Map[ToString,VariableSet[e]],
    expr=InString[$Line],list,n,ff},
    If[!TautologyQ[!(e)],
      (MakeFunction[e,ff];
      n = Length[args];
      list = 
        Map[Transpose[List[#,args]]&, Select[TT[n],Apply[ff,#]&]];
      list = Map[Map[MakeAtom,#]&,list];
         SymbolicApply[Map[
            StringJoin[ "(",SymbolicApply[#," && "],")"]&,list],
            " || "]
     ),"()"] (* End If *)
]
   
CNF[e_] :=
  Module[{args = Map[ToString,VariableSet[e]],
    expr=InString[$Line],list,n,ff},
    If[!TautologyQ[e],
      (MakeFunction[e,ff];
      n = Length[args];
      list = 
        Map[Transpose[List[Map[Not,#],args]]&,
           Select[TT[n],!Apply[ff,#]&]];
      list = Map[Map[MakeAtom,#]&,list];
         SymbolicApply[Map[
            StringJoin[ "(",SymbolicApply[#," || "],")"]&,list],
            " && "]
    ),"()"] (* End If *)
]
   
End[]

EndPackage[]