bsc: remove stp support

[thoughtpolice]

I've got a few cleanups to the codebase I wanted to do from a while back, and this is one of them. :) It follows in the footsteps of the CUDD removal several years ago. Really, this was annoying me because during compilation there are just a ton of really annoying warnings and stuff too, and it takes a while to compile everything.

Ideally, we would move to smtlib, and I think in the long run that's still right move. In the meantime, we can lighten the load and delete a ton of cruft by getting rid of the built-in STP. Note: I didn't remove any of the paths for SAT_Yices or the data type itself, because I think it should hopefully be possible to add a SAT_SMTLib case instead. Then we can delete the yices case in another change, a follow up to simplify the code paths and delete the data type entirely, and finally live happily ever after.

[thoughtpolice]

I'll also note this allows us to obsolete several other PRs as well; in general I think it's the right move. I have a bunch of touch ups I want to do across the code but I think smtlib support is doable, and it's definitely possible to find some license-compatible solvers and distribute them. So I think in the short run this is still a net win in support, complexity, etc.

(Edit: Also hi @quark17! Hope you're doing well.)

[thoughtpolice]

I went for a walk and remembered that I had forgotten that I actually proposed this exact change over 4 years ago! Time flies! #31

In the intermittent timeframe I think little has changed overall, except that the old STP snapshot has gotten rustier and older. Meanwhile I think many SMT solvers have redistributable binaries and there are more open-source ones with compatible licenses now than ever (boolector, z3, cvc5, etc).

So maybe we should instead just do the right thing and replace it with smtlib support outright and then delete yices and STP all in one swoop. We can then get a solver in place for the distributables and the CI/dev testing. In the past the problem was we didn't have a test suite, but now we do, so I think that's a much better spot...

I'll leave this to Julie to decide but I'm happy to let this get closed, I got a chuckle out of looking up the old PR. :)

[quark17]

A couple things to note:

• STP is now in GitHub, and recently tagged a new release (v2.3.4): https://github.com/stp/stp
• Yices also recently tagged a new release (v2.6.5): https://github.com/SRI-CSL/yices2
• It appears that STP won in the Bit Vector category at SMT-COMP in all metrics, beating out Yices, Z3, and cvc5: https://smt-comp.github.io/2023/results/qf-bitvec-single-query
• Build options can be used to skip the building of the STP or Yices library, if you want (currently it does this by building a stub library -- there are known bugs in the Makefiles for this that should be fixed, though)

We got rid of CUDD because it was a bottleneck. SMT solvers allowed for many more queries than previously possible. It's not unreasable to write modules that may require millions of queries. So I'd like to understand the overhead of using an SMTLib interface -- would it reintroduce a bottleneck? If I understand, it would require sending queries as text, which then have to be parsed by another process? The way that BSC currently uses the SMT solves, it caches pointers to expressions that have already been built, so that it doesn't rebuild them; I guess that the other process responding to queries could do the caching, but does it? (Back when Yices was added, we did some benchmarking on an example with many queries, and found that Yices was a bit faster. But sounds like maybe now STP is faster.)

My preference would be replace the STP snapshot with a github submodule (like Yices); update both STP and Yices to the newest releases; and change BSC's build to statically link them into BSC. This static linking would eliminate the need for a SAT directory in the installation, and having to add it to the LD_LIBRARY_PATH. It would also greatly simplify the process for building BSC without STP or Yices: right now, a stub .so file is created, so that the executable will link when run, and the first thing BSC does is to call some functions in the API to ask if it's a stub or not; instead, BSC's source can statically know whether STP or Yices was compiled into it, and not need to do this dance at run-time.