mauke

tybalt89 discovered a bug in Fun with logical expressions:

$ echo IEabEba | perl try.pl
ORIG: IEabEba
MOD: V~V~V~a~b;~V~~a~~b;;V~V~b~a;~V~~b~~a;;;
...> V~V~V~a~b;~Vab;;V~V~b~a;~Vba;;;
...> V~V~V~a~b;~Vab;;~V~b~a;~Vba;;
Not a tautology

(a equals b) implies (b equals a) is a tautology but the program fails to recognize it. With the fixed code below it generates this output instead:

$ echo IEabEba | perl taut.pl
ORIG: IEabEba
MOD: V~V~V~a~b;~V~~a~~b;;V~V~b~a;~V~~b~~a;;;
...> V~V~V~a~b;~Vab;;V~V~b~a;~Vba;;;
...> V~V~V~a~b;~Vab;;~V~b~a;~Vba;;
...> V~Vba;~V~V~a~b;~Vab;;~V~b~a;;
...> V~Vab;~V~Vab;~V~a~b;;~V~a~b;;
...> V~Vab;~V0~V~a~b;;~V~a~b;;
...> V~Vab;~V~V~a~b;;~V~a~b;;
...> V~Vab;~~V~a~b;~V~a~b;;
...> V~Vab;V~a~b;~V~a~b;;
...> V~Vab;~a~b~V~a~b;;
...> V~Vab;~a~b~V0~b;;
...> V~Vab;~a~b~V~b;;
...> V~Vab;~a~b~~b;
...> V~Vab;~a~bb;
...> V~V1b;~a~bb;
...> V~1~a~bb;
...> V0~a~bb;
...> V~a~bb;
...> V~a~b1;
...> 1
Tautology

The following changes were made to the code:

1. The "regex libraries" $rawlib and $modlib and their named subpatterns (?&rawexpr) and (?&exp) are gone. They were replaced by $rawexpr and $exp, subregexes that directly match and capture a simplifed and modified expression, respectively.

   This change was made in order to make it possible to split a string into subexpressions using my @expr = $str =~ /$exp/g (i.e. m//g in list context).

2. Two regexes were simplified by using \K.

3. The old "final rule" did some duplicate work: It used index($1, $3) < 0 && index($4, $3) < 0 inside the regex to search for the subexpression $3 in both $1 and $4. If successful, it repeated the search in the replacement part: s{ \Q$x\E }{$spec}g for $pre, $post;

   The new version uses s/// directly in the regex and checks the return value to see if any match was found/replaced. The replacement string is assembled directly in the regex and saved in an outer lexical variable to make it available in the right-hand side.

4. A new rule was added. If the other rules get stuck, it reorders V operands. The canonical order chosen is simply the default sort behavior: lexicographically ascending strings.

Due to change #3 and #4 the code no longer works on old perls (before v5.18) because in v5.18 the implementation of embedded code blocks in regexes was rewritten, fixing many bugs.

The new code:

#!/usr/bin/env perl
use v5.18.0;
use warnings;
use re '/xms';

my $rawexpr = qr{
    (
        (?>
            [a-z]
        |
            N (?-1)
        |
            [CDIE] (?-1) (?-1)
        )
    )
};

my $exp = qr{
    (
        (?>
            [01a-z]
        |
            ~ (?-1)
        |
            V (?-1)*+ ;
        )
    )
};

while (readline) {
    chomp;
    say "ORIG: $_";

    1 while s{ E $rawexpr $rawexpr }{DC$1$2CN$1N$2}g;
    1 while s{ I $rawexpr $rawexpr }{DN$1$2}g;
    1 while s{ C $rawexpr $rawexpr }{NDN$1N$2}g;
    1 while s{ D $rawexpr $rawexpr }{V$1$2;}g;
    tr/N/~/;

    say "MOD: $_";

    say "...> $_" while 0
        || s{ ~ ~ }{}g
        || s{ ~ 0 }{1}g
        || s{ ~ 1 }{0}g
        || s{ V ; }{0}g
        || s{ V $exp ; }{$1}g
        || s{ V $exp* \K V ($exp*+) ; }{$2}g
        || s{ V $exp* \K 0 }{}g
        || s{ V $exp* 1 $exp*+ ; }{1}g
        || do {
            my $repl;
            s{
                V ($exp*?) (~??) $exp ($exp*+) ;
                (?(?{
                    my ($pre, $neg, $x, $post) = ($1, $3, $4, $5);
                    my $spec = $neg ? '1' : '0';
                    my $n = 0;
                    $n += s{ \Q$x\E }{$spec}g for $pre, $post;
                    $repl = "V$pre$neg$x$post;";
                    !$n
                }) (*FAIL) )
            }{$repl}g
        }
        || do {
            my $canon;
            s{
                V ($exp {2,}+) ;
                (?(?{
                    my $orig = $1;
                    $canon = join '', sort $orig =~ m{ $exp }g;
                    $orig eq $canon
                }) (*FAIL) )
            }{V$canon;}g
        }
    ;

    say $_ eq '1' ? "Tautology" : "Not a tautology", "\n";
}

__END__