Support sbv-10.*
#1513
Labels
dependencies
Pull requests that update a dependency file
Comments
RyanGlScott
added a commit
that referenced
this issue
May 26, 2023
`sbv-10.0` brings in two changes to the SBV internals that affect Cryptol. 1. `sbv-10.0` removes the `generateSMTBenchmark` function in favor of two separate `generateSMTBenchmarkSat` and `generateSMTBenchmarkProof` functions. 2. `sbv-10.0` removes the `allSatHasPrefixExistentials` field of `AllSatResult`. We now use the appropriate CPP to make Cryptol compile before and after these changes. Fixes #1513.
RyanGlScott
added a commit
that referenced
this issue
May 26, 2023
`sbv-10.0` brings in two changes to the SBV internals that affect Cryptol. 1. `sbv-10.0` removes the `generateSMTBenchmark` function in favor of two separate `generateSMTBenchmarkSat` and `generateSMTBenchmarkProof` functions. 2. `sbv-10.0` removes the `allSatHasPrefixExistentials` field of `AllSatResult`. We now use the appropriate CPP to make Cryptol compile before and after these changes. Fixes #1513.
RyanGlScott
added a commit
to GaloisInc/saw-script
that referenced
this issue
Aug 31, 2023
`sbv-10.*` brings in two changes to the SBV internals that affects SAW: 1. `sbv-10.0` removes the `generateSMTBenchmark` function in favor of two separate `generateSMTBenchmarkSat` and `generateSMTBenchmarkProof` functions. We use the `generateSMTBenchmarkSat` variant in `SAWScript.Prover.Exporter`. 2. `sbv-10.0` changes the `Maybe [String]` argument to `svUninterpreted` (which we use in `saw-core-sbv`'s `Verifier.SAW.Simulator.SBV`) to a `UICodeKind` argument, where `UINone` is now what used to be denoted with `Nothing`. We now use the appropriate CPP to make SAW compile before and after these changes. See also GaloisInc/cryptol#1513, which was in similar territory.
RyanGlScott
added a commit
to GaloisInc/saw-script
that referenced
this issue
Nov 20, 2023
`sbv-10.*` brings in two changes to the SBV internals that affects SAW: 1. `sbv-10.0` removes the `generateSMTBenchmark` function in favor of two separate `generateSMTBenchmarkSat` and `generateSMTBenchmarkProof` functions. We use the `generateSMTBenchmarkSat` variant in `SAWScript.Prover.Exporter`. 2. `sbv-10.0` changes the `Maybe [String]` argument to `svUninterpreted` (which we use in `saw-core-sbv`'s `Verifier.SAW.Simulator.SBV`) to a `UICodeKind` argument, where `UINone` is now what used to be denoted with `Nothing`. We now use the appropriate CPP to make SAW compile before and after these changes. See also GaloisInc/cryptol#1513, which was in similar territory.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
sbv-10.0andsbv-10.1were recently released, and with them come some internal changes that Cryptol will need to adapt to. In particular, Cryptol uses thegenerateSMTBenchmarkfunction here:cryptol/src/Cryptol/Symbolic/SBV.hs
Line 473 in c941edd
But
sbv-10.0removesgenerateSMTBenchmarkin favor of two separategenerateSMTBenchmarkSatandgenerateSMTBenchmarkProoffunctions.The text was updated successfully, but these errors were encountered: