- Notifications
You must be signed in to change notification settings - Fork5
Commit99419d3
committed
Allow predicate_refuted_by() to deduce that NOT A refutes A.
We had originally made the stronger assumption that NOT A refutes any Bif B implies A, but this fails in three-valued logic, because we need toprove B is false not just that it's not true. However the logic doesgo through if B is equal to A.Recognizing this limited case is enough to handle examples that arise whenwe have simplified "bool_var = true" or "bool_var = false" to just "bool_var"or "NOT bool_var". If we had not done that simplification then thebtree-operator proof logic would have been able to prove that the expressionswere contradictory, but only for identical expressions being compared to theconstants; so handling identical A and B covers all the same cases.The motivation for doing this is to avoid unexpected asymmetrical behaviorwhen a partitioned table uses a boolean partitioning column, as in today'sgripe from Dominik Sander.Back-patch to 8.2, which is as far back as predicate_refuted_by attempts todo anything at all with NOTs.1 parent1951c97 commit99419d3
1 file changed
+38
-12
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
9 | 9 | | |
10 | 10 | | |
11 | 11 | | |
12 | | - | |
| 12 | + | |
13 | 13 | | |
14 | 14 | | |
15 | 15 | | |
| |||
95 | 95 | | |
96 | 96 | | |
97 | 97 | | |
| 98 | + | |
98 | 99 | | |
99 | 100 | | |
100 | 101 | | |
| |||
468 | 469 | | |
469 | 470 | | |
470 | 471 | | |
| 472 | + | |
| 473 | + | |
471 | 474 | | |
472 | 475 | | |
473 | 476 | | |
| |||
651 | 654 | | |
652 | 655 | | |
653 | 656 | | |
654 | | - | |
655 | | - | |
656 | 657 | | |
657 | | - | |
| 658 | + | |
658 | 659 | | |
659 | | - | |
660 | | - | |
661 | | - | |
662 | | - | |
| 660 | + | |
| 661 | + | |
| 662 | + | |
| 663 | + | |
| 664 | + | |
663 | 665 | | |
664 | | - | |
665 | | - | |
666 | | - | |
| 666 | + | |
| 667 | + | |
667 | 668 | | |
668 | | - | |
669 | 669 | | |
670 | 670 | | |
671 | 671 | | |
| |||
1178 | 1178 | | |
1179 | 1179 | | |
1180 | 1180 | | |
| 1181 | + | |
| 1182 | + | |
| 1183 | + | |
| 1184 | + | |
| 1185 | + | |
| 1186 | + | |
| 1187 | + | |
| 1188 | + | |
| 1189 | + | |
| 1190 | + | |
| 1191 | + | |
| 1192 | + | |
| 1193 | + | |
| 1194 | + | |
| 1195 | + | |
| 1196 | + | |
| 1197 | + | |
| 1198 | + | |
| 1199 | + | |
| 1200 | + | |
| 1201 | + | |
| 1202 | + | |
| 1203 | + | |
| 1204 | + | |
| 1205 | + | |
| 1206 | + | |
1181 | 1207 | | |
1182 | 1208 | | |
1183 | 1209 | | |
| |||
0 commit comments
Comments
(0)