tree 76db0ac9d058c303cb55a539f61cadfd1cfe348c
parent 183e3242a361bb86eaf65be68366cfde72e80d12
author Alastair Donaldson <afdx@google.com> 1586277507 +0100
committer GitHub <noreply@github.com> 1586277507 +0100
gpgsig -----BEGIN PGP SIGNATURE-----
 
 wsBcBAABCAAQBQJejKyDCRBK7hj4Ov3rIwAAdHIIAHHiLzlSDtptz9jE3o7SvJn3
 ABCwlv4XpD8o//TaZ0j2z8+piWTCjphh+VUI88Wuj0MsM9uv4WmrU82m53WkF5UX
 4Hmg6WacBv3hcdd6I8swyLcCk9+oI3dht5/gI6DTRR7VPAS4UrToc7xqJgg6eWrZ
 DatybIUaYbxSRKSGbZAmqREBe6i3u42p7LBwnVFlZ6v0FcE1Y9mzz1iezutmg21G
 m84bE6F8IgOqKR0gX2/8qUGfB9Nsvi7Ejw6wOHscfFXEcin/1ARL0ZmYmez2fqrS
 ikHYR8VkC2p23EWC4CNj7apwv3DjsKueCt+k2SSyWdLnq8yfn0XBWwyLrwH8DMc=
 =64H1
 -----END PGP SIGNATURE-----
 

spirv-fuzz: Improve the handling of equation facts (#3281)

The management of equation facts suffered from two problems:

(1) The processing of an equation fact required the data descriptors
    used in the equation to be in canonical form.  However, during
    fact processing it can be deduced that certain data descriptors
    are equivalent, causing their equivalence classes to be merged,
    and that could cause previously canonical data descriptors to no
    longer be canonical.

(2) Related to this, if id equations were known about a canonical data
    descriptor dd1, and other id equations known about a different
    canonical data descriptor dd2, the equation facts about these data
    descriptors were not being merged in the event that dd1 and dd2
    were deduced to be equivalent.

This changes solves (1) by not requiring equation facts to be in
canonical form while processing them, but instead always checking
whether (not necessary canonical) data descriptors are equivalent when
looking for corollaries of equation facts, rather than comparing them
using ==.

Problem (2) is solved by adding logic to merge sets of equations when
data descriptors are made equivalent.

In addition, the change also requires elements to be registered in an
equivalence relation before they can be made equivalent, rather than
being added (if not already present) at the point of being made
equivalent.