Provide explanations for complex transformations.
Unified · Split
| @@ -442,6 +442,7 @@ static struct expr *expr_join_or(struct expr *e1, struct expr *e2) · 441 unmodified lines | ||
| 442 | 442 | } |
| 443 | 443 | } |
| 444 | 444 | if (sym1->type == S_BOOLEAN) { |
| 445 | + // a || !a -> y | |
| 445 | 446 | if ((e1->type == E_NOT && e1->left.expr->type == E_SYMBOL && e2->type == E_SYMBOL) || |
| 446 | 447 | (e2->type == E_NOT && e2->left.expr->type == E_SYMBOL && e1->type == E_SYMBOL)) |
| 447 | 448 | return expr_alloc_symbol(&symbol_yes); |
| @@ -647,6 +648,30 @@ struct expr *expr_eliminate_dups(struct expr *e) · 199 unmodified lines | ||
| 647 | 648 | * Performs various simplifications involving logical operators and |
| 648 | 649 | * comparisons. |
| 649 | 650 | * |
| 651 | + * For bool type: | |
| 652 | + * A=n -> !A | |
| 653 | + * A=m -> n | |
| 654 | + * A=y -> A | |
| 655 | + * A!=n -> A | |
| 656 | + * A!=m -> y | |
| 657 | + * A!=y -> !A | |
| 658 | + * | |
| 659 | + * For any type: | |
| 660 | + * !!A -> A | |
| 661 | + * !(A=B) -> A!=B | |
| 662 | + * !(A!=B) -> A=B | |
| 663 | + * !(A<=B) -> A>B | |
| 664 | + * !(A>=B) -> A<B | |
| 665 | + * !(A<B) -> A>=B | |
| 666 | + * !(A>B) -> A<=B | |
| 667 | + * !(A || B) -> !A && !B | |
| 668 | + * !(A && B) -> !A || !B | |
| 669 | + * | |
| 670 | + * For constant: | |
| 671 | + * !y -> n | |
| 672 | + * !m -> m | |
| 673 | + * !n -> y | |
| 674 | + * | |
| 650 | 675 | * Allocates and returns a new expression. |
| 651 | 676 | */ |
| 652 | 677 | struct expr *expr_transform(struct expr *e) |
| @@ -674,12 +699,14 @@ struct expr *expr_transform(struct expr *e) · 21 unmodified lines | ||
| 674 | 699 | if (e->left.sym->type != S_BOOLEAN) |
| 675 | 700 | break; |
| 676 | 701 | if (e->right.sym == &symbol_no) { |
| 702 | + // A=n -> !A | |
| 677 | 703 | e->type = E_NOT; |
| 678 | 704 | e->left.expr = expr_alloc_symbol(e->left.sym); |
| 679 | 705 | e->right.sym = NULL; |
| 680 | 706 | break; |
| 681 | 707 | } |
| 682 | 708 | if (e->right.sym == &symbol_mod) { |
| 709 | + // A=m -> n | |
| 683 | 710 | printf("boolean symbol %s tested for 'm'? test forced to 'n'\n", e->left.sym->name); |
| 684 | 711 | e->type = E_SYMBOL; |
| 685 | 712 | e->left.sym = &symbol_no; |
| @@ -687,6 +714,7 @@ struct expr *expr_transform(struct expr *e) · 1 unmodified line | ||
| 687 | 714 | break; |
| 688 | 715 | } |
| 689 | 716 | if (e->right.sym == &symbol_yes) { |
| 717 | + // A=y -> A | |
| 690 | 718 | e->type = E_SYMBOL; |
| 691 | 719 | e->right.sym = NULL; |
| 692 | 720 | break; |
| @@ -696,11 +724,13 @@ struct expr *expr_transform(struct expr *e) · 3 unmodified lines | ||
| 696 | 724 | if (e->left.sym->type != S_BOOLEAN) |
| 697 | 725 | break; |
| 698 | 726 | if (e->right.sym == &symbol_no) { |
| 727 | + // A!=n -> A | |
| 699 | 728 | e->type = E_SYMBOL; |
| 700 | 729 | e->right.sym = NULL; |
| 701 | 730 | break; |
| 702 | 731 | } |
| 703 | 732 | if (e->right.sym == &symbol_mod) { |
| 733 | + // A!=m -> y | |
| 704 | 734 | printf("boolean symbol %s tested for 'm'? test forced to 'y'\n", e->left.sym->name); |
| 705 | 735 | e->type = E_SYMBOL; |
| 706 | 736 | e->left.sym = &symbol_yes; |
| @@ -708,6 +738,7 @@ struct expr *expr_transform(struct expr *e) · 1 unmodified line | ||
| 708 | 738 | break; |
| 709 | 739 | } |
| 710 | 740 | if (e->right.sym == &symbol_yes) { |
| 741 | + // A!=y -> !A | |
| 711 | 742 | e->type = E_NOT; |
| 712 | 743 | e->left.expr = expr_alloc_symbol(e->left.sym); |
| 713 | 744 | e->right.sym = NULL; |
| @@ -717,7 +748,7 @@ struct expr *expr_transform(struct expr *e) · 3 unmodified lines | ||
| 717 | 748 | case E_NOT: |
| 718 | 749 | switch (e->left.expr->type) { |
| 719 | 750 | case E_NOT: |
| 720 | − // !!a -> a | |
| 751 | + // !!A -> A | |
| 721 | 752 | tmp = e->left.expr->left.expr; |
| 722 | 753 | free(e->left.expr); |
| 723 | 754 | free(e); |
| @@ -726,7 +757,7 @@ struct expr *expr_transform(struct expr *e) · 2 unmodified lines | ||
| 726 | 757 | break; |
| 727 | 758 | case E_EQUAL: |
| 728 | 759 | case E_UNEQUAL: |
| 729 | − // !a='x' -> a!='x' | |
| 760 | + // !(A=B) -> A!=B | |
| 730 | 761 | tmp = e->left.expr; |
| 731 | 762 | free(e); |
| 732 | 763 | e = tmp; |
| @@ -734,7 +765,7 @@ struct expr *expr_transform(struct expr *e) · 1 unmodified line | ||
| 734 | 765 | break; |
| 735 | 766 | case E_LEQ: |
| 736 | 767 | case E_GEQ: |
| 737 | − // !a<='x' -> a>'x' | |
| 768 | + // !(A<=B) -> A>B | |
| 738 | 769 | tmp = e->left.expr; |
| 739 | 770 | free(e); |
| 740 | 771 | e = tmp; |
| @@ -742,14 +773,14 @@ struct expr *expr_transform(struct expr *e) · 1 unmodified line | ||
| 742 | 773 | break; |
| 743 | 774 | case E_LTH: |
| 744 | 775 | case E_GTH: |
| 745 | − // !a<'x' -> a>='x' | |
| 776 | + // !(A<B) -> A>=B | |
| 746 | 777 | tmp = e->left.expr; |
| 747 | 778 | free(e); |
| 748 | 779 | e = tmp; |
| 749 | 780 | e->type = e->type == E_LTH ? E_GEQ : E_LEQ; |
| 750 | 781 | break; |
| 751 | 782 | case E_OR: |
| 752 | − // !(a || b) -> !a && !b | |
| 783 | + // !(A || B) -> !A && !B | |
| 753 | 784 | tmp = e->left.expr; |
| 754 | 785 | e->type = E_AND; |
| 755 | 786 | e->right.expr = expr_alloc_one(E_NOT, tmp->right.expr); |
| @@ -758,7 +789,7 @@ struct expr *expr_transform(struct expr *e) · 2 unmodified lines | ||
| 758 | 789 | e = expr_transform(e); |
| 759 | 790 | break; |
| 760 | 791 | case E_AND: |
| 761 | − // !(a && b) -> !a || !b | |
| 792 | + // !(A && B) -> !A || !B | |
| 762 | 793 | tmp = e->left.expr; |
| 763 | 794 | e->type = E_OR; |
| 764 | 795 | e->right.expr = expr_alloc_one(E_NOT, tmp->right.expr); |