Merge pull request #263 from GaloisInc/1.6

1.6 release prep

what4-transition-system/what4-transition-system.cabal

@@ -20,7 +20,7 @@ common dependencies
     , lens
     , parameterized-utils  >=2.0  && <2.2
     , text
-    , what4                ^>=1.5
+    , what4                ^>=1.6
 
 library
   import:           dependencies

what4/CHANGES.md

@@ -1,12 +1,31 @@
-# next (TBA)
+# 1.6 (May 2024)
+
+* Allow building with GHC 9.8.
+
+* Add more robust support for Constrained Horn Clause (CHC) solving:
+  * The `IsSymExprBuilder` class now has two additional methods,
+    `transformPredBV2LIA` and `transformSymFnLIA2BV`, which describe how to
+    transform a bitvector (BV) predicate into a linear integer arithmetic (LIA)
+    predicate and vice versa.
+  * The `runZ3Horn` and `writeZ3HornSMT2File` functions now take an additional
+    `Bool` argument. When this argument is `True`, Z3 will transform bitvector
+    CHCs into linear integer arithmetic CHCs, which can sometimes help Z3 to
+    solve CHC problems that it couldn't in a bitvector setting.
 
 * Add support for the `bitwuzla` SMT solver.
 
+* Add `bvZero` and `bvOne` functions, which are convenient shorthand for
+  constructing bitvectors with the values `0` and `1`, respectively.
+
 * Add `pushMuxOps` and `pushMuxOpsOption`. If this option is enabled, What4 will
   push certain `ExprBuilder` operations (e.g., `zext`) down to the branches of
   `ite` expressions. In some (but not all) circumstances, this can result in
   operations that are easier for SMT solvers to reason about.
 
+* `annotateTerm` no longer adds annotations to bound variable expressions, which
+  already have annotations attached to them. This should result in slightly
+  better performance and better pretty-printing.
+
 # 1.5.1 (October 2023)
 
 * Require building with `versions >= 6.0.2`.

what4/what4.cabal

@@ -1,6 +1,6 @@
 Cabal-version: 2.4
 Name:          what4
-Version:       1.5.1.0.99
+Version:       1.6.0.0.99
 Author:        Galois Inc.
 Maintainer:    [email protected], [email protected]
 Copyright:     (c) Galois, Inc 2014-2023