I personally feel like it's best to not do dependency injection for the solver backends, especially because a download or build of all of them is going to add a lot to the already large toolchain download (nextpnr might need splitting up when it gains Xilinx 7 Series support, as it's already a pretty large download).

I used to have the toolchain injected into python3Packages.nmigen, but eventually concluded that a build tool that calls out to external tools should probably not inject dependencies for all the tools it could be used to invoke; it's more appropriate to inject those dependencies either at the application level (as is done in glasgow) or include the appropriate other tools along with the build tool in the derivation inputs.

That said, I wouldn't mind too much depending on just yices (the "preferred" backend, AIUI) and including it in propagatedBuildInputs by default, as it would make the common use-case work out of the box without adding unduly to the build/download weight.

Sounds good to me. Is there any downside to including the non-default solvers as optional deps defaulting to false? That way they're still wrapped up with the package, but won't add to build/download weight.

I guess I mostly just don't see too much of a difference between nativeBuildInputs = [ (symbiyosys.override { withBoolector = true; }) ]; and nativeBuildInputs = [ symbiyosys boolector ];, but I'm fine deferring to your or anyone else's opinions on this; I don't have a commit bit anyway ^^;

You're right, it's minor. My preference here is that if I have a derivation that uses symbiyosys and then decide to remove it, it doesn't require that I remember to also remove boolector, which I only included in the first place because I was using symbiyosys.

Sorry this has taken so long to get back to. My basic position is this: I agree with @emilazy here, and I think generally injecting all of these backends is probably not a good idea by default. However, I also agree there's a balance to be struct between "works out of the box" and "minimal closure size", and having symbiyosys work out of the box is desirable.

Therefore, I'd like to see this PR simply add yices as a propagated build input, so things will work by default. But I would prefer if that were all it did, with no other options. The minor nit you mentioned is still real, but in general it's true a lot of other ways inside nixpkgs, and going against the grain here leads to a lot more code for us to maintain for a bunch of solvers going forward. Personally I normally use some 'outer' derivation to wrap the others together with a consistent setup in such cases, which is what I'd suggest going for in cases like this if alternative solvers are really needed for your uses.

@thoughtpolice I've adjusted the commit to reflect your suggestions. I completely agree with your reasoning. Also, thanks for the suggestion to use an outer derivation. I'd previously been using an overlay, but I like your solution better.

@matthuszagh Thanks! Sorry again this took so long