# File prop_logic.ML

    (*  Title:      HOL/Tools/prop_logic.ML
        ID:         $Id: prop_logic.ML,v 1.11 2005/07/26 12:14:13 webertj Exp $
        Author:     Tjark Weber
        Copyright   2004-2005

    Formulas of propositional logic.
    *)

    signature PROP_LOGIC =
    sig
    	datatype prop_formula =
    		  True
    		| False
    		| BoolVar of int  (* NOTE: only use indices >= 1 *)
    		| Not of prop_formula
    		| Or of prop_formula * prop_formula
    		| And of prop_formula * prop_formula

    	val SNot     : prop_formula -> prop_formula
    	val SOr      : prop_formula * prop_formula -> prop_formula
    	val SAnd     : prop_formula * prop_formula -> prop_formula
    	val simplify : prop_formula -> prop_formula  (* eliminates True/False and double-negation *)

    	val indices : prop_formula -> int list  (* set of all variable indices *)
    	val maxidx  : prop_formula -> int       (* maximal variable index *)

    	val exists      : prop_formula list -> prop_formula  (* finite disjunction *)
    	val all         : prop_formula list -> prop_formula  (* finite conjunction *)
    	val dot_product : prop_formula list * prop_formula list -> prop_formula

    	val nnf    : prop_formula -> prop_formula  (* negation normal form *)
    	val cnf    : prop_formula -> prop_formula  (* conjunctive normal form *)
    	val auxcnf : prop_formula -> prop_formula  (* cnf with auxiliary variables *)
    	val defcnf : prop_formula -> prop_formula  (* definitional cnf *)

    	val eval : (int -> bool) -> prop_formula -> bool  (* semantics *)
    end;

    structure PropLogic : PROP_LOGIC =
    struct

    (* ------------------------------------------------------------------------- *)
    (* prop_formula: formulas of propositional logic, built from Boolean         *)
    (*               variables (referred to by index) and True/False using       *)
    (*               not/or/and                                                  *)
    (* ------------------------------------------------------------------------- *)

    	datatype prop_formula =
    		  True
    		| False
    		| BoolVar of int  (* NOTE: only use indices >= 1 *)
    		| Not of prop_formula
    		| Or of prop_formula * prop_formula
    		| And of prop_formula * prop_formula;

    (* ------------------------------------------------------------------------- *)
    (* The following constructor functions make sure that True and False do not  *)
    (* occur within any of the other connectives (i.e. Not, Or, And), and        *)
    (* perform double-negation elimination.                                      *)
    (* ------------------------------------------------------------------------- *)

    	(* prop_formula -> prop_formula *)

    	fun SNot True     = False
    	  | SNot False    = True
    	  | SNot (Not fm) = fm
    	  | SNot fm       = Not fm;

    	(* prop_formula * prop_formula -> prop_formula *)

    	fun SOr (True, _)   = True
    	  | SOr (_, True)   = True
    	  | SOr (False, fm) = fm
    	  | SOr (fm, False) = fm
    	  | SOr (fm1, fm2)  = Or (fm1, fm2);

    	(* prop_formula * prop_formula -> prop_formula *)

    	fun SAnd (True, fm) = fm
    	  | SAnd (fm, True) = fm
    	  | SAnd (False, _) = False
    	  | SAnd (_, False) = False
    	  | SAnd (fm1, fm2) = And (fm1, fm2);

    (* ------------------------------------------------------------------------- *)
    (* simplify: eliminates True/False below other connectives, and double-      *)
    (*      negation                                                             *)
    (* ------------------------------------------------------------------------- *)

    	(* prop_formula -> prop_formula *)

    	fun simplify (Not fm)         = SNot (simplify fm)
    	  | simplify (Or (fm1, fm2))  = SOr (simplify fm1, simplify fm2)
    	  | simplify (And (fm1, fm2)) = SAnd (simplify fm1, simplify fm2)
    	  | simplify fm               = fm;

    (* ------------------------------------------------------------------------- *)
    (* indices: collects all indices of Boolean variables that occur in a        *)
    (*      propositional formula 'fm'; no duplicates                            *)
    (* ------------------------------------------------------------------------- *)

    	(* prop_formula -> int list *)

    	fun indices True             = []
    	  | indices False            = []
    	  | indices (BoolVar i)      = [i]
    	  | indices (Not fm)         = indices fm
    	  | indices (Or (fm1, fm2))  = (indices fm1) union_int (indices fm2)
    	  | indices (And (fm1, fm2)) = (indices fm1) union_int (indices fm2);

    (* ------------------------------------------------------------------------- *)
    (* maxidx: computes the maximal variable index occuring in a formula of      *)
    (*      propositional logic 'fm'; 0 if 'fm' contains no variable             *)
    (* ------------------------------------------------------------------------- *)

    	(* prop_formula -> int *)

    	fun maxidx True             = 0
    	  | maxidx False            = 0
    	  | maxidx (BoolVar i)      = i
    	  | maxidx (Not fm)         = maxidx fm
    	  | maxidx (Or (fm1, fm2))  = Int.max (maxidx fm1, maxidx fm2)
    	  | maxidx (And (fm1, fm2)) = Int.max (maxidx fm1, maxidx fm2);

    (* ------------------------------------------------------------------------- *)
    (* exists: computes the disjunction over a list 'xs' of propositional        *)
    (*      formulas                                                             *)
    (* ------------------------------------------------------------------------- *)

    	(* prop_formula list -> prop_formula *)

    	fun exists xs = Library.foldl SOr (False, xs);

    (* ------------------------------------------------------------------------- *)
    (* all: computes the conjunction over a list 'xs' of propositional formulas  *)
    (* ------------------------------------------------------------------------- *)

    	(* prop_formula list -> prop_formula *)

    	fun all xs = Library.foldl SAnd (True, xs);

    (* ------------------------------------------------------------------------- *)
    (* dot_product: ([x1,...,xn], [y1,...,yn]) -> x1*y1+...+xn*yn                *)
    (* ------------------------------------------------------------------------- *)

    	(* prop_formula list * prop_formula list -> prop_formula *)

    	fun dot_product (xs,ys) = exists (map SAnd (xs~~ys));

    (* ------------------------------------------------------------------------- *)
    (* nnf: computes the negation normal form of a formula 'fm' of propositional *)
    (*      logic (i.e. only variables may be negated, but not subformulas).     *)
    (*      Simplification (c.f. 'simplify') is performed as well.               *)
    (* ------------------------------------------------------------------------- *)

    	(* prop_formula -> prop_formula *)

    	fun
    	(* constants *)
    	    nnf True                   = True
    	  | nnf False                  = False
    	(* variables *)
    	  | nnf (BoolVar i)            = (BoolVar i)
    	(* 'or' and 'and' as outermost connectives are left untouched *)
    	  | nnf (Or  (fm1, fm2))       = SOr  (nnf fm1, nnf fm2)
    	  | nnf (And (fm1, fm2))       = SAnd (nnf fm1, nnf fm2)
    	(* 'not' + constant *)
    	  | nnf (Not True)             = False
    	  | nnf (Not False)            = True
    	(* 'not' + variable *)
    	  | nnf (Not (BoolVar i))      = Not (BoolVar i)
    	(* pushing 'not' inside of 'or'/'and' using de Morgan's laws *)
    	  | nnf (Not (Or  (fm1, fm2))) = SAnd (nnf (SNot fm1), nnf (SNot fm2))
    	  | nnf (Not (And (fm1, fm2))) = SOr  (nnf (SNot fm1), nnf (SNot fm2))
    	(* double-negation elimination *)
    	  | nnf (Not (Not fm))         = nnf fm;

    (* ------------------------------------------------------------------------- *)
    (* cnf: computes the conjunctive normal form (i.e. a conjunction of          *)
    (*      disjunctions) of a formula 'fm' of propositional logic.  The result  *)
    (*      formula may be exponentially longer than 'fm'.                       *)
    (* ------------------------------------------------------------------------- *)

    	(* prop_formula -> prop_formula *)

    	fun cnf fm =
    	let
    		fun
    		(* constants *)
    		    cnf_from_nnf True             = True
    		  | cnf_from_nnf False            = False
    		(* literals *)
    		  | cnf_from_nnf (BoolVar i)      = BoolVar i
    		  | cnf_from_nnf (Not fm1)        = Not fm1  (* 'fm1' must be a variable since the formula is in NNF *)
    		(* pushing 'or' inside of 'and' using distributive laws *)
    		  | cnf_from_nnf (Or (fm1, fm2))  =
    			let
    				fun cnf_or (And (fm11, fm12), fm2) =
    					And (cnf_or (fm11, fm2), cnf_or (fm12, fm2))
    				  | cnf_or (fm1, And (fm21, fm22)) =
    					And (cnf_or (fm1, fm21), cnf_or (fm1, fm22))
    				(* neither subformula contains 'and' *)
    				  | cnf_or (fm1, fm2) =
    					Or (fm1, fm2)
    			in
    				cnf_or (cnf_from_nnf fm1, cnf_from_nnf fm2)
    			end
    		(* 'and' as outermost connective is left untouched *)
    		  | cnf_from_nnf (And (fm1, fm2)) = And (cnf_from_nnf fm1, cnf_from_nnf fm2)
    	in
    		(cnf_from_nnf o nnf) fm
    	end;

    (* ------------------------------------------------------------------------- *)
    (* auxcnf: computes the definitional conjunctive normal form of a formula    *)
    (*      'fm' of propositional logic, introducing auxiliary variables if      *)
    (*      necessary to avoid an exponential blowup of the formula.  The result *)
    (*      formula is satisfiable if and only if 'fm' is satisfiable.           *)
    (*      Auxiliary variables are introduced as switches for OR-nodes, based   *)
    (*      on the observation that e.g. "fm1 OR (fm21 AND fm22)" is             *)
    (*      equisatisfiable with "(fm1 OR ~aux) AND (fm21 OR aux) AND (fm22 OR   *)
    (*      aux)".                                                               *)
    (* ------------------------------------------------------------------------- *)

    (* ------------------------------------------------------------------------- *)
    (* Note: 'auxcnf' tends to use fewer variables and fewer clauses than        *)
    (*      'defcnf' below, but sometimes generates much larger SAT problems     *)
    (*      overall (hence it must sometimes generate longer clauses than        *)
    (*      'defcnf' does).  It is currently not quite clear to me if one of the *)
    (*      algorithms is clearly superior to the other, but I suggest using     *)
    (*      'defcnf' instead.                                                    *)
    (* ------------------------------------------------------------------------- *)

    	(* prop_formula -> prop_formula *)

    	fun auxcnf fm =
    	let
    		(* convert formula to NNF first *)
    		val fm' = nnf fm
    		(* 'new' specifies the next index that is available to introduce an auxiliary variable *)
    		(* int ref *)
    		val new = ref (maxidx fm' + 1)
    		(* unit -> int *)
    		fun new_idx () = let val idx = !new in new := idx+1; idx end
    		(* prop_formula -> prop_formula *)
    		fun
    		(* constants *)
    		    auxcnf_from_nnf True  = True
    		  | auxcnf_from_nnf False = False
    		(* literals *)
    		  | auxcnf_from_nnf (BoolVar i) = BoolVar i
    		  | auxcnf_from_nnf (Not fm1)   = Not fm1  (* 'fm1' must be a variable since the formula is in NNF *)
    		(* pushing 'or' inside of 'and' using auxiliary variables *)
    		  | auxcnf_from_nnf (Or (fm1, fm2)) =
    			let
    				val fm1' = auxcnf_from_nnf fm1
    				val fm2' = auxcnf_from_nnf fm2
    				(* prop_formula * prop_formula -> prop_formula *)
    				fun auxcnf_or (And (fm11, fm12), fm2) =
    					(case fm2 of
    					(* do not introduce an auxiliary variable for literals *)
    					  BoolVar _ =>
    							And (auxcnf_or (fm11, fm2), auxcnf_or (fm12, fm2))
    					| Not _ =>
    							And (auxcnf_or (fm11, fm2), auxcnf_or (fm12, fm2))
    					| _ =>
    						let
    							val aux = BoolVar (new_idx ())
    						in
    							And (And (auxcnf_or (fm11, aux), auxcnf_or (fm12, aux)), auxcnf_or (fm2, Not aux))
    						end)
    				  | auxcnf_or (fm1, And (fm21, fm22)) =
    					(case fm1 of
    					(* do not introduce an auxiliary variable for literals *)
    					  BoolVar _ =>
    							And (auxcnf_or (fm1, fm21), auxcnf_or (fm1, fm22))
    					| Not _ =>
    							And (auxcnf_or (fm1, fm21), auxcnf_or (fm1, fm22))
    					| _ =>
    						let
    							val aux = BoolVar (new_idx ())
    						in
    							And (auxcnf_or (fm1, Not aux), And (auxcnf_or (fm21, aux), auxcnf_or (fm22, aux)))
    						end)
    				(* neither subformula contains 'and' *)
    				  | auxcnf_or (fm1, fm2) =
    					Or (fm1, fm2)
    			in
    				auxcnf_or (fm1', fm2')
    			end
    		(* 'and' as outermost connective is left untouched *)
    		  | auxcnf_from_nnf (And (fm1, fm2)) =
    				And (auxcnf_from_nnf fm1, auxcnf_from_nnf fm2)
    	in
    		auxcnf_from_nnf fm'
    	end;

    (* ------------------------------------------------------------------------- *)
    (* defcnf: computes the definitional conjunctive normal form of a formula    *)
    (*      'fm' of propositional logic, introducing auxiliary variables to      *)
    (*      avoid an exponential blowup of the formula.  The result formula is   *)
    (*      satisfiable if and only if 'fm' is satisfiable.  Auxiliary variables *)
    (*      are introduced as abbreviations for AND-, OR-, and NOT-nodes, based  *)
    (*      on the following equisatisfiabilities (+/- indicates polarity):      *)
    (*      LITERAL+       == LITERAL                                            *)
    (*      LITERAL-       == NOT LITERAL                                        *)
    (*      (NOT fm1)+     == aux AND (NOT aux OR fm1-)                          *)
    (*      (fm1 OR fm2)+  == aux AND (NOT aux OR fm1+ OR fm2+)                  *)
    (*      (fm1 AND fm2)+ == aux AND (NOT aux OR fm1+) AND (NOT aux OR fm2+)    *)
    (*      (NOT fm1)-     == aux AND (NOT aux OR fm1+)                          *)
    (*      (fm1 OR fm2)-  == aux AND (NOT aux OR fm1-) AND (NOT aux OR fm2-)    *)
    (*      (fm1 AND fm2)- == aux AND (NOT aux OR fm1- OR fm2-)                  *)
    (*      Example:                                                             *)
    (*      NOT (a AND b) == aux1 AND (NOT aux1 OR aux2)                         *)
    (*                            AND (NOT aux2 OR NOT a OR NOT b)               *)
    (* ------------------------------------------------------------------------- *)

    	(* prop_formula -> prop_formula *)

    	fun defcnf fm =
    	let
    		(* simplify formula first *)
    		val fm' = simplify fm
    		(* 'new' specifies the next index that is available to introduce an auxiliary variable *)
    		(* int ref *)
    		val new = ref (maxidx fm' + 1)
    		(* unit -> int *)
    		fun new_idx () = let val idx = !new in new := idx+1; idx end
    		(* optimization for n-ary disjunction/conjunction *)
    		(* prop_formula -> prop_formula list *)
    		fun disjuncts (Or (fm1, fm2)) = (disjuncts fm1) @ (disjuncts fm2)
    		  | disjuncts fm1             = [fm1]
    		(* prop_formula -> prop_formula list *)
    		fun conjuncts (And (fm1, fm2)) = (conjuncts fm1) @ (conjuncts fm2)
    		  | conjuncts fm1              = [fm1]
    		(* polarity -> formula -> (defining clauses, literal) *)
    		(* bool -> prop_formula -> prop_formula * prop_formula *)
    		fun
    		(* constants *)
    		    defcnf' true  True  = (True, True)
    		  | defcnf' false True  = (*(True, False)*) error "formula is not simplified, True occurs with negative polarity"
    		  | defcnf' true  False = (True, False)
    		  | defcnf' false False = (*(True, True)*) error "formula is not simplified, False occurs with negative polarity"
    		(* literals *)
    		  | defcnf' true  (BoolVar i)       = (True, BoolVar i)
    		  | defcnf' false (BoolVar i)       = (True, Not (BoolVar i))
    		  | defcnf' true  (Not (BoolVar i)) = (True, Not (BoolVar i))
    		  | defcnf' false (Not (BoolVar i)) = (True, BoolVar i)
    		(* 'not' *)
    		  | defcnf' polarity (Not fm1) =
    			let
    				val (def1, aux1) = defcnf' (not polarity) fm1
    				val aux          = BoolVar (new_idx ())
    				val def          = Or (Not aux, aux1)
    			in
    				(SAnd (def1, def), aux)
    			end
    		(* 'or' *)
    		  | defcnf' polarity (Or (fm1, fm2)) =
    			let
    				val fms          = disjuncts (Or (fm1, fm2))
    				val (defs, auxs) = split_list (map (defcnf' polarity) fms)
    				val aux          = BoolVar (new_idx ())
    				val def          = if polarity then Or (Not aux, exists auxs) else all (map (fn a => Or (Not aux, a)) auxs)
    			in
    				(SAnd (all defs, def), aux)
    			end
    		(* 'and' *)
    		  | defcnf' polarity (And (fm1, fm2)) =
    			let
    				val fms          = conjuncts (And (fm1, fm2))
    				val (defs, auxs) = split_list (map (defcnf' polarity) fms)
    				val aux          = BoolVar (new_idx ())
    				val def          = if not polarity then Or (Not aux, exists auxs) else all (map (fn a => Or (Not aux, a)) auxs)
    			in
    				(SAnd (all defs, def), aux)
    			end
    		(* optimization: do not introduce auxiliary variables for parts of the formula that are in CNF already *)
    		(* prop_formula -> prop_formula * prop_formula *)
    		fun defcnf_or (Or (fm1, fm2)) =
    			let
    				val (def1, aux1) = defcnf_or fm1
    				val (def2, aux2) = defcnf_or fm2
    			in
    				(SAnd (def1, def2), Or (aux1, aux2))
    			end
    		  | defcnf_or fm =
    			defcnf' true fm
    		(* prop_formula -> prop_formula * prop_formula *)
    		fun defcnf_and (And (fm1, fm2)) =
    			let
    				val (def1, aux1) = defcnf_and fm1
    				val (def2, aux2) = defcnf_and fm2
    			in
    				(SAnd (def1, def2), And (aux1, aux2))
    			end
    		  | defcnf_and (Or (fm1, fm2)) =
    			let
    				val (def1, aux1) = defcnf_or fm1
    				val (def2, aux2) = defcnf_or fm2
    			in
    				(SAnd (def1, def2), Or (aux1, aux2))
    			end
    		  | defcnf_and fm =
    			defcnf' true fm
    	in
    		SAnd (defcnf_and fm')
    	end;

    (* ------------------------------------------------------------------------- *)
    (* eval: given an assignment 'a' of Boolean values to variable indices, the  *)
    (*      truth value of a propositional formula 'fm' is computed              *)
    (* ------------------------------------------------------------------------- *)

    	(* (int -> bool) -> prop_formula -> bool *)

    	fun eval a True            = true
    	  | eval a False           = false
    	  | eval a (BoolVar i)     = (a i)
    	  | eval a (Not fm)        = not (eval a fm)
    	  | eval a (Or (fm1,fm2))  = (eval a fm1) orelse (eval a fm2)
    	  | eval a (And (fm1,fm2)) = (eval a fm1) andalso (eval a fm2);

    end;