`base-4.20` (GHC 9.10) re-exports `foldl'` from the `Prelude`, which conflicts
with the `foldl'` function defined in `What4.Utils.Word16String`. To avoid
conflicts, we re-export `What4.Utils.Word16String.foldl'` using a qualified
export, which avoids warnings in a backwards-compatible fashion.
Fixes#272.
Bump the upper version bounds on `base` in the various `what4` packages, and
bump the `aig` submodule to bring in the changes from
https://github.com/GaloisInc/aig/pull/18.
CVC5 1.0.2 appears to suffer from a bug that causes it to hang when run on the
`expr-builder-smtlib2` test suite. Let's upgrade to a more recent version that
does not suffer from this bug.
Due to a bug in CVC4 (https://github.com/cvc5/cvc5/issues/3402), the What4
bindings to CVC4 avoid user-defined datatypes and instead use CVC4's built-in
`Tuple` datatype. This same `Tuple` workaround was applied to the CVC5 bindings
(added in #204), but they don't really work properly, as CVC4 and CVC5 use
completely different syntaxes for tuples. See #265.
We could attempt to update the CVC5 bindings to use the modern tuple syntax,
but this is somewhat non-trivial, as the syntax for 1-tuples changed in
`cvc5-1.0.9` from `Tuple` to `UnitTuple` (see
https://github.com/cvc5/cvc5/pull/10012). As such, we would have to generate
different code for different versions of CVC5, which would be unpleasant.
Thankfully, we need not worry about tuples at all when it comes to CVC5. This
is because the original CVC4 issue (https://github.com/cvc5/cvc5/issues/3402)
does not affect CVC5. As such, we can drop the tuple workaround entirely and
just generate user-defined datatypes to represent What4 structs, exactly like
the other solver bindings do. This means that we can fix#265 by simply
deleting code, which is nice.
This is regression-tested as part of the `expr-builder-smtlib2` test suite
(which includes several tuple-related tests), after a previous commit made it
so that the tests are run with both CVC4 and CVC5.
Fixes#265.
Due to a silly oversight, we weren't actually running the
`expr-builder-smtlib2` tests on CVC4. Instead, we were simply defining `let
cvc5Tests = cvc4Tests`, which meant that running `cvc5Tests` would simply
re-run the CVC4 tests.
This patch tweaks the tests to _actually_ run the tests separately with CVC5.
Doing so reveals some test failures with CVC5 specifically, all of which are
caused by the bug described in #265. I will fix this bug in a follow-up commit.
Fixes#257. The HLint configuration only checks that these helpers are
used where appropriate. I used it to find places where they would be
useful. It may also serve as a template for downstream repos. I added
HLint checking to CI as well.
The previous code, defined in terms of `unsnoc`, required multiple `panic`
cases, which was somewhat unsightly. This new implementation is functionally
equivalent, does not require any `panic` fall-through cases, and is much nicer
to look at.
This patch contains a variety of fixes needed to build the libraries in the
what4 repo with GHC 9.8:
* Bump the upper version bounds on `base` and `text` to allow building with the
versions that are bundled with GHC 9.8 (`base-4.19.*` and `text-2.1.*`,
respectively).
* Replace uses of `head` and `tail` (which trigger `-Wx-partial` warnings with
GHC 9.8) with total functions or `panic`s, depending on what is appropriate.
* Bump the `aig` submodule to bring in the changes from GaloisInc/aig#16 and
GaloisInc/aig#17.
