From 979e83084c50db399e39b30ac791fd295b1e983a Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Fri, 29 Nov 2024 12:58:17 -0800 Subject: [PATCH] Mention higher order support --- CHANGES.md | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/CHANGES.md b/CHANGES.md index 2ec73c69..10f24775 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -5,6 +5,14 @@ * Generalize the signatures of the default project-embed implementations of the Queriable class. + * Generalize support for higher-order functions. These are still experimental, as SMTLib's higher-order + function support is nascent. (Version 3 of SMTLib will have proper support for such functions, which + is not released yet.) Currently, SBV can handle higher order versions of any, all, and filter, all + exported from Data.SBV.List module. These functions take as arguments lambda-functions, and SBV + translates them carefully for Z3 and CVC5 which has preliminary support. Proof-support in backend + solvers for higher-order functions is still quite weak, though KnuckleDragger makes things easier. + See Documentation.SBV.Examples.KnuckleDragger.Lists for several examples. + ### Version 11.0, 2024-11-06 * [BACKWARDS COMPATIBILITY] SBV now handles arrays in a much more uniform way, unifying