1 (* ========================================================================= *) |
1 (* ========================================================================= *) |
2 (* NORMALIZING FORMULAS *) |
2 (* NORMALIZING FORMULAS *) |
3 (* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) |
3 (* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) |
4 (* ========================================================================= *) |
4 (* ========================================================================= *) |
5 |
5 |
6 structure Normalize :> Normalize = |
6 structure Normalize :> Normalize = |
7 struct |
7 struct |
8 |
8 |
646 True => Formula.True |
646 True => Formula.True |
647 | False => Formula.False |
647 | False => Formula.False |
648 | Literal (_,lit) => Literal.toFormula lit |
648 | Literal (_,lit) => Literal.toFormula lit |
649 | And (_,_,s) => Formula.listMkConj (Set.transform form s) |
649 | And (_,_,s) => Formula.listMkConj (Set.transform form s) |
650 | Or (_,_,s) => Formula.listMkDisj (Set.transform form s) |
650 | Or (_,_,s) => Formula.listMkDisj (Set.transform form s) |
651 | Xor (_,_,p,s) => |
651 | Xor (_,_,p,s) => xorForm p s |
652 let |
|
653 val s = if p then negateLastElt s else s |
|
654 in |
|
655 Formula.listMkEquiv (Set.transform form s) |
|
656 end |
|
657 | Exists (_,_,n,f) => Formula.listMkExists (NameSet.toList n, form f) |
652 | Exists (_,_,n,f) => Formula.listMkExists (NameSet.toList n, form f) |
658 | Forall (_,_,n,f) => Formula.listMkForall (NameSet.toList n, form f); |
653 | Forall (_,_,n,f) => Formula.listMkForall (NameSet.toList n, form f) |
|
654 |
|
655 (* To convert a Xor set to an Iff list we need to know *) |
|
656 (* whether the size of the set is even or odd: *) |
|
657 (* *) |
|
658 (* b XOR a = b <=> ~a *) |
|
659 (* c XOR b XOR a = c <=> b <=> a *) |
|
660 (* d XOR c XOR b XOR a = d <=> c <=> b <=> ~a *) |
|
661 (* e XOR d XOR c XOR b XOR a = e <=> d <=> c <=> b <=> a *) |
|
662 and xorForm p s = |
|
663 let |
|
664 val p = if Set.size s mod 2 = 0 then not p else p |
|
665 val s = if p then s else negateLastElt s |
|
666 in |
|
667 Formula.listMkEquiv (Set.transform form s) |
|
668 end; |
659 in |
669 in |
660 val toFormula = form; |
670 val toFormula = form; |
661 end; |
671 end; |
662 |
672 |
663 fun toLiteral (Literal (_,lit)) = lit |
673 fun toLiteral (Literal (_,lit)) = lit |