Algebra::combineOredClauses()   F
last analyzed

Complexity

Conditions 33
Paths 8525

Size

Total Lines 98

Duplication

Lines 0
Ratio 0 %

Importance

Changes 0
Metric Value
cc 33
nc 8525
nop 2
dl 0
loc 98
rs 0
c 0
b 0
f 0

How to fix   Long Method    Complexity   

Long Method

Small methods make your code easier to understand, in particular if combined with a good name. Besides, if your method is small, finding a good name is usually much easier.

For example, if you find yourself adding comments to a method's body, this is usually a good sign to extract the commented part to a new method, and use the comment as a starting point when coming up with a good name for this new method.

Commonly applied refactorings include:

1
<?php
2
namespace Psalm\Type;
3
4
use function array_filter;
5
use function array_keys;
6
use function array_map;
7
use function array_merge;
8
use function array_pop;
9
use function array_shift;
10
use function array_unique;
11
use function array_values;
12
use function count;
13
use function in_array;
14
use PhpParser;
15
use Psalm\Codebase;
16
use Psalm\Exception\ComplicatedExpressionException;
17
use Psalm\FileSource;
18
use Psalm\Internal\Analyzer\Statements\Expression\AssertionFinder;
19
use Psalm\Internal\Clause;
20
use function strlen;
21
use function strpos;
22
use function substr;
23
24
class Algebra
25
{
26
    /**
27
     * @param  array<string, non-empty-list<non-empty-list<string>>>  $all_types
28
     *
29
     * @return array<string, non-empty-list<non-empty-list<string>>>
0 ignored issues
show
Documentation introduced by
The doc-type array<string, could not be parsed: Expected ">" at position 5, but found "end of type". (view supported doc-types)

This check marks PHPDoc comments that could not be parsed by our parser. To see which comment annotations we can parse, please refer to our documentation on supported doc-types.

Loading history...
30
     */
31
    public static function negateTypes(array $all_types)
32
    {
33
        return array_filter(
34
            array_map(
35
                /**
36
                 * @param  non-empty-list<non-empty-list<string>> $anded_types
0 ignored issues
show
Documentation introduced by
The doc-type non-empty-list<non-empty-list<string>> could not be parsed: Unknown type name "non-empty-list" at position 0. (view supported doc-types)

This check marks PHPDoc comments that could not be parsed by our parser. To see which comment annotations we can parse, please refer to our documentation on supported doc-types.

Loading history...
37
                 *
38
                 * @return list<non-empty-list<string>>
0 ignored issues
show
Documentation introduced by
The doc-type list<non-empty-list<string>> could not be parsed: Expected "|" or "end of type", but got "<" at position 4. (view supported doc-types)

This check marks PHPDoc comments that could not be parsed by our parser. To see which comment annotations we can parse, please refer to our documentation on supported doc-types.

Loading history...
39
                 */
40
                function (array $anded_types) {
41
                    if (count($anded_types) > 1) {
42
                        $new_anded_types = [];
43
44
                        foreach ($anded_types as $orred_types) {
45
                            if (count($orred_types) > 1) {
46
                                return [];
47
                            }
48
49
                            $new_anded_types[] = self::negateType($orred_types[0]);
50
                        }
51
52
                        return [$new_anded_types];
53
                    }
54
55
                    $new_orred_types = [];
56
57
                    foreach ($anded_types[0] as $orred_type) {
58
                        $new_orred_types[] = [self::negateType($orred_type)];
59
                    }
60
61
                    return $new_orred_types;
62
                },
63
                $all_types
64
            )
65
        );
66
    }
67
68
    /**
69
     * @param  string $type
70
     *
71
     * @return  string
72
     */
73
    private static function negateType($type)
74
    {
75
        if ($type === 'mixed') {
76
            return $type;
77
        }
78
79
        return $type[0] === '!' ? substr($type, 1) : '!' . $type;
80
    }
81
82
    /**
83
     * @param  PhpParser\Node\Expr      $conditional
84
     * @param  string|null              $this_class_name
85
     * @param  FileSource         $source
86
     *
87
     * @return array<int, Clause>
0 ignored issues
show
Documentation introduced by
The doc-type array<int, could not be parsed: Expected ">" at position 5, but found "end of type". (view supported doc-types)

This check marks PHPDoc comments that could not be parsed by our parser. To see which comment annotations we can parse, please refer to our documentation on supported doc-types.

Loading history...
88
     */
89
    public static function getFormula(
90
        int $object_id,
91
        PhpParser\Node\Expr $conditional,
92
        $this_class_name,
93
        FileSource $source,
94
        Codebase $codebase = null,
95
        bool $inside_negation = false,
96
        bool $cache = true
97
    ) {
98
        if ($conditional instanceof PhpParser\Node\Expr\BinaryOp\BooleanAnd ||
99
            $conditional instanceof PhpParser\Node\Expr\BinaryOp\LogicalAnd
100
        ) {
101
            $left_assertions = self::getFormula(
102
                $object_id,
103
                $conditional->left,
104
                $this_class_name,
105
                $source,
106
                $codebase,
107
                $inside_negation,
108
                $cache
109
            );
110
111
            $right_assertions = self::getFormula(
112
                $object_id,
113
                $conditional->right,
114
                $this_class_name,
115
                $source,
116
                $codebase,
117
                $inside_negation,
118
                $cache
119
            );
120
121
            return array_merge(
122
                $left_assertions,
123
                $right_assertions
124
            );
125
        }
126
127
        if ($conditional instanceof PhpParser\Node\Expr\BinaryOp\BooleanOr ||
128
            $conditional instanceof PhpParser\Node\Expr\BinaryOp\LogicalOr
129
        ) {
130
            // at the moment we only support formulae in CNF
131
132
            $left_clauses = self::getFormula(
133
                $object_id,
134
                $conditional->left,
135
                $this_class_name,
136
                $source,
137
                $codebase,
138
                $inside_negation,
139
                $cache
140
            );
141
142
            $right_clauses = self::getFormula(
143
                $object_id,
144
                $conditional->right,
145
                $this_class_name,
146
                $source,
147
                $codebase,
148
                $inside_negation,
149
                $cache
150
            );
151
152
            return self::combineOredClauses($left_clauses, $right_clauses);
153
        }
154
155
        if ($conditional instanceof PhpParser\Node\Expr\BooleanNot) {
156
            if ($conditional->expr instanceof PhpParser\Node\Expr\BinaryOp\BooleanOr) {
157
                $and_expr = new PhpParser\Node\Expr\BinaryOp\BooleanAnd(
158
                    new PhpParser\Node\Expr\BooleanNot(
159
                        $conditional->expr->left,
160
                        $conditional->getAttributes()
161
                    ),
162
                    new PhpParser\Node\Expr\BooleanNot(
163
                        $conditional->expr->right,
164
                        $conditional->getAttributes()
165
                    ),
166
                    $conditional->expr->getAttributes()
167
                );
168
169
                return self::getFormula(
170
                    $object_id,
171
                    $and_expr,
172
                    $this_class_name,
173
                    $source,
174
                    $codebase,
175
                    $inside_negation,
176
                    false
177
                );
178
            }
179
180
            if ($conditional->expr instanceof PhpParser\Node\Expr\Isset_
181
                && count($conditional->expr->vars) > 1
182
            ) {
183
                $assertions = null;
184
185
                if ($cache && $source instanceof \Psalm\Internal\Analyzer\StatementsAnalyzer) {
186
                    $assertions = $source->node_data->getAssertions($conditional->expr);
187
                }
188
189
                if ($assertions === null) {
190
                    $assertions = AssertionFinder::scrapeAssertions(
191
                        $conditional->expr,
192
                        $this_class_name,
193
                        $source,
194
                        $codebase,
195
                        $inside_negation,
196
                        $cache
197
                    );
198
199
                    if ($cache && $source instanceof \Psalm\Internal\Analyzer\StatementsAnalyzer) {
200
                        $source->node_data->setAssertions($conditional->expr, $assertions);
201
                    }
202
                }
203
204
                if ($assertions !== null) {
205
                    $clauses = [];
206
207
                    foreach ($assertions as $var => $anded_types) {
208
                        $redefined = false;
209
210
                        if ($var[0] === '=') {
211
                            /** @var string */
212
                            $var = substr($var, 1);
213
                            $redefined = true;
214
                        }
215
216
                        foreach ($anded_types as $orred_types) {
217
                            $clauses[] = new Clause(
218
                                [$var => $orred_types],
219
                                false,
220
                                true,
221
                                $orred_types[0][0] === '='
222
                                    || $orred_types[0][0] === '~'
223
                                    || (strlen($orred_types[0]) > 1
224
                                        && ($orred_types[0][1] === '='
225
                                            || $orred_types[0][1] === '~')),
226
                                $redefined ? [$var => true] : [],
227
                                $object_id
228
                            );
229
                        }
230
                    }
231
232
                    return self::negateFormula($clauses);
233
                }
234
            }
235
236
            if ($conditional->expr instanceof PhpParser\Node\Expr\BinaryOp\BooleanAnd) {
237
                $and_expr = new PhpParser\Node\Expr\BinaryOp\BooleanOr(
238
                    new PhpParser\Node\Expr\BooleanNot(
239
                        $conditional->expr->left,
240
                        $conditional->getAttributes()
241
                    ),
242
                    new PhpParser\Node\Expr\BooleanNot(
243
                        $conditional->expr->right,
244
                        $conditional->getAttributes()
245
                    ),
246
                    $conditional->expr->getAttributes()
247
                );
248
249
                return self::getFormula(
250
                    $object_id,
251
                    $and_expr,
252
                    $this_class_name,
253
                    $source,
254
                    $codebase,
255
                    $inside_negation,
256
                    false
257
                );
258
            }
259
260
            return self::negateFormula(
261
                self::getFormula(
262
                    $object_id,
263
                    $conditional->expr,
264
                    $this_class_name,
265
                    $source,
266
                    $codebase,
267
                    !$inside_negation
268
                )
269
            );
270
        }
271
272
        if ($conditional instanceof PhpParser\Node\Expr\BinaryOp\Identical
273
            || $conditional instanceof PhpParser\Node\Expr\BinaryOp\Equal
274
        ) {
275
            $false_pos = AssertionFinder::hasFalseVariable($conditional);
276
            $true_pos = AssertionFinder::hasTrueVariable($conditional);
277
278
            if ($false_pos === AssertionFinder::ASSIGNMENT_TO_RIGHT
279
                && ($conditional->left instanceof PhpParser\Node\Expr\BinaryOp\BooleanAnd
280
                    || $conditional->left instanceof PhpParser\Node\Expr\BinaryOp\BooleanOr)
281
            ) {
282
                $inside_negation = !$inside_negation;
283
284
                return self::getFormula(
285
                    $object_id,
286
                    $conditional->left,
287
                    $this_class_name,
288
                    $source,
289
                    $codebase,
290
                    $inside_negation,
291
                    $cache
292
                );
293
            }
294
295
            if ($false_pos === AssertionFinder::ASSIGNMENT_TO_LEFT
296
                && ($conditional->right instanceof PhpParser\Node\Expr\BinaryOp\BooleanAnd
297
                    || $conditional->right instanceof PhpParser\Node\Expr\BinaryOp\BooleanOr)
298
            ) {
299
                $inside_negation = !$inside_negation;
300
301
                return self::getFormula(
302
                    $object_id,
303
                    $conditional->right,
304
                    $this_class_name,
305
                    $source,
306
                    $codebase,
307
                    $inside_negation,
308
                    $cache
309
                );
310
            }
311
312
            if ($true_pos === AssertionFinder::ASSIGNMENT_TO_RIGHT
313
                && ($conditional->left instanceof PhpParser\Node\Expr\BinaryOp\BooleanAnd
314
                    || $conditional->left instanceof PhpParser\Node\Expr\BinaryOp\BooleanOr)
315
            ) {
316
                return self::getFormula(
317
                    $object_id,
318
                    $conditional->left,
319
                    $this_class_name,
320
                    $source,
321
                    $codebase,
322
                    $inside_negation,
323
                    $cache
324
                );
325
            }
326
327
            if ($true_pos === AssertionFinder::ASSIGNMENT_TO_LEFT
328
                && ($conditional->right instanceof PhpParser\Node\Expr\BinaryOp\BooleanAnd
329
                    || $conditional->right instanceof PhpParser\Node\Expr\BinaryOp\BooleanOr)
330
            ) {
331
                return self::getFormula(
332
                    $object_id,
333
                    $conditional->right,
334
                    $this_class_name,
335
                    $source,
336
                    $codebase,
337
                    $inside_negation,
338
                    $cache
339
                );
340
            }
341
        }
342
343
        $assertions = null;
344
345
        if ($cache && $source instanceof \Psalm\Internal\Analyzer\StatementsAnalyzer) {
346
            $assertions = $source->node_data->getAssertions($conditional);
347
        }
348
349
        if ($assertions === null) {
350
            $assertions = AssertionFinder::scrapeAssertions(
351
                $conditional,
352
                $this_class_name,
353
                $source,
354
                $codebase,
355
                $inside_negation,
356
                $cache
357
            );
358
359
            if ($cache && $source instanceof \Psalm\Internal\Analyzer\StatementsAnalyzer) {
360
                $source->node_data->setAssertions($conditional, $assertions);
361
            }
362
        }
363
364
        if ($assertions) {
365
            $clauses = [];
366
367
            foreach ($assertions as $var => $anded_types) {
368
                $redefined = false;
369
370
                if ($var[0] === '=') {
371
                    /** @var string */
372
                    $var = substr($var, 1);
373
                    $redefined = true;
374
                }
375
376
                foreach ($anded_types as $orred_types) {
377
                    $clauses[] = new Clause(
378
                        [$var => $orred_types],
379
                        false,
380
                        true,
381
                        $orred_types[0][0] === '='
382
                            || $orred_types[0][0] === '~'
383
                            || (strlen($orred_types[0]) > 1
384
                                && ($orred_types[0][1] === '='
385
                                    || $orred_types[0][1] === '~')),
386
                        $redefined ? [$var => true] : [],
387
                        $object_id
388
                    );
389
                }
390
            }
391
392
            return $clauses;
393
        }
394
395
        return [new Clause([], true)];
396
    }
397
398
    /**
399
     * This is a very simple simplification heuristic
400
     * for CNF formulae.
401
     *
402
     * It simplifies formulae:
403
     *     ($a) && ($a || $b) => $a
404
     *     (!$a) && (!$b) && ($a || $b || $c) => $c
405
     *
406
     * @param  array<int, Clause>  $clauses
407
     *
408
     * @return list<Clause>
0 ignored issues
show
Documentation introduced by
The doc-type list<Clause> could not be parsed: Expected "|" or "end of type", but got "<" at position 4. (view supported doc-types)

This check marks PHPDoc comments that could not be parsed by our parser. To see which comment annotations we can parse, please refer to our documentation on supported doc-types.

Loading history...
409
     */
410
    public static function simplifyCNF(array $clauses)
411
    {
412
        $cloned_clauses = [];
413
414
        // avoid strict duplicates
415
        foreach ($clauses as $clause) {
416
            $unique_clause = clone $clause;
417
            foreach ($unique_clause->possibilities as $var_id => $possibilities) {
418
                $unique_clause->possibilities[$var_id] = array_values(array_unique($possibilities));
419
            }
420
            $cloned_clauses[$clause->getHash()] = $unique_clause;
421
        }
422
423
        // remove impossible types
424
        foreach ($cloned_clauses as $clause_a) {
425
            if (count($clause_a->possibilities) !== 1 || count(array_values($clause_a->possibilities)[0]) !== 1) {
426
                continue;
427
            }
428
429
            if (!$clause_a->reconcilable || $clause_a->wedge) {
430
                continue;
431
            }
432
433
            $clause_var = array_keys($clause_a->possibilities)[0];
434
            $only_type = array_pop(array_values($clause_a->possibilities)[0]);
435
            $negated_clause_type = self::negateType($only_type);
436
437
            foreach ($cloned_clauses as $clause_b) {
438
                if ($clause_a === $clause_b || !$clause_b->reconcilable || $clause_b->wedge) {
439
                    continue;
440
                }
441
442
                if (isset($clause_b->possibilities[$clause_var]) &&
443
                    in_array($negated_clause_type, $clause_b->possibilities[$clause_var], true)
444
                ) {
445
                    $clause_var_possibilities = array_values(
446
                        array_filter(
447
                            $clause_b->possibilities[$clause_var],
448
                            /**
449
                             * @param string $possible_type
450
                             *
451
                             * @return bool
452
                             */
453
                            function ($possible_type) use ($negated_clause_type) {
454
                                return $possible_type !== $negated_clause_type;
455
                            }
456
                        )
457
                    );
458
459
                    if (!$clause_var_possibilities) {
460
                        unset($clause_b->possibilities[$clause_var]);
461
                        $clause_b->impossibilities = null;
462
                    } else {
463
                        $clause_b->possibilities[$clause_var] = $clause_var_possibilities;
464
                    }
465
                }
466
            }
467
        }
468
469
        $deduped_clauses = [];
470
471
        // avoid strict duplicates
472
        foreach ($cloned_clauses as $clause) {
473
            $deduped_clauses[$clause->getHash()] = clone $clause;
474
        }
475
476
        $deduped_clauses = array_filter(
477
            $deduped_clauses,
478
            /**
479
             * @return bool
480
             */
481
            function (Clause $clause) {
482
                return count($clause->possibilities) || $clause->wedge;
483
            }
484
        );
485
486
        $simplified_clauses = [];
487
488
        foreach ($deduped_clauses as $clause_a) {
489
            $is_redundant = false;
490
491
            foreach ($deduped_clauses as $clause_b) {
492
                if ($clause_a === $clause_b
493
                    || !$clause_b->reconcilable
494
                    || $clause_b->wedge
495
                    || $clause_a->wedge
496
                ) {
497
                    continue;
498
                }
499
500
                if ($clause_a->contains($clause_b)) {
501
                    $is_redundant = true;
502
                    break;
503
                }
504
            }
505
506
            if (!$is_redundant) {
507
                $simplified_clauses[] = $clause_a;
508
            }
509
        }
510
511
        return $simplified_clauses;
512
    }
513
514
    /**
515
     * Look for clauses with only one possible value
516
     *
517
     * @param  list<Clause>  $clauses
0 ignored issues
show
Documentation introduced by
The doc-type list<Clause> could not be parsed: Expected "|" or "end of type", but got "<" at position 4. (view supported doc-types)

This check marks PHPDoc comments that could not be parsed by our parser. To see which comment annotations we can parse, please refer to our documentation on supported doc-types.

Loading history...
518
     * @param  array<string, bool> $cond_referenced_var_ids
519
     * @param  array<string, array<int, array<int, string>>> $active_truths
520
     *
521
     * @return array<string, array<int, array<int, string>>>
0 ignored issues
show
Documentation introduced by
The doc-type array<string, could not be parsed: Expected ">" at position 5, but found "end of type". (view supported doc-types)

This check marks PHPDoc comments that could not be parsed by our parser. To see which comment annotations we can parse, please refer to our documentation on supported doc-types.

Loading history...
522
     */
523
    public static function getTruthsFromFormula(
524
        array $clauses,
525
        ?int $creating_object_id = null,
526
        array &$cond_referenced_var_ids = [],
527
        array &$active_truths = []
528
    ) {
529
        $truths = [];
530
        $active_truths = [];
531
532
        if (empty($clauses)) {
533
            return [];
534
        }
535
536
        foreach ($clauses as $clause) {
537
            if (!$clause->reconcilable) {
538
                continue;
539
            }
540
541
            foreach ($clause->possibilities as $var => $possible_types) {
542
                // if there's only one possible type, return it
543
                if (count($clause->possibilities) === 1 && count($possible_types) === 1) {
544
                    $possible_type = array_pop($possible_types);
545
546
                    if (isset($truths[$var]) && !isset($clause->redefined_vars[$var])) {
547
                        $truths[$var][] = [$possible_type];
548
                    } else {
549
                        $truths[$var] = [[$possible_type]];
550
                    }
551
552
                    if ($creating_object_id && $creating_object_id === $clause->creating_object_id) {
553
                        if (!isset($active_truths[$var])) {
554
                            $active_truths[$var] = [];
555
                        }
556
557
                        $active_truths[$var][count($truths[$var]) - 1] = [$possible_type];
558
                    }
559
                } elseif (count($clause->possibilities) === 1) {
560
                    // if there's only one active clause, return all the non-negation clause members ORed together
561
                    $things_that_can_be_said = array_filter(
562
                        $possible_types,
563
                        /**
564
                         * @param  string $possible_type
565
                         *
566
                         * @return bool
567
                         */
568
                        function ($possible_type) {
569
                            return $possible_type[0] !== '!';
570
                        }
571
                    );
572
573
                    if ($things_that_can_be_said && count($things_that_can_be_said) === count($possible_types)) {
574
                        $things_that_can_be_said = array_unique($things_that_can_be_said);
575
576
                        if ($clause->generated && count($possible_types) > 1) {
577
                            unset($cond_referenced_var_ids[$var]);
578
                        }
579
580
                        /** @var array<int, string> $things_that_can_be_said */
581
                        $truths[$var] = [$things_that_can_be_said];
582
583
                        if ($creating_object_id && $creating_object_id === $clause->creating_object_id) {
584
                            $active_truths[$var] = [$things_that_can_be_said];
585
                        }
586
                    }
587
                }
588
            }
589
        }
590
591
        return $truths;
592
    }
593
594
    /**
595
     * @param  non-empty-array<int, Clause>  $clauses
596
     *
597
     * @return array<int, Clause>
0 ignored issues
show
Documentation introduced by
The doc-type array<int, could not be parsed: Expected ">" at position 5, but found "end of type". (view supported doc-types)

This check marks PHPDoc comments that could not be parsed by our parser. To see which comment annotations we can parse, please refer to our documentation on supported doc-types.

Loading history...
598
     */
599
    public static function groupImpossibilities(array $clauses)
600
    {
601
        $complexity = 1;
602
603
        $seed_clauses = [];
604
605
        $clause = array_pop($clauses);
606
607
        if (!$clause->wedge) {
608
            if ($clause->impossibilities === null) {
609
                throw new \UnexpectedValueException('$clause->impossibilities should not be null');
610
            }
611
612
            foreach ($clause->impossibilities as $var => $impossible_types) {
613
                foreach ($impossible_types as $impossible_type) {
614
                    $seed_clause = new Clause(
615
                        [$var => [$impossible_type]],
616
                        false,
617
                        true,
618
                        false,
619
                        [],
620
                        $clause->creating_object_id
621
                    );
622
623
                    $seed_clauses[] = $seed_clause;
624
625
                    ++$complexity;
626
                }
627
            }
628
        }
629
630
        if (!$clauses || !$seed_clauses) {
631
            return $seed_clauses;
632
        }
633
634
        while ($clauses) {
635
            $clause = array_pop($clauses);
636
637
            $new_clauses = [];
638
639
            foreach ($seed_clauses as $grouped_clause) {
640
                if ($clause->impossibilities === null) {
641
                    throw new \UnexpectedValueException('$clause->impossibilities should not be null');
642
                }
643
644
                foreach ($clause->impossibilities as $var => $impossible_types) {
645
                    foreach ($impossible_types as $impossible_type) {
646
                        $new_clause_possibilities = $grouped_clause->possibilities;
647
648
                        if (isset($grouped_clause->possibilities[$var])) {
649
                            $new_clause_possibilities[$var][] = $impossible_type;
650
                        } else {
651
                            $new_clause_possibilities[$var] = [$impossible_type];
652
                        }
653
654
                        $new_clause = new Clause(
655
                            $new_clause_possibilities,
656
                            false,
657
                            true,
658
                            true,
659
                            [],
660
                            $clause->creating_object_id === $grouped_clause->creating_object_id
661
                                ? $clause->creating_object_id
662
                                : null
663
                        );
664
665
                        $new_clauses[] = $new_clause;
666
667
                        ++$complexity;
668
669
                        if ($complexity > 20000) {
670
                            throw new ComplicatedExpressionException();
671
                        }
672
                    }
673
                }
674
            }
675
676
            $seed_clauses = $new_clauses;
677
        }
678
679
        return $seed_clauses;
680
    }
681
682
    /**
683
     * @param  array<int, Clause>  $left_clauses
684
     * @param  array<int, Clause>  $right_clauses
685
     *
686
     * @return array<int, Clause>
0 ignored issues
show
Documentation introduced by
The doc-type array<int, could not be parsed: Expected ">" at position 5, but found "end of type". (view supported doc-types)

This check marks PHPDoc comments that could not be parsed by our parser. To see which comment annotations we can parse, please refer to our documentation on supported doc-types.

Loading history...
687
     */
688
    public static function combineOredClauses(array $left_clauses, array $right_clauses)
689
    {
690
        $clauses = [];
691
692
        $all_wedges = true;
693
        $has_wedge = false;
694
695
        foreach ($left_clauses as $left_clause) {
696
            foreach ($right_clauses as $right_clause) {
697
                $all_wedges = $all_wedges && ($left_clause->wedge && $right_clause->wedge);
698
                $has_wedge = $has_wedge || ($left_clause->wedge && $right_clause->wedge);
699
            }
700
        }
701
702
        if ($all_wedges) {
703
            return [new Clause([], true)];
704
        }
705
706
        foreach ($left_clauses as $left_clause) {
707
            foreach ($right_clauses as $right_clause) {
708
                if ($left_clause->wedge && $right_clause->wedge) {
709
                    // handled below
710
                    continue;
711
                }
712
713
                /** @var  array<string, non-empty-list<string>> */
714
                $possibilities = [];
715
716
                $can_reconcile = true;
717
718
                if ($left_clause->wedge ||
719
                    $right_clause->wedge ||
720
                    !$left_clause->reconcilable ||
721
                    !$right_clause->reconcilable
722
                ) {
723
                    $can_reconcile = false;
724
                }
725
726
                foreach ($left_clause->possibilities as $var => $possible_types) {
727
                    if (isset($right_clause->redefined_vars[$var])) {
728
                        continue;
729
                    }
730
731
                    if (isset($possibilities[$var])) {
732
                        $possibilities[$var] = array_merge($possibilities[$var], $possible_types);
733
                    } else {
734
                        $possibilities[$var] = $possible_types;
735
                    }
736
                }
737
738
                foreach ($right_clause->possibilities as $var => $possible_types) {
739
                    if (isset($possibilities[$var])) {
740
                        $possibilities[$var] = array_merge($possibilities[$var], $possible_types);
741
                    } else {
742
                        $possibilities[$var] = $possible_types;
743
                    }
744
                }
745
746
                if (count($left_clauses) > 1 || count($right_clauses) > 1) {
747
                    foreach ($possibilities as $var => $p) {
748
                        $possibilities[$var] = array_values(array_unique($p));
749
                    }
750
                }
751
752
                foreach ($possibilities as $var_possibilities) {
753
                    if (count($var_possibilities) === 2) {
754
                        if ($var_possibilities[0] === '!' . $var_possibilities[1]
755
                            || $var_possibilities[1] === '!' . $var_possibilities[0]
756
                        ) {
757
                            continue 2;
758
                        }
759
                    }
760
                }
761
762
                $creating_object_id = $right_clause->creating_object_id === $left_clause->creating_object_id
763
                    ? $right_clause->creating_object_id
764
                    : null;
765
766
                $clauses[] = new Clause(
767
                    $possibilities,
768
                    false,
769
                    $can_reconcile,
770
                    $right_clause->generated
771
                        || $left_clause->generated
772
                        || count($left_clauses) > 1
773
                        || count($right_clauses) > 1,
774
                    [],
775
                    $creating_object_id
776
                );
777
            }
778
        }
779
780
        if ($has_wedge) {
781
            $clauses[] = new Clause([], true);
782
        }
783
784
        return $clauses;
785
    }
786
787
    /**
788
     * Negates a set of clauses
789
     * negateClauses([$a || $b]) => !$a && !$b
790
     * negateClauses([$a, $b]) => !$a || !$b
791
     * negateClauses([$a, $b || $c]) =>
792
     *   (!$a || !$b) &&
793
     *   (!$a || !$c)
794
     * negateClauses([$a, $b || $c, $d || $e || $f]) =>
795
     *   (!$a || !$b || !$d) &&
796
     *   (!$a || !$b || !$e) &&
797
     *   (!$a || !$b || !$f) &&
798
     *   (!$a || !$c || !$d) &&
799
     *   (!$a || !$c || !$e) &&
800
     *   (!$a || !$c || !$f)
801
     *
802
     * @param  array<int, Clause>  $clauses
803
     *
804
     * @return non-empty-list<Clause>
0 ignored issues
show
Documentation introduced by
The doc-type non-empty-list<Clause> could not be parsed: Unknown type name "non-empty-list" at position 0. (view supported doc-types)

This check marks PHPDoc comments that could not be parsed by our parser. To see which comment annotations we can parse, please refer to our documentation on supported doc-types.

Loading history...
805
     */
806
    public static function negateFormula(array $clauses)
807
    {
808
        if (!$clauses) {
809
            return [new Clause([], true)];
810
        }
811
812
        foreach ($clauses as $clause) {
813
            self::calculateNegation($clause);
814
        }
815
816
        $impossible_clauses = self::groupImpossibilities($clauses);
817
818
        if (!$impossible_clauses) {
819
            return [new Clause([], true)];
820
        }
821
822
        $negated = self::simplifyCNF($impossible_clauses);
823
824
        if (!$negated) {
825
            return [new Clause([], true)];
826
        }
827
828
        return $negated;
829
    }
830
831
    /**
832
     * @param  Clause $clause
833
     *
834
     * @return void
835
     */
836
    public static function calculateNegation(Clause $clause)
837
    {
838
        if ($clause->impossibilities !== null) {
839
            return;
840
        }
841
842
        $impossibilities = [];
843
844
        foreach ($clause->possibilities as $var_id => $possibility) {
845
            $impossibility = [];
846
847
            foreach ($possibility as $type) {
848
                if (($type[0] !== '=' && $type[0] !== '~'
849
                        && (!isset($type[1]) || ($type[1] !== '=' && $type[1] !== '~')))
850
                    || strpos($type, '(')
851
                    || strpos($type, 'getclass-')
852
                ) {
853
                    $impossibility[] = self::negateType($type);
854
                }
855
            }
856
857
            if ($impossibility) {
858
                $impossibilities[$var_id] = $impossibility;
859
            }
860
        }
861
862
        $clause->impossibilities = $impossibilities;
863
    }
864
}
865