GaloisInc / saw-script

The SAW scripting language.
BSD 3-Clause "New" or "Revised" License
441 stars 63 forks source link

Allow sharing abc solver cache entries between OSs #2080

Open mrogers67 opened 3 months ago

mrogers67 commented 3 months ago

Determining the solver version for SBV.ABC currently yields a string specific to the operating system.

For example, this is from Ubuntu:

$ abc -q "version;quit"
UC Berkeley, ABC 1.01 (compiled Dec 12 2022 14:58:41)

And here's the output on macOS:

$ abc -q "version;quit"
UC Berkeley, ABC 1.01 (compiled Dec 12 2022 15:01:38)

They're the same version, yet they'll unfortunately produce different hash keys.

A possible solution might be to match the version string inside those messages and use that as input to the hash key instead?

Also, it seems that the arguments ["-q", "version;quit"] would be correct, without the leading "s"?

RyanGlScott commented 3 months ago

Good catch. I agree that leaking timestamps into version numbers is quite unfortunate, and we should strive to remove them. We might also consider doing the same in the original what4 code that this was based on, although the what4 code isn't used for caching purposes (just debugging information), so it's less important there.

Also, I agree that it would be better to run abc -q "version;quit" rather than abc s -q "version;quit", as the latter has the unfortunate side effect of starting an interactive abc session. Most of the time, we are invoking abc subprocesses in a non-interactive way, so we usually don't notice this. It is definitely noticeable when you try to run the same command in an interactive shell, however (given that you have to Ctrl-D afterwards to exit).