* Add additional SMT solvers to Docker image.
This change downloads specific stable release versions of each supported SMT solver to the Dockerfile. In cases where a build was available(yices, cvc4, Mathsat), it is downloaded directly. In other cases, it is build from a specific source snapshot (boolector, abc). These versions could be changes if desired.
This allows easy access to Cryptol and all solvers in a single Docker container, which is useful since some common problems are not amenable to solution with Z3 alone.
As with the original Cryptol Dockerfile, this implementation uses Docker's staged build functionality both to keep the final size as small as possible and to modularize the build. If desired, this segment could be copied verbatim to the SAW Dockerfile to add additional solvers there as well.
Note that this Dockerfile doesn't currently build. However, the new segment has been tested and does work. It may be desirable to update the rest of the Dockerfile before adding this change.
This is semantically the same as `map` on finite sequences,
but forks a separate Haskell thread for each element of the sequence.
When the GHC runtime is instructed to use multiple OS threads,
data-parallel exeuction can be achieved.
More precisely, in both cases we unload all modules and then reload
everything (this is what `:l` used to do, while `:m` only reloaded
the current module). This fixes#668.
There are opportunities to be smarter here: in particular when we
reload modules, we do need to parse them so that we can find out what
their dependencies are, and if needed to reload those. However, if
none of the dependencies have changed, and we didn't change, then we
could reuse the current module. This could be quite useful for modules
that take a long time to load.
We now allow indented fenced blocks. Apparently those happen if you
want to put code in a list. This being markdown, things are ambiguous,
but the main change is that if we see an indented line that starts with
``` now we treat it as starting a fenced block, rather than an
indented code block.
This fixes#805
This used to look for decimal literals applied to specific primitive
operations and cause them to silently default to bitvector types
large enough to hold their values.
With the new literal defaulting system, this special case is no longer
necessary.
use that information to emit error messages rather than warnings.
This provides more specific messages than simply allowing the
affected type variables to remain uninstantiated and failing later.
It also causes some examples that otherwise would have ambiguous
types to fail earlier. This converts some test instances where
REPL defaulting would eventually succeed into examples that fail
outright instead. I largely think these instances are improvements.
Fix up the test suite. This mostly delays defaulting
warnings into "showing specific instance of polymorpic
type warnings", but requires actual fixes in a small number
of places. Those places were higly questionable, in my opinion.
Instead of relying on the internal SBV portfolio mechanism, we simply
do it ourselves "from the outside". The SBV portfolio solver now works
in essentially the same way as the What4 one: if the first result we
get is an error, we continue waiting for other solvers and only
present exceptions to the user if all provers fail.
Fixes#798Fixes#693
This turned out to be relatively straightforward. Using
a simliar strategy to SBV, we simply spawn off all the solvers
in separate threads and wait using the `async` package.
Some minor fixes in `What4` allow the threads to respond properly
to being interrupted.
Some care is required to install the necessary solver options
_before_ spawning off the threads to avoid race conditions
in the configuration datastructure itself; such race conditions should
be fixed in What4 at some point.
When configuring the SBV `yices` solver, search for both
spellings of the SMTLib2 executable for `yices`. Different
environments/packaging, for some reason, use different names
for this.
Fixes#592
Rather than looking up prover information by name every
time we do a proof, we fetch the prover configuration as soon
as the user selects a prover using `:set prover=` and remember
it as part of the REPL state. This will allow us to
do some work at configuration time and remember the results.
As part of this refactoring, we now print the list of solvers
that SBV found when using `:set prover=any`.
