Remove dependency on abcBridge #1320
Conversation
There was a problem hiding this comment.
Looks good to me, but we should also think about what documentation we should add along with it. It looks like multiple commands have switched status along the deprecated/current/experimental axis, so there should probably be at least something in the change log about that.
| @@ -1314,7 +1307,7 @@ primitives = Map.fromList | |||
| ] | |||
|
|
|||
| , prim "abc" "ProofScript ()" | |||
There was a problem hiding this comment.
I looks like you removed abc from pretty much all of the example scripts and such. Should this command be Deprecated instead?
There was a problem hiding this comment.
I'm still debating that, honestly. I've tried making abc map to w4_abc_aiger, w4_abc_smtlib2, and w4_abc_verilog, and there are always cases where at least one of the benchmarks that worked well with the old abc doesn't work well with that choice (though all benchmarks seem to work well with at least one prover, either a mode of ABC or Yices). So, does having abc still exist for backward compatibility make sense if it will sometimes work equally well and sometimes not? It's hard to say.
There was a problem hiding this comment.
Any interest in having the "best" solver for each example discovered automatically eventually? @kquick could be a good future use of the dependency reasoning automation you're working on.
There was a problem hiding this comment.
@ldettwy this is something that has been discussed but as I currently understand it, the likely approach will probably be to simultaneously submit the formula to multiple solvers and take the first responder. Other than specific functionality areas that may not be supported, it is difficult to predict which solvers will do better for a particular problem so it's unlikely that my constraint solver will be helpful in this regard.
There was a problem hiding this comment.
Yeah, Cryptol has any and all solvers and we might want to adopt a similar approach in SAW.
And there are still a bunch of uses of abc in the integration tests, even though I changed a few. Also, many of the external verifications (s2n, AWS-LC, BLS, etc.) use it. So, given that it does still exist in some form, I'm inclined to leave it.
Yep, good point! I'll add some change log stuff. |
atomb
added
the
PR: ready to merge
| @@ -3,7 +3,7 @@ double_imp <- llvm_extract l "double_imp"; | |||
| double_ref <- llvm_extract l "double_ref"; | |||
| let thm = {{ \x -> double_ref x == double_imp x }}; | |||
|
|
|||
| r <- prove abc thm; | |||
| r <- prove yices thm; | |||
There was a problem hiding this comment.
Is anything checking these exercises/tutorials? @benjaminselfridge could we eventually get something like https://github.com/GaloisInc/cryptol/blob/master/cryptol/CheckExercises.hs implemented for this if not?
There was a problem hiding this comment.
Yep, there's an integration test that pulls them in. That's how I discovered that this would be a lot faster with Yices. :)
| git submodule update --init | ||
| git -C deps/abcBridge submodule update --init | ||
| with: | ||
| submodules: true |
There was a problem hiding this comment.
I think the original intent was to checkout only the abcBridge dependency and not the entire set of submodules, @ldettwy .
This introduces a `w4_abc_aiger` command that invokes ABC as an external process on a generated AIGER file. Also makes `abc` a synonym for `w4_abc_aiger`, so that it behaves similarly to how it did with the `abcBridge`-based `abc` command (specifically, using the same bit-blasting approach from the `aig` library). Introducing this command required some refactoring to the types of many of the prover interfaces, making functions that were in `IO` be in `TopLevel`, instead. This generally seems to be a simplification.
Includes test used to identify the bug.
This makes some run significantly faster
This makes them depend less on ABC, which we haven't installed as widely, and often isn't the best choice anymore.
The hope is that the failures on macOS are just failures invoking Yices, and that they’ll work for Z3.
This PR removes the dependency of SAW on
abcBridge. It preserves some of the existing SAW commands by including new features in theaigpackage for reading and writing AIGER files. For the moment, it does not preserve thececcommand, as it wasn't widely used. We could implement it in terms of an externalabcinvocation if needed, though.For the moment, this PR does not remove the
abcBridgesubmodule because the build system currently still uses it to build theabcexecutable, even though it's no longer linked in as a library. Once some of the reusable CI infrastructure for solvers is done, we can use that instead of this submodule.Closes #975.