diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-07-09 12:24:50 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-07-09 17:24:50 +0000 |
commit | e25d2ce5eff672bb5b58c245f0414a1ed9c51a6c (patch) | |
tree | 4713df6d48a3a61a551a361a4d511dc229d083ea /docs/binary/binary.rst | |
parent | ff91290122d478dc637fb3e9ff4fe4c0ead5bd32 (diff) |
Fix sets cardinality inference involving equivalent parents (#6855)
This fixes an unsoundness issue in the sets + cardinality solver.
One rule of this solver applies in sets when two parents of a child of a cardinality graph are equal, in which case we know that child or one of its siblings must be equal to the opposite parent. For example, this rule tells us that:
if T = (union T S), then (intersect T S) = S.
The explanation of this rule could consider the representative term of one the parents instead of the term itself say (union T S) is representative T, giving the unsound inference: if (union T S) = (union T S), then (intersect T S) = S. This ensures we use the original terms.
This PR also does some minor cleanup.
Diffstat (limited to 'docs/binary/binary.rst')
0 files changed, 0 insertions, 0 deletions