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.
This was removed from the `flakes` repo in GaloisInc/flakes#7. The rationale is
that odd Yices version numbers are development versions, and we only want to
test release versions. `what4`'s CI was testing 2.6.1 (a development version),
so let's just remove it.
Bitwuzla is a relatively new SMT solver with support for the bitvector,
floating point, array, and uninterpreted function theories. This patch adds the
necessary plumbing to invoke Bitwuzla using What4.
Co-authored-by: Ryan Scott <rscott@galois.com>
`versions-6.0.2` introduces a `Lift Version` instance, which finally allows us
to delete the ugly, CPP'd mess of orphan instances that we define in
`What4.Utils.Versions`.
Related to #240.
`versions-6.0.*` removes the `VChunk` data type, which `what4` defines an
orphan `Lift` instance for. This requires some CPP to fix up. This is somewhat
messy, and in an ideal world, we'd move these orphan instances directly to the
`versions` library. (See also https://github.com/fosskers/versions/issues/68.)
Fixes#240.
This patch contains a variety of fixes needed to build the libraries in the
`what4` repo with GHC 9.6:
* GHC 9.6 bundles `mtl-2.3.*`, which no longer re-exports `Control.Monad`,
`Control.Monad.IO.Class`, and similar modules from `mtl`-related modules.
To accommodate this, various imports have been made more explicit.
* `MonadTrans t` now has a quantified `forall m. Monad m => Monad (t m)`
superclass in `mtl-2.3.*`. As a result, the `MonadTrans (PartialT sym)`
instance must now have an `IsExpr (SymExpr sym)` instance context in order
for it to typecheck, as this is the same instance context that `PartialT`'s
`Monad` instance has.
This is technically a breaking change, so I have noted it in the `what4`
changelog. That being said, this change is unlikely to affect many people
in practice, considering that the `MonadTrans` instance for `PartialT` is
usually used in tandem with the `Monad` instance.
* Various upper version bounds on `base` have been lifted to allow building
with `base-4.18`.
* The `aig` submodule has been bumped to bring in the changes from
GaloisInc/aig#15, which allows it to build with GHC 9.6.
