Lowering to SAT/SMT #7
Description
We currently compare the existing resolver in cargo to a new resolver based on PubGrub. This comparison is extremely useful at present while the implementations are entirely disjoint. At some point cargo will upstream a PubGrub based resolver and this comparison will no longer be able to identify those bugs. Adding an additional implementation(s) would help ensure that we continue to get the correct result. This could be a lowering to SAT, like varisat which is currently done in both Cargo and PubGrub, and allows for fewer rust dependencies. Or we could lower to SMT, like z3 which provides higher-level abstractions but is not straightforward to build. Or we could lower to resolvo, which also implements dependency resolution but has seen less production hardening.