what4-1.2: CHANGES.md

# 1.2 (June 2021)

This is primarily a bugfix release, but also adds support
for GHC 9.x

* Tweaks to the `SolverEvent` data type to remove partial
fields.

* Fix issue #126.  The shift operations of `What4.SWord` were
not correctly handling cases where the shift amount has more
bits than the word to be shifted.

* Fix issue #121. The ordering of inputs in generated Verilog files is
now more predictable. Previously, it was determined by the order the
inputs were encountered during term traversal. Now the user can provide
a list of (input, name) pairs which are declared in order. Any
additional inputs discovered during traversal will be added after these
specified inputs.

* Fix issue #113.  The `bvSliceLE` and `bvSliceBE` functions of
`What4.SWord` did not properly handle size 0 bit-vectors and
requests for 0 length slices.  They now correctly fail for slice
lengths longer than 0 on 0-length vectors, and correctly
allow 0 length slices regardless of the length of the input.

* Fix issue #103. Some of the string operations would give incorrect
results when string offsets are out-of-bounds.  The SMTLib 2.6 standard
specifies precise results for these cases, which we now implement.

* Configuration parameters relative to solvers have been renamed in a
  more consistent and heirarchical fashion; the old configuration
  parameters still work but will emit deprecation warnings when used.

  * `default_solver` --> `solver.default`
  * `abc_path` --> `solver.abc.path`
  * `boolector_path` --> `solver.boolector.path`
  * `cvc4_path` --> `solver.cvc4.path`
  * `cvc4.random-seed` --> `solver.cvc4.random-seed`
  * `cvc4_timeout` --> `solver.cvc4.timeout`
  * `dreal_path` --> `solver.dreal.path`
  * `stp_path` --> `solver.stp.path`
  * `stp.random-seed` --> `solver.stp.random-seed`
  * `yices_path` --> `solver.yices.path`
  * `yices_enable-mcsat` --> `solver.yices.enable-mcsat`
  * `yices_enable-interactive` --> `solver.yices.enable-interactive`
  * `yices_goal_timeout` --> `solver.yices.goal-timeout`
  * `yices.*` --> `solver.yices.*` for many yices internal options
  * `z3_path` --> `solver.z3.path`
  * `z3_timeout` --> `solver.z3.timeout`

* Added the `solver.strict_parsing` configuration parameter.  This is
  enabled by default but could be disabled to allow running solvers in
  debug mode or to workaround other unexpected output from solver
  processes.

# 1.1 (February 2021)

* Use multithread-safe storage primitive for configuration options,
  and clarify single-threaded use assumptions for other data structures.

* Fix issue #63, which caused traversals to include the bodies of
defined functions at call sites, which yielded confusing results.

* Add concrete evaluation and constant folding for floating-point
operations via the `libBF` library.

* Add min and max operations for integers and reals to the expression interface.

* Remove `BaseNatType` from the set of base types. There were bugs
  relating to having nat types appear in structs, arrays and
  functions that were difficult to fix. Natural number values are
  still available as scalars (where they are represented by integers with
  nonzero assumptions) via the `SymNat` type.

* Support for exporting What4 terms to Verilog syntax.

* Various documentation fixes and improvements.

* Test coverage improvements.

* Switch to use the `prettyprinter` package for user-facing output.

# 1.0 (July 2020)

* Initial Hackage release