src/HOL/Tools/prop_logic.ML
author webertj
Tue Jul 26 14:14:13 2005 +0200 (2005-07-26)
changeset 16913 1d8a8d010e69
parent 16909 acbc7a9c3864
child 17809 195045659c06
permissions -rw-r--r--
comment modified
     1 (*  Title:      HOL/Tools/prop_logic.ML
     2     ID:         $Id$
     3     Author:     Tjark Weber
     4     Copyright   2004-2005
     5 
     6 Formulas of propositional logic.
     7 *)
     8 
     9 signature PROP_LOGIC =
    10 sig
    11 	datatype prop_formula =
    12 		  True
    13 		| False
    14 		| BoolVar of int  (* NOTE: only use indices >= 1 *)
    15 		| Not of prop_formula
    16 		| Or of prop_formula * prop_formula
    17 		| And of prop_formula * prop_formula
    18 
    19 	val SNot     : prop_formula -> prop_formula
    20 	val SOr      : prop_formula * prop_formula -> prop_formula
    21 	val SAnd     : prop_formula * prop_formula -> prop_formula
    22 	val simplify : prop_formula -> prop_formula  (* eliminates True/False and double-negation *)
    23 
    24 	val indices : prop_formula -> int list  (* set of all variable indices *)
    25 	val maxidx  : prop_formula -> int       (* maximal variable index *)
    26 
    27 	val exists      : prop_formula list -> prop_formula  (* finite disjunction *)
    28 	val all         : prop_formula list -> prop_formula  (* finite conjunction *)
    29 	val dot_product : prop_formula list * prop_formula list -> prop_formula
    30 
    31 	val nnf    : prop_formula -> prop_formula  (* negation normal form *)
    32 	val cnf    : prop_formula -> prop_formula  (* conjunctive normal form *)
    33 	val auxcnf : prop_formula -> prop_formula  (* cnf with auxiliary variables *)
    34 	val defcnf : prop_formula -> prop_formula  (* definitional cnf *)
    35 
    36 	val eval : (int -> bool) -> prop_formula -> bool  (* semantics *)
    37 end;
    38 
    39 structure PropLogic : PROP_LOGIC =
    40 struct
    41 
    42 (* ------------------------------------------------------------------------- *)
    43 (* prop_formula: formulas of propositional logic, built from Boolean         *)
    44 (*               variables (referred to by index) and True/False using       *)
    45 (*               not/or/and                                                  *)
    46 (* ------------------------------------------------------------------------- *)
    47 
    48 	datatype prop_formula =
    49 		  True
    50 		| False
    51 		| BoolVar of int  (* NOTE: only use indices >= 1 *)
    52 		| Not of prop_formula
    53 		| Or of prop_formula * prop_formula
    54 		| And of prop_formula * prop_formula;
    55 
    56 (* ------------------------------------------------------------------------- *)
    57 (* The following constructor functions make sure that True and False do not  *)
    58 (* occur within any of the other connectives (i.e. Not, Or, And), and        *)
    59 (* perform double-negation elimination.                                      *)
    60 (* ------------------------------------------------------------------------- *)
    61 
    62 	(* prop_formula -> prop_formula *)
    63 
    64 	fun SNot True     = False
    65 	  | SNot False    = True
    66 	  | SNot (Not fm) = fm
    67 	  | SNot fm       = Not fm;
    68 
    69 	(* prop_formula * prop_formula -> prop_formula *)
    70 
    71 	fun SOr (True, _)   = True
    72 	  | SOr (_, True)   = True
    73 	  | SOr (False, fm) = fm
    74 	  | SOr (fm, False) = fm
    75 	  | SOr (fm1, fm2)  = Or (fm1, fm2);
    76 
    77 	(* prop_formula * prop_formula -> prop_formula *)
    78 
    79 	fun SAnd (True, fm) = fm
    80 	  | SAnd (fm, True) = fm
    81 	  | SAnd (False, _) = False
    82 	  | SAnd (_, False) = False
    83 	  | SAnd (fm1, fm2) = And (fm1, fm2);
    84 
    85 (* ------------------------------------------------------------------------- *)
    86 (* simplify: eliminates True/False below other connectives, and double-      *)
    87 (*      negation                                                             *)
    88 (* ------------------------------------------------------------------------- *)
    89 
    90 	(* prop_formula -> prop_formula *)
    91 
    92 	fun simplify (Not fm)         = SNot (simplify fm)
    93 	  | simplify (Or (fm1, fm2))  = SOr (simplify fm1, simplify fm2)
    94 	  | simplify (And (fm1, fm2)) = SAnd (simplify fm1, simplify fm2)
    95 	  | simplify fm               = fm;
    96 
    97 (* ------------------------------------------------------------------------- *)
    98 (* indices: collects all indices of Boolean variables that occur in a        *)
    99 (*      propositional formula 'fm'; no duplicates                            *)
   100 (* ------------------------------------------------------------------------- *)
   101 
   102 	(* prop_formula -> int list *)
   103 
   104 	fun indices True             = []
   105 	  | indices False            = []
   106 	  | indices (BoolVar i)      = [i]
   107 	  | indices (Not fm)         = indices fm
   108 	  | indices (Or (fm1, fm2))  = (indices fm1) union_int (indices fm2)
   109 	  | indices (And (fm1, fm2)) = (indices fm1) union_int (indices fm2);
   110 
   111 (* ------------------------------------------------------------------------- *)
   112 (* maxidx: computes the maximal variable index occuring in a formula of      *)
   113 (*      propositional logic 'fm'; 0 if 'fm' contains no variable             *)
   114 (* ------------------------------------------------------------------------- *)
   115 
   116 	(* prop_formula -> int *)
   117 
   118 	fun maxidx True             = 0
   119 	  | maxidx False            = 0
   120 	  | maxidx (BoolVar i)      = i
   121 	  | maxidx (Not fm)         = maxidx fm
   122 	  | maxidx (Or (fm1, fm2))  = Int.max (maxidx fm1, maxidx fm2)
   123 	  | maxidx (And (fm1, fm2)) = Int.max (maxidx fm1, maxidx fm2);
   124 
   125 (* ------------------------------------------------------------------------- *)
   126 (* exists: computes the disjunction over a list 'xs' of propositional        *)
   127 (*      formulas                                                             *)
   128 (* ------------------------------------------------------------------------- *)
   129 
   130 	(* prop_formula list -> prop_formula *)
   131 
   132 	fun exists xs = Library.foldl SOr (False, xs);
   133 
   134 (* ------------------------------------------------------------------------- *)
   135 (* all: computes the conjunction over a list 'xs' of propositional formulas  *)
   136 (* ------------------------------------------------------------------------- *)
   137 
   138 	(* prop_formula list -> prop_formula *)
   139 
   140 	fun all xs = Library.foldl SAnd (True, xs);
   141 
   142 (* ------------------------------------------------------------------------- *)
   143 (* dot_product: ([x1,...,xn], [y1,...,yn]) -> x1*y1+...+xn*yn                *)
   144 (* ------------------------------------------------------------------------- *)
   145 
   146 	(* prop_formula list * prop_formula list -> prop_formula *)
   147 
   148 	fun dot_product (xs,ys) = exists (map SAnd (xs~~ys));
   149 
   150 (* ------------------------------------------------------------------------- *)
   151 (* nnf: computes the negation normal form of a formula 'fm' of propositional *)
   152 (*      logic (i.e. only variables may be negated, but not subformulas).     *)
   153 (*      Simplification (c.f. 'simplify') is performed as well.               *)
   154 (* ------------------------------------------------------------------------- *)
   155 
   156 	(* prop_formula -> prop_formula *)
   157 
   158 	fun
   159 	(* constants *)
   160 	    nnf True                   = True
   161 	  | nnf False                  = False
   162 	(* variables *)
   163 	  | nnf (BoolVar i)            = (BoolVar i)
   164 	(* 'or' and 'and' as outermost connectives are left untouched *)
   165 	  | nnf (Or  (fm1, fm2))       = SOr  (nnf fm1, nnf fm2)
   166 	  | nnf (And (fm1, fm2))       = SAnd (nnf fm1, nnf fm2)
   167 	(* 'not' + constant *)
   168 	  | nnf (Not True)             = False
   169 	  | nnf (Not False)            = True
   170 	(* 'not' + variable *)
   171 	  | nnf (Not (BoolVar i))      = Not (BoolVar i)
   172 	(* pushing 'not' inside of 'or'/'and' using de Morgan's laws *)
   173 	  | nnf (Not (Or  (fm1, fm2))) = SAnd (nnf (SNot fm1), nnf (SNot fm2))
   174 	  | nnf (Not (And (fm1, fm2))) = SOr  (nnf (SNot fm1), nnf (SNot fm2))
   175 	(* double-negation elimination *)
   176 	  | nnf (Not (Not fm))         = nnf fm;
   177 
   178 (* ------------------------------------------------------------------------- *)
   179 (* cnf: computes the conjunctive normal form (i.e. a conjunction of          *)
   180 (*      disjunctions) of a formula 'fm' of propositional logic.  The result  *)
   181 (*      formula may be exponentially longer than 'fm'.                       *)
   182 (* ------------------------------------------------------------------------- *)
   183 
   184 	(* prop_formula -> prop_formula *)
   185 
   186 	fun cnf fm =
   187 	let
   188 		fun
   189 		(* constants *)
   190 		    cnf_from_nnf True             = True
   191 		  | cnf_from_nnf False            = False
   192 		(* literals *)
   193 		  | cnf_from_nnf (BoolVar i)      = BoolVar i
   194 		  | cnf_from_nnf (Not fm1)        = Not fm1  (* 'fm1' must be a variable since the formula is in NNF *)
   195 		(* pushing 'or' inside of 'and' using distributive laws *)
   196 		  | cnf_from_nnf (Or (fm1, fm2))  =
   197 			let
   198 				fun cnf_or (And (fm11, fm12), fm2) =
   199 					And (cnf_or (fm11, fm2), cnf_or (fm12, fm2))
   200 				  | cnf_or (fm1, And (fm21, fm22)) =
   201 					And (cnf_or (fm1, fm21), cnf_or (fm1, fm22))
   202 				(* neither subformula contains 'and' *)
   203 				  | cnf_or (fm1, fm2) =
   204 					Or (fm1, fm2)
   205 			in
   206 				cnf_or (cnf_from_nnf fm1, cnf_from_nnf fm2)
   207 			end
   208 		(* 'and' as outermost connective is left untouched *)
   209 		  | cnf_from_nnf (And (fm1, fm2)) = And (cnf_from_nnf fm1, cnf_from_nnf fm2)
   210 	in
   211 		(cnf_from_nnf o nnf) fm
   212 	end;
   213 
   214 (* ------------------------------------------------------------------------- *)
   215 (* auxcnf: computes the definitional conjunctive normal form of a formula    *)
   216 (*      'fm' of propositional logic, introducing auxiliary variables if      *)
   217 (*      necessary to avoid an exponential blowup of the formula.  The result *)
   218 (*      formula is satisfiable if and only if 'fm' is satisfiable.           *)
   219 (*      Auxiliary variables are introduced as switches for OR-nodes, based   *)
   220 (*      on the observation that e.g. "fm1 OR (fm21 AND fm22)" is             *)
   221 (*      equisatisfiable with "(fm1 OR ~aux) AND (fm21 OR aux) AND (fm22 OR   *)
   222 (*      aux)".                                                               *)
   223 (* ------------------------------------------------------------------------- *)
   224 
   225 (* ------------------------------------------------------------------------- *)
   226 (* Note: 'auxcnf' tends to use fewer variables and fewer clauses than        *)
   227 (*      'defcnf' below, but sometimes generates much larger SAT problems     *)
   228 (*      overall (hence it must sometimes generate longer clauses than        *)
   229 (*      'defcnf' does).  It is currently not quite clear to me if one of the *)
   230 (*      algorithms is clearly superior to the other, but I suggest using     *)
   231 (*      'defcnf' instead.                                                    *)
   232 (* ------------------------------------------------------------------------- *)
   233 
   234 	(* prop_formula -> prop_formula *)
   235 
   236 	fun auxcnf fm =
   237 	let
   238 		(* convert formula to NNF first *)
   239 		val fm' = nnf fm
   240 		(* 'new' specifies the next index that is available to introduce an auxiliary variable *)
   241 		(* int ref *)
   242 		val new = ref (maxidx fm' + 1)
   243 		(* unit -> int *)
   244 		fun new_idx () = let val idx = !new in new := idx+1; idx end
   245 		(* prop_formula -> prop_formula *)
   246 		fun
   247 		(* constants *)
   248 		    auxcnf_from_nnf True  = True
   249 		  | auxcnf_from_nnf False = False
   250 		(* literals *)
   251 		  | auxcnf_from_nnf (BoolVar i) = BoolVar i
   252 		  | auxcnf_from_nnf (Not fm1)   = Not fm1  (* 'fm1' must be a variable since the formula is in NNF *)
   253 		(* pushing 'or' inside of 'and' using auxiliary variables *)
   254 		  | auxcnf_from_nnf (Or (fm1, fm2)) =
   255 			let
   256 				val fm1' = auxcnf_from_nnf fm1
   257 				val fm2' = auxcnf_from_nnf fm2
   258 				(* prop_formula * prop_formula -> prop_formula *)
   259 				fun auxcnf_or (And (fm11, fm12), fm2) =
   260 					(case fm2 of
   261 					(* do not introduce an auxiliary variable for literals *)
   262 					  BoolVar _ =>
   263 							And (auxcnf_or (fm11, fm2), auxcnf_or (fm12, fm2))
   264 					| Not _ =>
   265 							And (auxcnf_or (fm11, fm2), auxcnf_or (fm12, fm2))
   266 					| _ =>
   267 						let
   268 							val aux = BoolVar (new_idx ())
   269 						in
   270 							And (And (auxcnf_or (fm11, aux), auxcnf_or (fm12, aux)), auxcnf_or (fm2, Not aux))
   271 						end)
   272 				  | auxcnf_or (fm1, And (fm21, fm22)) =
   273 					(case fm1 of
   274 					(* do not introduce an auxiliary variable for literals *)
   275 					  BoolVar _ =>
   276 							And (auxcnf_or (fm1, fm21), auxcnf_or (fm1, fm22))
   277 					| Not _ =>
   278 							And (auxcnf_or (fm1, fm21), auxcnf_or (fm1, fm22))
   279 					| _ =>
   280 						let
   281 							val aux = BoolVar (new_idx ())
   282 						in
   283 							And (auxcnf_or (fm1, Not aux), And (auxcnf_or (fm21, aux), auxcnf_or (fm22, aux)))
   284 						end)
   285 				(* neither subformula contains 'and' *)
   286 				  | auxcnf_or (fm1, fm2) =
   287 					Or (fm1, fm2)
   288 			in
   289 				auxcnf_or (fm1', fm2')
   290 			end
   291 		(* 'and' as outermost connective is left untouched *)
   292 		  | auxcnf_from_nnf (And (fm1, fm2)) =
   293 				And (auxcnf_from_nnf fm1, auxcnf_from_nnf fm2)
   294 	in
   295 		auxcnf_from_nnf fm'
   296 	end;
   297 
   298 (* ------------------------------------------------------------------------- *)
   299 (* defcnf: computes the definitional conjunctive normal form of a formula    *)
   300 (*      'fm' of propositional logic, introducing auxiliary variables to      *)
   301 (*      avoid an exponential blowup of the formula.  The result formula is   *)
   302 (*      satisfiable if and only if 'fm' is satisfiable.  Auxiliary variables *)
   303 (*      are introduced as abbreviations for AND-, OR-, and NOT-nodes, based  *)
   304 (*      on the following equisatisfiabilities (+/- indicates polarity):      *)
   305 (*      LITERAL+       == LITERAL                                            *)
   306 (*      LITERAL-       == NOT LITERAL                                        *)
   307 (*      (NOT fm1)+     == aux AND (NOT aux OR fm1-)                          *)
   308 (*      (fm1 OR fm2)+  == aux AND (NOT aux OR fm1+ OR fm2+)                  *)
   309 (*      (fm1 AND fm2)+ == aux AND (NOT aux OR fm1+) AND (NOT aux OR fm2+)    *)
   310 (*      (NOT fm1)-     == aux AND (NOT aux OR fm1+)                          *)
   311 (*      (fm1 OR fm2)-  == aux AND (NOT aux OR fm1-) AND (NOT aux OR fm2-)    *)
   312 (*      (fm1 AND fm2)- == aux AND (NOT aux OR fm1- OR fm2-)                  *)
   313 (*      Example:                                                             *)
   314 (*      NOT (a AND b) == aux1 AND (NOT aux1 OR aux2)                         *)
   315 (*                            AND (NOT aux2 OR NOT a OR NOT b)               *)
   316 (* ------------------------------------------------------------------------- *)
   317 
   318 	(* prop_formula -> prop_formula *)
   319 
   320 	fun defcnf fm =
   321 	let
   322 		(* simplify formula first *)
   323 		val fm' = simplify fm
   324 		(* 'new' specifies the next index that is available to introduce an auxiliary variable *)
   325 		(* int ref *)
   326 		val new = ref (maxidx fm' + 1)
   327 		(* unit -> int *)
   328 		fun new_idx () = let val idx = !new in new := idx+1; idx end
   329 		(* optimization for n-ary disjunction/conjunction *)
   330 		(* prop_formula -> prop_formula list *)
   331 		fun disjuncts (Or (fm1, fm2)) = (disjuncts fm1) @ (disjuncts fm2)
   332 		  | disjuncts fm1             = [fm1]
   333 		(* prop_formula -> prop_formula list *)
   334 		fun conjuncts (And (fm1, fm2)) = (conjuncts fm1) @ (conjuncts fm2)
   335 		  | conjuncts fm1              = [fm1]
   336 		(* polarity -> formula -> (defining clauses, literal) *)
   337 		(* bool -> prop_formula -> prop_formula * prop_formula *)
   338 		fun
   339 		(* constants *)
   340 		    defcnf' true  True  = (True, True)
   341 		  | defcnf' false True  = (*(True, False)*) error "formula is not simplified, True occurs with negative polarity"
   342 		  | defcnf' true  False = (True, False)
   343 		  | defcnf' false False = (*(True, True)*) error "formula is not simplified, False occurs with negative polarity"
   344 		(* literals *)
   345 		  | defcnf' true  (BoolVar i)       = (True, BoolVar i)
   346 		  | defcnf' false (BoolVar i)       = (True, Not (BoolVar i))
   347 		  | defcnf' true  (Not (BoolVar i)) = (True, Not (BoolVar i))
   348 		  | defcnf' false (Not (BoolVar i)) = (True, BoolVar i)
   349 		(* 'not' *)
   350 		  | defcnf' polarity (Not fm1) =
   351 			let
   352 				val (def1, aux1) = defcnf' (not polarity) fm1
   353 				val aux          = BoolVar (new_idx ())
   354 				val def          = Or (Not aux, aux1)
   355 			in
   356 				(SAnd (def1, def), aux)
   357 			end
   358 		(* 'or' *)
   359 		  | defcnf' polarity (Or (fm1, fm2)) =
   360 			let
   361 				val fms          = disjuncts (Or (fm1, fm2))
   362 				val (defs, auxs) = split_list (map (defcnf' polarity) fms)
   363 				val aux          = BoolVar (new_idx ())
   364 				val def          = if polarity then Or (Not aux, exists auxs) else all (map (fn a => Or (Not aux, a)) auxs)
   365 			in
   366 				(SAnd (all defs, def), aux)
   367 			end
   368 		(* 'and' *)
   369 		  | defcnf' polarity (And (fm1, fm2)) =
   370 			let
   371 				val fms          = conjuncts (And (fm1, fm2))
   372 				val (defs, auxs) = split_list (map (defcnf' polarity) fms)
   373 				val aux          = BoolVar (new_idx ())
   374 				val def          = if not polarity then Or (Not aux, exists auxs) else all (map (fn a => Or (Not aux, a)) auxs)
   375 			in
   376 				(SAnd (all defs, def), aux)
   377 			end
   378 		(* optimization: do not introduce auxiliary variables for parts of the formula that are in CNF already *)
   379 		(* prop_formula -> prop_formula * prop_formula *)
   380 		fun defcnf_or (Or (fm1, fm2)) =
   381 			let
   382 				val (def1, aux1) = defcnf_or fm1
   383 				val (def2, aux2) = defcnf_or fm2
   384 			in
   385 				(SAnd (def1, def2), Or (aux1, aux2))
   386 			end
   387 		  | defcnf_or fm =
   388 			defcnf' true fm
   389 		(* prop_formula -> prop_formula * prop_formula *)
   390 		fun defcnf_and (And (fm1, fm2)) =
   391 			let
   392 				val (def1, aux1) = defcnf_and fm1
   393 				val (def2, aux2) = defcnf_and fm2
   394 			in
   395 				(SAnd (def1, def2), And (aux1, aux2))
   396 			end
   397 		  | defcnf_and (Or (fm1, fm2)) =
   398 			let
   399 				val (def1, aux1) = defcnf_or fm1
   400 				val (def2, aux2) = defcnf_or fm2
   401 			in
   402 				(SAnd (def1, def2), Or (aux1, aux2))
   403 			end
   404 		  | defcnf_and fm =
   405 			defcnf' true fm
   406 	in
   407 		SAnd (defcnf_and fm')
   408 	end;
   409 
   410 (* ------------------------------------------------------------------------- *)
   411 (* eval: given an assignment 'a' of Boolean values to variable indices, the  *)
   412 (*      truth value of a propositional formula 'fm' is computed              *)
   413 (* ------------------------------------------------------------------------- *)
   414 
   415 	(* (int -> bool) -> prop_formula -> bool *)
   416 
   417 	fun eval a True            = true
   418 	  | eval a False           = false
   419 	  | eval a (BoolVar i)     = (a i)
   420 	  | eval a (Not fm)        = not (eval a fm)
   421 	  | eval a (Or (fm1,fm2))  = (eval a fm1) orelse (eval a fm2)
   422 	  | eval a (And (fm1,fm2)) = (eval a fm1) andalso (eval a fm2);
   423 
   424 end;