The `data-binary-ieee754` library, which `what4` depends on, is deprecated.
Fortunately, `what4` only uses this library for converting `Float`s and
`Double`s to `Word`s, which is functionality that the `base` library has
provided since GHC 8.2. As a result, removing the `data-binary-ieee754`
dependency is straightforward.
This fixes #195—or, at the very least, makes the deprecation warnings that
arise from `tasty-hedgehog`'s version of `testProperty` go away. The "real"
fix would be to convert every use of `testProperty` into a top-level `Property`
value, but given how tedious that would be, I'm disinclined to do this unless
someone specifically requests it.
This contains a variety of changes needed to make the libraries in the `what4`
compile warning-free with GHC 9.2:
* GHC 9.2 includes `-Woperator-whitespace-ext-conflict` as a part of `-Wall`,
which causes `Test.Verification` to warn when built with GHC 9.2. The fix is
simple: just add spaces after certain uses of the `$` character.
* GHC 9.2 includes `-Wincomplete-uni-patterns` as a part of `-Wall`, which
causes `GenWhat4Expr` to warn when built with GHC 9.2. I fixed the warnings
by introducing new `from{Bool,Int,BV8,BV16,BV32,BV64}TestExpr` functions to
extract the payloads of different `TestExpr` constructors. This is no less
partial than before, but at least this way any accidental partiality will
result in a more descriptive error message than
`Non-exhaustive patterns in ...`.
* In `base-4.16.*`, `Nat` is now a type synonym for `Natural`, and
`GHC.TypeNats` now re-exports `Natural`. This causes an import of
`Numeric.Natural` in `What4.SemiRing` (previously required to bring `Natural`
into scope) trigger an `-Wunused-imports` warning. I fixed the warning by
using explicit imports from `GHC.TypeNats` and `Numeric.Natural`.
* The `aig` and `abcBridge` submodules were bumped to bring in the changes
from GaloisInc/aig#12 and GaloisInc/abcBridge#19, respectively, which allows
them to build with `base-4.16.*`.
* The upper version bounds on `base` were raised in `what4-abc`, `what4-blt`,
and `what4-transition-system` to allow them to build with `base-4.16.*`.
Previously, we were too liberal with the characters we would emit
without escaping, and we would incorrectly fail to escape `\` characters
if they had a following `u` character. In addition, our unescaping routine
was incorrectly rejecting strings from solvers if they ended with a literal
`\` character.
Fixes#184Fixes#185
Instead of doing exponential search followed by binary search, there may be
situations in which it is faster to jump straight into binary search. This
commit allows configuring which search strategy to use in `resolveSymBV` by way
of a `SearchStrategy` data type. In the future, we may even consider adding
other search strategies.
Sometimes, `{un,}signedBVBounds` aren't sufficient to determine the lower and
upper bounds of a `SymBV`. For these situations, it can be helpful to query the
SMT solver to search for the bounds, later using `unsafeSetAbstractValue` to
update the newly discovered bounds to unlock further What4 simplifications.
The `resolveSymBV` function does exactly this kind of search. I've added
`hedgehog` tests which ensure that it behaves the way you'd expect it to.
This allows unsafely setting the abstract domain used by an expression.
This is primarily useful for symbolic expressions whose bounds have been
queried externally, as updating the bounds can sometimes unlock further
simplifications in subsequent What4 operations.
Doing so will cause the integers to be rendered with decimals (e.g., `0.0`
instead of `0`). While some solvers are OK with such integers, CVC4 is picky
and will reject integers with decimal places, as seen in #182. The fix is
straightforward: just use `integerTerm` instead of
`rationalTerm . fromInteger`.
Fixes#182.
