Invalid `ParadoxicalCondition` raised with nested conditions in if statement

[driehle]

The following code raises two ParadoxicalCondition errors:

$isImmutable = substr($typeOfField, -9) === 'immutable';

if (
    ($isImmutable && $value instanceof DateTimeImmutable)
    || (! $isImmutable && $value instanceof DateTime)
) {
    return $value;
} elseif ($isImmutable && $value instanceof DateTime) {
    return DateTimeImmutable::createFromMutable($value);
} elseif (! $isImmutable && $value instanceof DateTimeImmutable) {
    return DateTime::createFromImmutable($value);
}

ERROR: ParadoxicalCondition - src/DoctrineObject.php:620:23 - Condition (($value is DateTime) && ($isImmutable)) contradicts a previously-established condition ($value is not DateTime) (see https://psalm.dev/089)
                } if ($isImmutable && $value instanceof DateTime) {

ERROR: ParadoxicalCondition - src/DoctrineObject.php:622:27 - Condition (($value is DateTimeImmutable) && (!$isImmutable)) contradicts a previously-established condition ($value is not DateTimeImmutable) (see https://psalm.dev/089)
                } elseif ((! $isImmutable) && $value instanceof DateTimeImmutable) {

Rewriting the first if condition in two statements makes the error disappear:

$isImmutable = substr($typeOfField, -9) === 'immutable';

if ($isImmutable && $value instanceof DateTimeImmutable) {
    return $value;
} elseif (! $isImmutable && $value instanceof DateTime) {
    return $value;
} elseif ($isImmutable && $value instanceof DateTime) {
    return DateTimeImmutable::createFromMutable($value);
} elseif (! $isImmutable && $value instanceof DateTimeImmutable) {
    return DateTime::createFromImmutable($value);
}

Code example: https://psalm.dev/r/d26bab675e

[psalm-github-bot[bot]]

I found these snippets:

https://psalm.dev/r/d26bab675e

```php

[driehle]

@greg0ire has further simplified down the issue to https://psalm.dev/r/53f79d44aa.

[psalm-github-bot[bot]]

I found these snippets:

https://psalm.dev/r/53f79d44aa

```php

[orklah]

Reduced even more: https://psalm.dev/r/e79c2894ec

Must be a flaw in boolean module of Psalm. Which I believe is located in FormulaGenerator::getFormula. It's 400 lines of recursive boolean operations. It's gonna be tricky

[psalm-github-bot[bot]]

I found these snippets:

https://psalm.dev/r/e79c2894ec

```php

[muglug]

OK so this is tricky.

($a && $b) || (!$a && $c)

is expanded by Psalm to the conjunctive normal form

($a || $c) && (!$a || $b) && ($b || $c)

This equivalent (to Psalm) version demonstrates the same bug.

But when you enter that CNF into Wolfram Alpha it tells you the last term is unnecessary.

If you remove the unnecessary term the bug disappears.

The buggy method is Algebra::combineOredClauses, but I don't know how to fix it — combineOredClauses is a pretty simple method that just applies the standard distributed method for converting DNF to CNF. Then it looks like Algebra::negateFormula has incorrect behaviour when passed a formula with unnecessary terms, but I don't think that is a bug — negateFormula expects an optimal CNF.

I don't, honestly, remember how to obviously get the DNF to CNF conversion correct (missing the unnecessary term) on paper — once that was correct, fixing the combineOredClauses method wouldn't be too difficult. Either way the solution would probably slow down combineOredClauses.

[psalm-github-bot[bot]]

I found these snippets:

https://psalm.dev/r/76864ff3a5

```php

https://psalm.dev/r/bc5487153d

```php

[muglug]

Another example:

These two are functionally similar but give different output: https://psalm.dev/r/8f6b691a68

[psalm-github-bot[bot]]

I found these snippets:

https://psalm.dev/r/8f6b691a68

```php

[muglug]

The solution is for me to add a rule to reduce the specific pattern

(A || <set of orred terms X>)
    && (!A || <set of orred terms Y>)
    && (<set of orred terms X> || <set of orred terms Y>)

to

(A || <set of orred terms X>)
    && (!A || <set of orred terms Y>)

i.e. when we have two clauses that negate a term within one another and another clause that's just the two uncontradicted terms together that clause is redundant. Should be a reasonably simple rule to add.

[orklah]

This is fixed on Psalm 5! Thanks Matt!