# HG changeset patch # User webertj # Date 1087142255 -7200 # Node ID 29fe4a9a7cb5c0d6e1eee0f278a3517846020bf2 # Parent 393b75c92c071c482ddbc3511c4e5c59bc50dfc8 faster defcnf conversion diff -r 393b75c92c07 -r 29fe4a9a7cb5 src/HOL/Tools/prop_logic.ML --- a/src/HOL/Tools/prop_logic.ML Sun Jun 13 15:43:55 2004 +0200 +++ b/src/HOL/Tools/prop_logic.ML Sun Jun 13 17:57:35 2004 +0200 @@ -109,6 +109,14 @@ | maxidx (And (fm1,fm2)) = Int.max (maxidx fm1, maxidx fm2); (* ------------------------------------------------------------------------- *) +(* exception SAME: raised to indicate that the return value of a function is *) +(* identical to its argument (optimization to allow sharing, *) +(* rather than copying) *) +(* ------------------------------------------------------------------------- *) + + exception SAME; + +(* ------------------------------------------------------------------------- *) (* nnf: computes the negation normal form of a formula 'fm' of propositional *) (* logic (i.e. only variables may be negated, but not subformulas) *) (* ------------------------------------------------------------------------- *) @@ -120,7 +128,7 @@ nnf True = True | nnf False = False (* variables *) - | nnf (BoolVar i) = BoolVar i + | 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) @@ -147,29 +155,26 @@ let fun (* constants *) - cnf_from_nnf True = True - | cnf_from_nnf False = False + cnf_from_nnf True = True + | cnf_from_nnf False = False (* literals *) - | cnf_from_nnf (BoolVar i) = BoolVar i - | cnf_from_nnf (Not (BoolVar i)) = Not (BoolVar i) + | 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)) = + | cnf_from_nnf (Or (fm1, fm2)) = let - val fm1' = cnf_from_nnf fm1 - val fm2' = cnf_from_nnf fm2 + 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 - case fm1' of - And (fm11,fm12) => cnf_from_nnf (SAnd (SOr(fm11,fm2'),SOr(fm12,fm2'))) - | _ => - (case fm2' of - And (fm21,fm22) => cnf_from_nnf (SAnd (SOr(fm1',fm21),SOr(fm1',fm22))) - (* neither subformula contains 'and' *) - | _ => Or (fm1,fm2)) + cnf_or (cnf_from_nnf fm1, cnf_from_nnf fm2) end (* 'and' as outermost connective is left untouched *) - | cnf_from_nnf (And (fm1,fm2)) = SAnd (cnf_from_nnf fm1, cnf_from_nnf fm2) - (* 'not' + something other than a variable: formula is not in negation normal form *) - | cnf_from_nnf _ = raise ERROR + | cnf_from_nnf (And (fm1, fm2)) = And (cnf_from_nnf fm1, cnf_from_nnf fm2) in (cnf_from_nnf o nnf) fm end; @@ -189,49 +194,52 @@ (* 'new' specifies the next index that is available to introduce an auxiliary variable *) fun (* constants *) - defcnf_from_nnf (True,new) = (True, new) - | defcnf_from_nnf (False,new) = (False, new) + defcnf_from_nnf (True, new) = (True, new) + | defcnf_from_nnf (False, new) = (False, new) (* literals *) - | defcnf_from_nnf (BoolVar i,new) = (BoolVar i, new) - | defcnf_from_nnf (Not (BoolVar i),new) = (Not (BoolVar i), new) - (* pushing 'or' inside of 'and' using distributive laws *) - | defcnf_from_nnf (Or (fm1,fm2),new) = + | defcnf_from_nnf (BoolVar i, new) = (BoolVar i, new) + | defcnf_from_nnf (Not fm1, new) = (Not fm1, new) (* 'fm1' must be a variable since the formula is in NNF *) + (* pushing 'or' inside of 'and' using auxiliary variables *) + | defcnf_from_nnf (Or (fm1, fm2), new) = let - val (fm1',new') = defcnf_from_nnf (fm1, new) - val (fm2',new'') = defcnf_from_nnf (fm2, new') - in - case fm1' of - And (fm11,fm12) => + val (fm1', new') = defcnf_from_nnf (fm1, new) + val (fm2', new'') = defcnf_from_nnf (fm2, new') + (* prop_formula * prop_formula -> int -> prop_formula * int *) + fun defcnf_or (And (fm11, fm12), fm2) new = let - val aux = BoolVar new'' + val aux = BoolVar new + val (fm_a, new') = defcnf_or (fm11, aux) (new+1) + val (fm_b, new'') = defcnf_or (fm12, aux) new' + val (fm_c, new''') = defcnf_or (fm2, Not aux) new'' in - (* '(fm11 AND fm12) OR fm2' is SAT-equivalent to '(fm11 OR aux) AND (fm12 OR aux) AND (fm2 OR NOT aux)' *) - defcnf_from_nnf (SAnd (SAnd (SOr (fm11,aux), SOr (fm12,aux)), SOr(fm2', Not aux)), new''+1) + (And (And (fm_a, fm_b), fm_c), new''') end - | _ => - (case fm2' of - And (fm21,fm22) => - let - val aux = BoolVar new'' - in - (* 'fm1 OR (fm21 AND fm22)' is SAT-equivalent to '(fm1 OR NOT aux) AND (fm21 OR aux) AND (fm22 OR NOT aux)' *) - defcnf_from_nnf (SAnd (SOr (fm1', Not aux), SAnd (SOr (fm21,aux), SOr (fm22,aux))), new''+1) - end - (* neither subformula contains 'and' *) - | _ => (Or (fm1,fm2),new)) + | defcnf_or (fm1, And (fm21, fm22)) new = + let + val aux = BoolVar new + val (fm_a, new') = defcnf_or (fm1, Not aux) (new+1) + val (fm_b, new'') = defcnf_or (fm21, aux) new' + val (fm_c, new''') = defcnf_or (fm22, aux) new'' + in + (And (fm_a, And (fm_b, fm_c)), new''') + end + (* neither subformula contains 'and' *) + | defcnf_or (fm1, fm2) new = + (Or (fm1, fm2), new) + in + defcnf_or (fm1', fm2') new'' end (* 'and' as outermost connective is left untouched *) - | defcnf_from_nnf (And (fm1,fm2),new) = + | defcnf_from_nnf (And (fm1, fm2), new) = let - val (fm1',new') = defcnf_from_nnf (fm1, new) - val (fm2',new'') = defcnf_from_nnf (fm2, new') + val (fm1', new') = defcnf_from_nnf (fm1, new) + val (fm2', new'') = defcnf_from_nnf (fm2, new') in - (SAnd (fm1', fm2'), new'') + (And (fm1', fm2'), new'') end - (* 'not' + something other than a variable: formula is not in negation normal form *) - | defcnf_from_nnf (_,_) = raise ERROR + val fm' = nnf fm in - (fst o defcnf_from_nnf) (nnf fm, (maxidx fm)+1) + (fst o defcnf_from_nnf) (fm', (maxidx fm')+1) end; (* ------------------------------------------------------------------------- *)